Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison src/OD.agda @ 1148:d39c79bb71f0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
recovered
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 16 Jan 2023 14:01:45 +0900
parents f46a16cebbab
children 7d2bae0ff36b
comparison
equal deleted inserted replaced
1146:1966127fc14f 1148:d39c79bb71f0
214 eq← ∅0 {w} lt = lift (¬x<0 lt) 214 eq← ∅0 {w} lt = lift (¬x<0 lt)
215 215
216 ∅< : { x y : HOD } → odef x (& y ) → ¬ ( od x == od od∅ ) 216 ∅< : { x y : HOD } → odef x (& y ) → ¬ ( od x == od od∅ )
217 ∅< {x} {y} d eq with eq→ (==-trans eq (==-sym ∅0) ) d 217 ∅< {x} {y} d eq with eq→ (==-trans eq (==-sym ∅0) ) d
218 ∅< {x} {y} d eq | lift () 218 ∅< {x} {y} d eq | lift ()
219
220 0<P→ne : { x : HOD } → o∅ o< & x → ¬ ( od x == od od∅ )
221 0<P→ne {x} 0<x eq = ⊥-elim ( o<¬≡ (sym (=od∅→≡o∅ eq)) 0<x )
219 222
220 ∈∅< : { x : HOD } {y : Ordinal } → odef x y → o∅ o< (& x) 223 ∈∅< : { x : HOD } {y : Ordinal } → odef x y → o∅ o< (& x)
221 ∈∅< {x} {y} d with trio< o∅ (& x) 224 ∈∅< {x} {y} d with trio< o∅ (& x)
222 ... | tri< a ¬b ¬c = a 225 ... | tri< a ¬b ¬c = a
223 ... | tri≈ ¬a b ¬c = ⊥-elim ( ∅< {x} {* y} (subst (λ k → odef x k ) (sym &iso) d ) ( ≡o∅→=od∅ (sym b) ) ) 226 ... | tri≈ ¬a b ¬c = ⊥-elim ( ∅< {x} {* y} (subst (λ k → odef x k ) (sym &iso) d ) ( ≡o∅→=od∅ (sym b) ) )