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

comparison ODC.agda @ 396:8c092c042093

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 27 Jul 2020 15:11:54 +0900
parents 8b0715e28b33
children 44a484f17f26
comparison
equal deleted inserted replaced
395:77c6123f49ee 396:8c092c042093
82 open _⊆_ 82 open _⊆_
83 83
84 power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A 84 power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A
85 power→⊆ A t PA∋t = record { incl = λ {x} t∋x → double-neg-eilm (t1 t∋x) } where 85 power→⊆ A t PA∋t = record { incl = λ {x} t∋x → double-neg-eilm (t1 t∋x) } where
86 t1 : {x : HOD } → t ∋ x → ¬ ¬ (A ∋ x) 86 t1 : {x : HOD } → t ∋ x → ¬ ¬ (A ∋ x)
87 t1 = zf.IsZF.power→ isZF A t PA∋t 87 t1 = power→ A t PA∋t
88 88
89 OrdP : ( x : Ordinal ) ( y : HOD ) → Dec ( Ord x ∋ y ) 89 OrdP : ( x : Ordinal ) ( y : HOD ) → Dec ( Ord x ∋ y )
90 OrdP x y with trio< x (od→ord y) 90 OrdP x y with trio< x (od→ord y)
91 OrdP x y | tri< a ¬b ¬c = no ¬c 91 OrdP x y | tri< a ¬b ¬c = no ¬c
92 OrdP x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl ) 92 OrdP x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl )