ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  omp1eomlem GIF version

Theorem omp1eomlem 7083
Description: Lemma for omp1eom 7084. (Contributed by Jim Kingdon, 11-Jul-2023.)
Hypotheses
Ref Expression
omp1eom.f 𝐹 = (𝑥 ∈ ω ↦ if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)))
omp1eom.s 𝑆 = (𝑥 ∈ ω ↦ suc 𝑥)
omp1eom.g 𝐺 = case(𝑆, ( I ↾ 1o))
Assertion
Ref Expression
omp1eomlem 𝐹:ω–1-1-onto→(ω ⊔ 1o)
Distinct variable group:   𝑥,𝐺
Allowed substitution hints:   𝑆(𝑥)   𝐹(𝑥)

Proof of Theorem omp1eomlem
Dummy variables 𝑧 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 omp1eom.f . . 3 𝐹 = (𝑥 ∈ ω ↦ if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)))
2 el1o 6428 . . . . . . 7 (𝑥 ∈ 1o𝑥 = ∅)
32biimpri 133 . . . . . 6 (𝑥 = ∅ → 𝑥 ∈ 1o)
43adantl 277 . . . . 5 (((⊤ ∧ 𝑥 ∈ ω) ∧ 𝑥 = ∅) → 𝑥 ∈ 1o)
5 djurcl 7041 . . . . 5 (𝑥 ∈ 1o → (inr‘𝑥) ∈ (ω ⊔ 1o))
64, 5syl 14 . . . 4 (((⊤ ∧ 𝑥 ∈ ω) ∧ 𝑥 = ∅) → (inr‘𝑥) ∈ (ω ⊔ 1o))
7 nnpredcl 4616 . . . . . 6 (𝑥 ∈ ω → 𝑥 ∈ ω)
87ad2antlr 489 . . . . 5 (((⊤ ∧ 𝑥 ∈ ω) ∧ ¬ 𝑥 = ∅) → 𝑥 ∈ ω)
9 djulcl 7040 . . . . 5 ( 𝑥 ∈ ω → (inl‘ 𝑥) ∈ (ω ⊔ 1o))
108, 9syl 14 . . . 4 (((⊤ ∧ 𝑥 ∈ ω) ∧ ¬ 𝑥 = ∅) → (inl‘ 𝑥) ∈ (ω ⊔ 1o))
11 nndceq0 4611 . . . . 5 (𝑥 ∈ ω → DECID 𝑥 = ∅)
1211adantl 277 . . . 4 ((⊤ ∧ 𝑥 ∈ ω) → DECID 𝑥 = ∅)
136, 10, 12ifcldadc 3561 . . 3 ((⊤ ∧ 𝑥 ∈ ω) → if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) ∈ (ω ⊔ 1o))
14 omp1eom.s . . . . . . . 8 𝑆 = (𝑥 ∈ ω ↦ suc 𝑥)
15 peano2 4588 . . . . . . . 8 (𝑥 ∈ ω → suc 𝑥 ∈ ω)
1614, 15fmpti 5660 . . . . . . 7 𝑆:ω⟶ω
1716a1i 9 . . . . . 6 (⊤ → 𝑆:ω⟶ω)
18 f1oi 5491 . . . . . . . . 9 ( I ↾ 1o):1o1-1-onto→1o
19 f1of 5453 . . . . . . . . 9 (( I ↾ 1o):1o1-1-onto→1o → ( I ↾ 1o):1o⟶1o)
2018, 19ax-mp 5 . . . . . . . 8 ( I ↾ 1o):1o⟶1o
21 1onn 6511 . . . . . . . . 9 1o ∈ ω
22 omelon 4602 . . . . . . . . . 10 ω ∈ On
2322onelssi 4423 . . . . . . . . 9 (1o ∈ ω → 1o ⊆ ω)
2421, 23ax-mp 5 . . . . . . . 8 1o ⊆ ω
25 fss 5369 . . . . . . . 8 ((( I ↾ 1o):1o⟶1o ∧ 1o ⊆ ω) → ( I ↾ 1o):1o⟶ω)
2620, 24, 25mp2an 426 . . . . . . 7 ( I ↾ 1o):1o⟶ω
2726a1i 9 . . . . . 6 (⊤ → ( I ↾ 1o):1o⟶ω)
2817, 27casef 7077 . . . . 5 (⊤ → case(𝑆, ( I ↾ 1o)):(ω ⊔ 1o)⟶ω)
29 omp1eom.g . . . . . 6 𝐺 = case(𝑆, ( I ↾ 1o))
3029feq1i 5350 . . . . 5 (𝐺:(ω ⊔ 1o)⟶ω ↔ case(𝑆, ( I ↾ 1o)):(ω ⊔ 1o)⟶ω)
3128, 30sylibr 134 . . . 4 (⊤ → 𝐺:(ω ⊔ 1o)⟶ω)
3231ffvelcdmda 5643 . . 3 ((⊤ ∧ 𝑦 ∈ (ω ⊔ 1o)) → (𝐺𝑦) ∈ ω)
33 ffn 5357 . . . . . . . . . . . . . . . 16 (𝑆:ω⟶ω → 𝑆 Fn ω)
3416, 33mp1i 10 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → 𝑆 Fn ω)
35 ffun 5360 . . . . . . . . . . . . . . . 16 (( I ↾ 1o):1o⟶1o → Fun ( I ↾ 1o))
3620, 35mp1i 10 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → Fun ( I ↾ 1o))
37 simpl 109 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → 𝑧 ∈ ω)
3834, 36, 37caseinl 7080 . . . . . . . . . . . . . 14 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → (case(𝑆, ( I ↾ 1o))‘(inl‘𝑧)) = (𝑆𝑧))
3929eqcomi 2179 . . . . . . . . . . . . . . . 16 case(𝑆, ( I ↾ 1o)) = 𝐺
4039a1i 9 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → case(𝑆, ( I ↾ 1o)) = 𝐺)
41 simpr 110 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → 𝑦 = (inl‘𝑧))
4241eqcomd 2181 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → (inl‘𝑧) = 𝑦)
4340, 42fveq12d 5514 . . . . . . . . . . . . . 14 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → (case(𝑆, ( I ↾ 1o))‘(inl‘𝑧)) = (𝐺𝑦))
44 peano2 4588 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ω → suc 𝑧 ∈ ω)
45 suceq 4396 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑧 → suc 𝑥 = suc 𝑧)
4645, 14fvmptg 5584 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ ω ∧ suc 𝑧 ∈ ω) → (𝑆𝑧) = suc 𝑧)
4744, 46mpdan 421 . . . . . . . . . . . . . . 15 (𝑧 ∈ ω → (𝑆𝑧) = suc 𝑧)
4847adantr 276 . . . . . . . . . . . . . 14 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → (𝑆𝑧) = suc 𝑧)
4938, 43, 483eqtr3d 2216 . . . . . . . . . . . . 13 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → (𝐺𝑦) = suc 𝑧)
50 peano3 4589 . . . . . . . . . . . . . 14 (𝑧 ∈ ω → suc 𝑧 ≠ ∅)
5150adantr 276 . . . . . . . . . . . . 13 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → suc 𝑧 ≠ ∅)
5249, 51eqnetrd 2369 . . . . . . . . . . . 12 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → (𝐺𝑦) ≠ ∅)
5352adantl 277 . . . . . . . . . . 11 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (𝐺𝑦) ≠ ∅)
5453necomd 2431 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → ∅ ≠ (𝐺𝑦))
5554neneqd 2366 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → ¬ ∅ = (𝐺𝑦))
56 simplr 528 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → 𝑥 = ∅)
5756eqeq1d 2184 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (𝑥 = (𝐺𝑦) ↔ ∅ = (𝐺𝑦)))
5855, 57mtbird 673 . . . . . . . 8 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → ¬ 𝑥 = (𝐺𝑦))
59 djune 7067 . . . . . . . . . . . 12 ((𝑧 ∈ V ∧ 𝑥 ∈ V) → (inl‘𝑧) ≠ (inr‘𝑥))
6059elvd 2740 . . . . . . . . . . 11 (𝑧 ∈ V → (inl‘𝑧) ≠ (inr‘𝑥))
6160elv 2739 . . . . . . . . . 10 (inl‘𝑧) ≠ (inr‘𝑥)
6261neii 2347 . . . . . . . . 9 ¬ (inl‘𝑧) = (inr‘𝑥)
63 simprr 531 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → 𝑦 = (inl‘𝑧))
64 simpr 110 . . . . . . . . . . . 12 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) → 𝑥 = ∅)
6564iftrued 3539 . . . . . . . . . . 11 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) → if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) = (inr‘𝑥))
6665adantr 276 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) = (inr‘𝑥))
6763, 66eqeq12d 2190 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) ↔ (inl‘𝑧) = (inr‘𝑥)))
6862, 67mtbiri 675 . . . . . . . 8 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → ¬ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)))
6958, 682falsed 702 . . . . . . 7 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥))))
7069rexlimdvaa 2593 . . . . . 6 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) → (∃𝑧 ∈ ω 𝑦 = (inl‘𝑧) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)))))
71 simplr 528 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → 𝑥 = ∅)
7229a1i 9 . . . . . . . . . . . 12 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → 𝐺 = case(𝑆, ( I ↾ 1o)))
73 simpr 110 . . . . . . . . . . . 12 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → 𝑦 = (inr‘𝑧))
7472, 73fveq12d 5514 . . . . . . . . . . 11 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → (𝐺𝑦) = (case(𝑆, ( I ↾ 1o))‘(inr‘𝑧)))
7514funmpt2 5247 . . . . . . . . . . . . . 14 Fun 𝑆
7675a1i 9 . . . . . . . . . . . . 13 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → Fun 𝑆)
77 fnresi 5325 . . . . . . . . . . . . . 14 ( I ↾ 1o) Fn 1o
7877a1i 9 . . . . . . . . . . . . 13 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → ( I ↾ 1o) Fn 1o)
79 simpl 109 . . . . . . . . . . . . 13 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → 𝑧 ∈ 1o)
8076, 78, 79caseinr 7081 . . . . . . . . . . . 12 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → (case(𝑆, ( I ↾ 1o))‘(inr‘𝑧)) = (( I ↾ 1o)‘𝑧))
81 fvresi 5701 . . . . . . . . . . . . 13 (𝑧 ∈ 1o → (( I ↾ 1o)‘𝑧) = 𝑧)
8281adantr 276 . . . . . . . . . . . 12 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → (( I ↾ 1o)‘𝑧) = 𝑧)
8380, 82eqtrd 2208 . . . . . . . . . . 11 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → (case(𝑆, ( I ↾ 1o))‘(inr‘𝑧)) = 𝑧)
84 el1o 6428 . . . . . . . . . . . 12 (𝑧 ∈ 1o𝑧 = ∅)
8579, 84sylib 122 . . . . . . . . . . 11 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → 𝑧 = ∅)
8674, 83, 853eqtrd 2212 . . . . . . . . . 10 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → (𝐺𝑦) = ∅)
8786adantl 277 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → (𝐺𝑦) = ∅)
8871, 87eqtr4d 2211 . . . . . . . 8 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → 𝑥 = (𝐺𝑦))
8985adantl 277 . . . . . . . . . . 11 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → 𝑧 = ∅)
9071, 89eqtr4d 2211 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → 𝑥 = 𝑧)
9190fveq2d 5511 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → (inr‘𝑥) = (inr‘𝑧))
9265adantr 276 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) = (inr‘𝑥))
93 simprr 531 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → 𝑦 = (inr‘𝑧))
9491, 92, 933eqtr4rd 2219 . . . . . . . 8 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)))
9588, 942thd 175 . . . . . . 7 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥))))
9695rexlimdvaa 2593 . . . . . 6 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) → (∃𝑧 ∈ 1o 𝑦 = (inr‘𝑧) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)))))
97 djur 7058 . . . . . . . 8 (𝑦 ∈ (ω ⊔ 1o) ↔ (∃𝑧 ∈ ω 𝑦 = (inl‘𝑧) ∨ ∃𝑧 ∈ 1o 𝑦 = (inr‘𝑧)))
9897biimpi 120 . . . . . . 7 (𝑦 ∈ (ω ⊔ 1o) → (∃𝑧 ∈ ω 𝑦 = (inl‘𝑧) ∨ ∃𝑧 ∈ 1o 𝑦 = (inr‘𝑧)))
9998ad2antlr 489 . . . . . 6 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) → (∃𝑧 ∈ ω 𝑦 = (inl‘𝑧) ∨ ∃𝑧 ∈ 1o 𝑦 = (inr‘𝑧)))
10070, 96, 99mpjaod 718 . . . . 5 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥))))
101 simplll 533 . . . . . . . . . . 11 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → 𝑥 ∈ ω)
102 simplr 528 . . . . . . . . . . . 12 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → ¬ 𝑥 = ∅)
103102neqned 2352 . . . . . . . . . . 11 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → 𝑥 ≠ ∅)
104 nnsucpred 4610 . . . . . . . . . . 11 ((𝑥 ∈ ω ∧ 𝑥 ≠ ∅) → suc 𝑥 = 𝑥)
105101, 103, 104syl2anc 411 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → suc 𝑥 = 𝑥)
106105eqeq2d 2187 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (suc 𝑧 = suc 𝑥 ↔ suc 𝑧 = 𝑥))
107 eqcom 2177 . . . . . . . . 9 (suc 𝑧 = 𝑥𝑥 = suc 𝑧)
108106, 107bitrdi 196 . . . . . . . 8 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (suc 𝑧 = suc 𝑥𝑥 = suc 𝑧))
109 simprr 531 . . . . . . . . . . 11 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → 𝑦 = (inl‘𝑧))
110 simpr 110 . . . . . . . . . . . . 13 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) → ¬ 𝑥 = ∅)
111110iffalsed 3542 . . . . . . . . . . . 12 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) → if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) = (inl‘ 𝑥))
112111adantr 276 . . . . . . . . . . 11 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) = (inl‘ 𝑥))
113109, 112eqeq12d 2190 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) ↔ (inl‘𝑧) = (inl‘ 𝑥)))
114 vuniex 4432 . . . . . . . . . . . 12 𝑥 ∈ V
115 inl11 7054 . . . . . . . . . . . 12 ((𝑧 ∈ V ∧ 𝑥 ∈ V) → ((inl‘𝑧) = (inl‘ 𝑥) ↔ 𝑧 = 𝑥))
116114, 115mpan2 425 . . . . . . . . . . 11 (𝑧 ∈ V → ((inl‘𝑧) = (inl‘ 𝑥) ↔ 𝑧 = 𝑥))
117116elv 2739 . . . . . . . . . 10 ((inl‘𝑧) = (inl‘ 𝑥) ↔ 𝑧 = 𝑥)
118113, 117bitrdi 196 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) ↔ 𝑧 = 𝑥))
119 nnon 4603 . . . . . . . . . . 11 (𝑧 ∈ ω → 𝑧 ∈ On)
120119ad2antrl 490 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → 𝑧 ∈ On)
1217ad3antrrr 492 . . . . . . . . . . 11 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → 𝑥 ∈ ω)
122 nnon 4603 . . . . . . . . . . 11 ( 𝑥 ∈ ω → 𝑥 ∈ On)
123121, 122syl 14 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → 𝑥 ∈ On)
124 suc11 4551 . . . . . . . . . 10 ((𝑧 ∈ On ∧ 𝑥 ∈ On) → (suc 𝑧 = suc 𝑥𝑧 = 𝑥))
125120, 123, 124syl2anc 411 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (suc 𝑧 = suc 𝑥𝑧 = 𝑥))
126118, 125bitr4d 191 . . . . . . . 8 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) ↔ suc 𝑧 = suc 𝑥))
12749adantl 277 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (𝐺𝑦) = suc 𝑧)
128127eqeq2d 2187 . . . . . . . 8 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (𝑥 = (𝐺𝑦) ↔ 𝑥 = suc 𝑧))
129108, 126, 1283bitr4rd 221 . . . . . . 7 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥))))
130129rexlimdvaa 2593 . . . . . 6 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) → (∃𝑧 ∈ ω 𝑦 = (inl‘𝑧) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)))))
131 simplr 528 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → ¬ 𝑥 = ∅)
13286adantl 277 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → (𝐺𝑦) = ∅)
133132eqeq2d 2187 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → (𝑥 = (𝐺𝑦) ↔ 𝑥 = ∅))
134131, 133mtbird 673 . . . . . . . 8 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → ¬ 𝑥 = (𝐺𝑦))
135 djune 7067 . . . . . . . . . . . 12 (( 𝑥 ∈ V ∧ 𝑧 ∈ V) → (inl‘ 𝑥) ≠ (inr‘𝑧))
136135elvd 2740 . . . . . . . . . . 11 ( 𝑥 ∈ V → (inl‘ 𝑥) ≠ (inr‘𝑧))
137114, 136ax-mp 5 . . . . . . . . . 10 (inl‘ 𝑥) ≠ (inr‘𝑧)
138137nesymi 2391 . . . . . . . . 9 ¬ (inr‘𝑧) = (inl‘ 𝑥)
13973, 111eqeqan12rd 2192 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → (𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) ↔ (inr‘𝑧) = (inl‘ 𝑥)))
140138, 139mtbiri 675 . . . . . . . 8 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → ¬ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)))
141134, 1402falsed 702 . . . . . . 7 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥))))
142141rexlimdvaa 2593 . . . . . 6 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) → (∃𝑧 ∈ 1o 𝑦 = (inr‘𝑧) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)))))
14398ad2antlr 489 . . . . . 6 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) → (∃𝑧 ∈ ω 𝑦 = (inl‘𝑧) ∨ ∃𝑧 ∈ 1o 𝑦 = (inr‘𝑧)))
144130, 142, 143mpjaod 718 . . . . 5 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥))))
145 exmiddc 836 . . . . . . 7 (DECID 𝑥 = ∅ → (𝑥 = ∅ ∨ ¬ 𝑥 = ∅))
14611, 145syl 14 . . . . . 6 (𝑥 ∈ ω → (𝑥 = ∅ ∨ ¬ 𝑥 = ∅))
147146adantr 276 . . . . 5 ((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) → (𝑥 = ∅ ∨ ¬ 𝑥 = ∅))
148100, 144, 147mpjaodan 798 . . . 4 ((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥))))
149148adantl 277 . . 3 ((⊤ ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o))) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥))))
1501, 13, 32, 149f1o2d 6066 . 2 (⊤ → 𝐹:ω–1-1-onto→(ω ⊔ 1o))
151150mptru 1362 1 𝐹:ω–1-1-onto→(ω ⊔ 1o)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wa 104  wb 105  wo 708  DECID wdc 834   = wceq 1353  wtru 1354  wcel 2146  wne 2345  wrex 2454  Vcvv 2735  wss 3127  c0 3420  ifcif 3532   cuni 3805  cmpt 4059   I cid 4282  Oncon0 4357  suc csuc 4359  ωcom 4583  cres 4622  Fun wfun 5202   Fn wfn 5203  wf 5204  1-1-ontowf1o 5207  cfv 5208  1oc1o 6400  cdju 7026  inlcinl 7034  inrcinr 7035  casecdjucase 7072
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-13 2148  ax-14 2149  ax-ext 2157  ax-sep 4116  ax-nul 4124  ax-pow 4169  ax-pr 4203  ax-un 4427  ax-setind 4530  ax-iinf 4581
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1459  df-sb 1761  df-eu 2027  df-mo 2028  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ne 2346  df-ral 2458  df-rex 2459  df-rab 2462  df-v 2737  df-sbc 2961  df-csb 3056  df-dif 3129  df-un 3131  df-in 3133  df-ss 3140  df-nul 3421  df-if 3533  df-pw 3574  df-sn 3595  df-pr 3596  df-op 3598  df-uni 3806  df-int 3841  df-br 3999  df-opab 4060  df-mpt 4061  df-tr 4097  df-id 4287  df-iord 4360  df-on 4362  df-suc 4365  df-iom 4584  df-xp 4626  df-rel 4627  df-cnv 4628  df-co 4629  df-dm 4630  df-rn 4631  df-res 4632  df-ima 4633  df-iota 5170  df-fun 5210  df-fn 5211  df-f 5212  df-f1 5213  df-fo 5214  df-f1o 5215  df-fv 5216  df-1st 6131  df-2nd 6132  df-1o 6407  df-dju 7027  df-inl 7036  df-inr 7037  df-case 7073
This theorem is referenced by:  omp1eom  7084
  Copyright terms: Public domain W3C validator