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

comparison BAlgbra.agda @ 424:cc7909f86841

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
remvoe TransFinifte1
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 01 Aug 2020 23:37:10 +0900
parents 9984cdd88da3
children
comparison
equal deleted inserted replaced
423:9984cdd88da3 424:cc7909f86841
2 open import Ordinals 2 open import Ordinals
3 module BAlgbra {n : Level } (O : Ordinals {n}) where 3 module BAlgbra {n : Level } (O : Ordinals {n}) where
4 4
5 open import zf 5 open import zf
6 open import logic 6 open import logic
7 import OrdUtil
7 import OD 8 import OD
9 import ODUtil
8 import ODC 10 import ODC
9 11
10 open import Relation.Nullary 12 open import Relation.Nullary
11 open import Relation.Binary 13 open import Relation.Binary
12 open import Data.Empty 14 open import Data.Empty
14 open import Relation.Binary.Core 16 open import Relation.Binary.Core
15 open import Relation.Binary.PropositionalEquality 17 open import Relation.Binary.PropositionalEquality
16 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ; _+_ to _n+_ ) 18 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ; _+_ to _n+_ )
17 19
18 open inOrdinal O 20 open inOrdinal O
21 open Ordinals.Ordinals O
22 open Ordinals.IsOrdinals isOrdinal
23 open Ordinals.IsNext isNext
24 open OrdUtil O
25 open ODUtil O
26
19 open OD O 27 open OD O
20 open OD.OD 28 open OD.OD
21 open ODAxiom odAxiom 29 open ODAxiom odAxiom
22 open HOD 30 open HOD
23 31
45 lemma1 {x} lt = lemma3 lt where 53 lemma1 {x} lt = lemma3 lt where
46 lemma4 : {y : Ordinal} → odef (A , B) y ∧ odef (* y) x → ¬ (¬ ( odef A x ∨ odef B x) ) 54 lemma4 : {y : Ordinal} → odef (A , B) y ∧ odef (* y) x → ¬ (¬ ( odef A x ∨ odef B x) )
47 lemma4 {y} z with proj1 z 55 lemma4 {y} z with proj1 z
48 lemma4 {y} z | case1 refl = double-neg (case1 ( subst (λ k → odef k x ) *iso (proj2 z)) ) 56 lemma4 {y} z | case1 refl = double-neg (case1 ( subst (λ k → odef k x ) *iso (proj2 z)) )
49 lemma4 {y} z | case2 refl = double-neg (case2 ( subst (λ k → odef k x ) *iso (proj2 z)) ) 57 lemma4 {y} z | case2 refl = double-neg (case2 ( subst (λ k → odef k x ) *iso (proj2 z)) )
50 lemma3 : (((u : Ordinals.ord O) → ¬ odef (A , B) u ∧ odef (* u) x) → ⊥) → odef (A ∪ B) x 58 lemma3 : (((u : Ordinal ) → ¬ odef (A , B) u ∧ odef (* u) x) → ⊥) → odef (A ∪ B) x
51 lemma3 not = ODC.double-neg-eilm O (FExists _ lemma4 not) -- choice 59 lemma3 not = ODC.double-neg-eilm O (FExists _ lemma4 not) -- choice
52 lemma2 : {x : Ordinal} → odef (A ∪ B) x → odef (Union (A , B)) x 60 lemma2 : {x : Ordinal} → odef (A ∪ B) x → odef (Union (A , B)) x
53 lemma2 {x} (case1 A∋x) = subst (λ k → odef (Union (A , B)) k) &iso ( IsZF.union→ isZF (A , B) (* x) A 61 lemma2 {x} (case1 A∋x) = subst (λ k → odef (Union (A , B)) k) &iso ( IsZF.union→ isZF (A , B) (* x) A
54 ⟪ case1 refl , d→∋ A A∋x ⟫ ) 62 ⟪ case1 refl , d→∋ A A∋x ⟫ )
55 lemma2 {x} (case2 B∋x) = subst (λ k → odef (Union (A , B)) k) &iso ( IsZF.union→ isZF (A , B) (* x) B 63 lemma2 {x} (case2 B∋x) = subst (λ k → odef (Union (A , B)) k) &iso ( IsZF.union→ isZF (A , B) (* x) B