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

comparison src/ODC.agda @ 447:364d738f871d

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 Sun, 13 Mar 2022 14:44:24 +0900
parents a5f8084b8368
children 5acf6483a9e3
comparison
equal deleted inserted replaced
446:eb4049abad70 447:364d738f871d
93 power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A 93 power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A
94 power→⊆ A t PA∋t = record { incl = λ {x} t∋x → double-neg-eilm (t1 t∋x) } where 94 power→⊆ A t PA∋t = record { incl = λ {x} t∋x → double-neg-eilm (t1 t∋x) } where
95 t1 : {x : HOD } → t ∋ x → ¬ ¬ (A ∋ x) 95 t1 : {x : HOD } → t ∋ x → ¬ ¬ (A ∋ x)
96 t1 = power→ A t PA∋t 96 t1 = power→ A t PA∋t
97 97
98 power-∩ : { A x y : HOD } → Power A ∋ x → Power A ∋ y → Power A ∋ ( x ∩ y )
99 power-∩ {A} {x} {y} ax ay = power← A (x ∩ y) p01 where
100 p01 : {z : HOD} → (x ∩ y) ∋ z → A ∋ z
101 p01 {z} xyz = double-neg-eilm ( power→ A x ax (proj1 xyz ))
102
98 OrdP : ( x : Ordinal ) ( y : HOD ) → Dec ( Ord x ∋ y ) 103 OrdP : ( x : Ordinal ) ( y : HOD ) → Dec ( Ord x ∋ y )
99 OrdP x y with trio< x (& y) 104 OrdP x y with trio< x (& y)
100 OrdP x y | tri< a ¬b ¬c = no ¬c 105 OrdP x y | tri< a ¬b ¬c = no ¬c
101 OrdP x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl ) 106 OrdP x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl )
102 OrdP x y | tri> ¬a ¬b c = yes c 107 OrdP x y | tri> ¬a ¬b c = yes c