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

Theorem omp1eomlem 6987
Description: Lemma for omp1eom 6988. (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 6342 . . . . . . 7 (𝑥 ∈ 1o𝑥 = ∅)
32biimpri 132 . . . . . 6 (𝑥 = ∅ → 𝑥 ∈ 1o)
43adantl 275 . . . . 5 (((⊤ ∧ 𝑥 ∈ ω) ∧ 𝑥 = ∅) → 𝑥 ∈ 1o)
5 djurcl 6945 . . . . 5 (𝑥 ∈ 1o → (inr‘𝑥) ∈ (ω ⊔ 1o))
64, 5syl 14 . . . 4 (((⊤ ∧ 𝑥 ∈ ω) ∧ 𝑥 = ∅) → (inr‘𝑥) ∈ (ω ⊔ 1o))
7 nnpredcl 4544 . . . . . 6 (𝑥 ∈ ω → 𝑥 ∈ ω)
87ad2antlr 481 . . . . 5 (((⊤ ∧ 𝑥 ∈ ω) ∧ ¬ 𝑥 = ∅) → 𝑥 ∈ ω)
9 djulcl 6944 . . . . 5 ( 𝑥 ∈ ω → (inl‘ 𝑥) ∈ (ω ⊔ 1o))
108, 9syl 14 . . . 4 (((⊤ ∧ 𝑥 ∈ ω) ∧ ¬ 𝑥 = ∅) → (inl‘ 𝑥) ∈ (ω ⊔ 1o))
11 nndceq0 4539 . . . . 5 (𝑥 ∈ ω → DECID 𝑥 = ∅)
1211adantl 275 . . . 4 ((⊤ ∧ 𝑥 ∈ ω) → DECID 𝑥 = ∅)
136, 10, 12ifcldadc 3506 . . 3 ((⊤ ∧ 𝑥 ∈ ω) → if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) ∈ (ω ⊔ 1o))
14 omp1eom.s . . . . . . . 8 𝑆 = (𝑥 ∈ ω ↦ suc 𝑥)
15 peano2 4517 . . . . . . . 8 (𝑥 ∈ ω → suc 𝑥 ∈ ω)
1614, 15fmpti 5580 . . . . . . 7 𝑆:ω⟶ω
1716a1i 9 . . . . . 6 (⊤ → 𝑆:ω⟶ω)
18 f1oi 5413 . . . . . . . . 9 ( I ↾ 1o):1o1-1-onto→1o
19 f1of 5375 . . . . . . . . 9 (( I ↾ 1o):1o1-1-onto→1o → ( I ↾ 1o):1o⟶1o)
2018, 19ax-mp 5 . . . . . . . 8 ( I ↾ 1o):1o⟶1o
21 1onn 6424 . . . . . . . . 9 1o ∈ ω
22 omelon 4530 . . . . . . . . . 10 ω ∈ On
2322onelssi 4359 . . . . . . . . 9 (1o ∈ ω → 1o ⊆ ω)
2421, 23ax-mp 5 . . . . . . . 8 1o ⊆ ω
25 fss 5292 . . . . . . . 8 ((( I ↾ 1o):1o⟶1o ∧ 1o ⊆ ω) → ( I ↾ 1o):1o⟶ω)
2620, 24, 25mp2an 423 . . . . . . 7 ( I ↾ 1o):1o⟶ω
2726a1i 9 . . . . . 6 (⊤ → ( I ↾ 1o):1o⟶ω)
2817, 27casef 6981 . . . . 5 (⊤ → case(𝑆, ( I ↾ 1o)):(ω ⊔ 1o)⟶ω)
29 omp1eom.g . . . . . 6 𝐺 = case(𝑆, ( I ↾ 1o))
3029feq1i 5273 . . . . 5 (𝐺:(ω ⊔ 1o)⟶ω ↔ case(𝑆, ( I ↾ 1o)):(ω ⊔ 1o)⟶ω)
3128, 30sylibr 133 . . . 4 (⊤ → 𝐺:(ω ⊔ 1o)⟶ω)
3231ffvelrnda 5563 . . 3 ((⊤ ∧ 𝑦 ∈ (ω ⊔ 1o)) → (𝐺𝑦) ∈ ω)
33 ffn 5280 . . . . . . . . . . . . . . . 16 (𝑆:ω⟶ω → 𝑆 Fn ω)
3416, 33mp1i 10 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → 𝑆 Fn ω)
35 ffun 5283 . . . . . . . . . . . . . . . 16 (( I ↾ 1o):1o⟶1o → Fun ( I ↾ 1o))
3620, 35mp1i 10 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → Fun ( I ↾ 1o))
37 simpl 108 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → 𝑧 ∈ ω)
3834, 36, 37caseinl 6984 . . . . . . . . . . . . . 14 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → (case(𝑆, ( I ↾ 1o))‘(inl‘𝑧)) = (𝑆𝑧))
3929eqcomi 2144 . . . . . . . . . . . . . . . 16 case(𝑆, ( I ↾ 1o)) = 𝐺
4039a1i 9 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → case(𝑆, ( I ↾ 1o)) = 𝐺)
41 simpr 109 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → 𝑦 = (inl‘𝑧))
4241eqcomd 2146 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → (inl‘𝑧) = 𝑦)
4340, 42fveq12d 5436 . . . . . . . . . . . . . 14 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → (case(𝑆, ( I ↾ 1o))‘(inl‘𝑧)) = (𝐺𝑦))
44 peano2 4517 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ω → suc 𝑧 ∈ ω)
45 suceq 4332 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑧 → suc 𝑥 = suc 𝑧)
4645, 14fvmptg 5505 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ ω ∧ suc 𝑧 ∈ ω) → (𝑆𝑧) = suc 𝑧)
4744, 46mpdan 418 . . . . . . . . . . . . . . 15 (𝑧 ∈ ω → (𝑆𝑧) = suc 𝑧)
4847adantr 274 . . . . . . . . . . . . . 14 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → (𝑆𝑧) = suc 𝑧)
4938, 43, 483eqtr3d 2181 . . . . . . . . . . . . 13 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → (𝐺𝑦) = suc 𝑧)
50 peano3 4518 . . . . . . . . . . . . . 14 (𝑧 ∈ ω → suc 𝑧 ≠ ∅)
5150adantr 274 . . . . . . . . . . . . 13 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → suc 𝑧 ≠ ∅)
5249, 51eqnetrd 2333 . . . . . . . . . . . 12 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → (𝐺𝑦) ≠ ∅)
5352adantl 275 . . . . . . . . . . 11 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (𝐺𝑦) ≠ ∅)
5453necomd 2395 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → ∅ ≠ (𝐺𝑦))
5554neneqd 2330 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → ¬ ∅ = (𝐺𝑦))
56 simplr 520 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → 𝑥 = ∅)
5756eqeq1d 2149 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (𝑥 = (𝐺𝑦) ↔ ∅ = (𝐺𝑦)))
5855, 57mtbird 663 . . . . . . . 8 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → ¬ 𝑥 = (𝐺𝑦))
59 djune 6971 . . . . . . . . . . . 12 ((𝑧 ∈ V ∧ 𝑥 ∈ V) → (inl‘𝑧) ≠ (inr‘𝑥))
6059elvd 2694 . . . . . . . . . . 11 (𝑧 ∈ V → (inl‘𝑧) ≠ (inr‘𝑥))
6160elv 2693 . . . . . . . . . 10 (inl‘𝑧) ≠ (inr‘𝑥)
6261neii 2311 . . . . . . . . 9 ¬ (inl‘𝑧) = (inr‘𝑥)
63 simprr 522 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → 𝑦 = (inl‘𝑧))
64 simpr 109 . . . . . . . . . . . 12 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) → 𝑥 = ∅)
6564iftrued 3486 . . . . . . . . . . 11 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) → if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) = (inr‘𝑥))
6665adantr 274 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) = (inr‘𝑥))
6763, 66eqeq12d 2155 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) ↔ (inl‘𝑧) = (inr‘𝑥)))
6862, 67mtbiri 665 . . . . . . . 8 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → ¬ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)))
6958, 682falsed 692 . . . . . . 7 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥))))
7069rexlimdvaa 2553 . . . . . 6 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) → (∃𝑧 ∈ ω 𝑦 = (inl‘𝑧) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)))))
71 simplr 520 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → 𝑥 = ∅)
7229a1i 9 . . . . . . . . . . . 12 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → 𝐺 = case(𝑆, ( I ↾ 1o)))
73 simpr 109 . . . . . . . . . . . 12 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → 𝑦 = (inr‘𝑧))
7472, 73fveq12d 5436 . . . . . . . . . . 11 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → (𝐺𝑦) = (case(𝑆, ( I ↾ 1o))‘(inr‘𝑧)))
7514funmpt2 5170 . . . . . . . . . . . . . 14 Fun 𝑆
7675a1i 9 . . . . . . . . . . . . 13 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → Fun 𝑆)
77 fnresi 5248 . . . . . . . . . . . . . 14 ( I ↾ 1o) Fn 1o
7877a1i 9 . . . . . . . . . . . . 13 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → ( I ↾ 1o) Fn 1o)
79 simpl 108 . . . . . . . . . . . . 13 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → 𝑧 ∈ 1o)
8076, 78, 79caseinr 6985 . . . . . . . . . . . 12 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → (case(𝑆, ( I ↾ 1o))‘(inr‘𝑧)) = (( I ↾ 1o)‘𝑧))
81 fvresi 5621 . . . . . . . . . . . . 13 (𝑧 ∈ 1o → (( I ↾ 1o)‘𝑧) = 𝑧)
8281adantr 274 . . . . . . . . . . . 12 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → (( I ↾ 1o)‘𝑧) = 𝑧)
8380, 82eqtrd 2173 . . . . . . . . . . 11 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → (case(𝑆, ( I ↾ 1o))‘(inr‘𝑧)) = 𝑧)
84 el1o 6342 . . . . . . . . . . . 12 (𝑧 ∈ 1o𝑧 = ∅)
8579, 84sylib 121 . . . . . . . . . . 11 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → 𝑧 = ∅)
8674, 83, 853eqtrd 2177 . . . . . . . . . 10 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → (𝐺𝑦) = ∅)
8786adantl 275 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → (𝐺𝑦) = ∅)
8871, 87eqtr4d 2176 . . . . . . . 8 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → 𝑥 = (𝐺𝑦))
8985adantl 275 . . . . . . . . . . 11 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → 𝑧 = ∅)
9071, 89eqtr4d 2176 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → 𝑥 = 𝑧)
9190fveq2d 5433 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → (inr‘𝑥) = (inr‘𝑧))
9265adantr 274 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) = (inr‘𝑥))
93 simprr 522 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → 𝑦 = (inr‘𝑧))
9491, 92, 933eqtr4rd 2184 . . . . . . . 8 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)))
9588, 942thd 174 . . . . . . 7 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥))))
9695rexlimdvaa 2553 . . . . . 6 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) → (∃𝑧 ∈ 1o 𝑦 = (inr‘𝑧) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)))))
97 djur 6962 . . . . . . . 8 (𝑦 ∈ (ω ⊔ 1o) ↔ (∃𝑧 ∈ ω 𝑦 = (inl‘𝑧) ∨ ∃𝑧 ∈ 1o 𝑦 = (inr‘𝑧)))
9897biimpi 119 . . . . . . 7 (𝑦 ∈ (ω ⊔ 1o) → (∃𝑧 ∈ ω 𝑦 = (inl‘𝑧) ∨ ∃𝑧 ∈ 1o 𝑦 = (inr‘𝑧)))
9998ad2antlr 481 . . . . . 6 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) → (∃𝑧 ∈ ω 𝑦 = (inl‘𝑧) ∨ ∃𝑧 ∈ 1o 𝑦 = (inr‘𝑧)))
10070, 96, 99mpjaod 708 . . . . 5 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥))))
101 simplll 523 . . . . . . . . . . 11 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → 𝑥 ∈ ω)
102 simplr 520 . . . . . . . . . . . 12 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → ¬ 𝑥 = ∅)
103102neqned 2316 . . . . . . . . . . 11 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → 𝑥 ≠ ∅)
104 nnsucpred 4538 . . . . . . . . . . 11 ((𝑥 ∈ ω ∧ 𝑥 ≠ ∅) → suc 𝑥 = 𝑥)
105101, 103, 104syl2anc 409 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → suc 𝑥 = 𝑥)
106105eqeq2d 2152 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (suc 𝑧 = suc 𝑥 ↔ suc 𝑧 = 𝑥))
107 eqcom 2142 . . . . . . . . 9 (suc 𝑧 = 𝑥𝑥 = suc 𝑧)
108106, 107syl6bb 195 . . . . . . . 8 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (suc 𝑧 = suc 𝑥𝑥 = suc 𝑧))
109 simprr 522 . . . . . . . . . . 11 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → 𝑦 = (inl‘𝑧))
110 simpr 109 . . . . . . . . . . . . 13 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) → ¬ 𝑥 = ∅)
111110iffalsed 3489 . . . . . . . . . . . 12 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) → if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) = (inl‘ 𝑥))
112111adantr 274 . . . . . . . . . . 11 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) = (inl‘ 𝑥))
113109, 112eqeq12d 2155 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) ↔ (inl‘𝑧) = (inl‘ 𝑥)))
114 vuniex 4368 . . . . . . . . . . . 12 𝑥 ∈ V
115 inl11 6958 . . . . . . . . . . . 12 ((𝑧 ∈ V ∧ 𝑥 ∈ V) → ((inl‘𝑧) = (inl‘ 𝑥) ↔ 𝑧 = 𝑥))
116114, 115mpan2 422 . . . . . . . . . . 11 (𝑧 ∈ V → ((inl‘𝑧) = (inl‘ 𝑥) ↔ 𝑧 = 𝑥))
117116elv 2693 . . . . . . . . . 10 ((inl‘𝑧) = (inl‘ 𝑥) ↔ 𝑧 = 𝑥)
118113, 117syl6bb 195 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) ↔ 𝑧 = 𝑥))
119 nnon 4531 . . . . . . . . . . 11 (𝑧 ∈ ω → 𝑧 ∈ On)
120119ad2antrl 482 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → 𝑧 ∈ On)
1217ad3antrrr 484 . . . . . . . . . . 11 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → 𝑥 ∈ ω)
122 nnon 4531 . . . . . . . . . . 11 ( 𝑥 ∈ ω → 𝑥 ∈ On)
123121, 122syl 14 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → 𝑥 ∈ On)
124 suc11 4481 . . . . . . . . . 10 ((𝑧 ∈ On ∧ 𝑥 ∈ On) → (suc 𝑧 = suc 𝑥𝑧 = 𝑥))
125120, 123, 124syl2anc 409 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (suc 𝑧 = suc 𝑥𝑧 = 𝑥))
126118, 125bitr4d 190 . . . . . . . 8 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) ↔ suc 𝑧 = suc 𝑥))
12749adantl 275 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (𝐺𝑦) = suc 𝑧)
128127eqeq2d 2152 . . . . . . . 8 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (𝑥 = (𝐺𝑦) ↔ 𝑥 = suc 𝑧))
129108, 126, 1283bitr4rd 220 . . . . . . 7 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥))))
130129rexlimdvaa 2553 . . . . . 6 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) → (∃𝑧 ∈ ω 𝑦 = (inl‘𝑧) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)))))
131 simplr 520 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → ¬ 𝑥 = ∅)
13286adantl 275 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → (𝐺𝑦) = ∅)
133132eqeq2d 2152 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → (𝑥 = (𝐺𝑦) ↔ 𝑥 = ∅))
134131, 133mtbird 663 . . . . . . . 8 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → ¬ 𝑥 = (𝐺𝑦))
135 djune 6971 . . . . . . . . . . . 12 (( 𝑥 ∈ V ∧ 𝑧 ∈ V) → (inl‘ 𝑥) ≠ (inr‘𝑧))
136135elvd 2694 . . . . . . . . . . 11 ( 𝑥 ∈ V → (inl‘ 𝑥) ≠ (inr‘𝑧))
137114, 136ax-mp 5 . . . . . . . . . 10 (inl‘ 𝑥) ≠ (inr‘𝑧)
138137nesymi 2355 . . . . . . . . 9 ¬ (inr‘𝑧) = (inl‘ 𝑥)
13973, 111eqeqan12rd 2157 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → (𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) ↔ (inr‘𝑧) = (inl‘ 𝑥)))
140138, 139mtbiri 665 . . . . . . . 8 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → ¬ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)))
141134, 1402falsed 692 . . . . . . 7 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥))))
142141rexlimdvaa 2553 . . . . . 6 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) → (∃𝑧 ∈ 1o 𝑦 = (inr‘𝑧) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)))))
14398ad2antlr 481 . . . . . 6 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) → (∃𝑧 ∈ ω 𝑦 = (inl‘𝑧) ∨ ∃𝑧 ∈ 1o 𝑦 = (inr‘𝑧)))
144130, 142, 143mpjaod 708 . . . . 5 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥))))
145 exmiddc 822 . . . . . . 7 (DECID 𝑥 = ∅ → (𝑥 = ∅ ∨ ¬ 𝑥 = ∅))
14611, 145syl 14 . . . . . 6 (𝑥 ∈ ω → (𝑥 = ∅ ∨ ¬ 𝑥 = ∅))
147146adantr 274 . . . . 5 ((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) → (𝑥 = ∅ ∨ ¬ 𝑥 = ∅))
148100, 144, 147mpjaodan 788 . . . 4 ((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥))))
149148adantl 275 . . 3 ((⊤ ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o))) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥))))
1501, 13, 32, 149f1o2d 5983 . 2 (⊤ → 𝐹:ω–1-1-onto→(ω ⊔ 1o))
151150mptru 1341 1 𝐹:ω–1-1-onto→(ω ⊔ 1o)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wa 103  wb 104  wo 698  DECID wdc 820   = wceq 1332  wtru 1333  wcel 1481  wne 2309  wrex 2418  Vcvv 2689  wss 3076  c0 3368  ifcif 3479   cuni 3744  cmpt 3997   I cid 4218  Oncon0 4293  suc csuc 4295  ωcom 4512  cres 4549  Fun wfun 5125   Fn wfn 5126  wf 5127  1-1-ontowf1o 5130  cfv 5131  1oc1o 6314  cdju 6930  inlcinl 6938  inrcinr 6939  casecdjucase 6976
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4054  ax-nul 4062  ax-pow 4106  ax-pr 4139  ax-un 4363  ax-setind 4460  ax-iinf 4510
This theorem depends on definitions:  df-bi 116  df-dc 821  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-ral 2422  df-rex 2423  df-rab 2426  df-v 2691  df-sbc 2914  df-csb 3008  df-dif 3078  df-un 3080  df-in 3082  df-ss 3089  df-nul 3369  df-if 3480  df-pw 3517  df-sn 3538  df-pr 3539  df-op 3541  df-uni 3745  df-int 3780  df-br 3938  df-opab 3998  df-mpt 3999  df-tr 4035  df-id 4223  df-iord 4296  df-on 4298  df-suc 4301  df-iom 4513  df-xp 4553  df-rel 4554  df-cnv 4555  df-co 4556  df-dm 4557  df-rn 4558  df-res 4559  df-ima 4560  df-iota 5096  df-fun 5133  df-fn 5134  df-f 5135  df-f1 5136  df-fo 5137  df-f1o 5138  df-fv 5139  df-1st 6046  df-2nd 6047  df-1o 6321  df-dju 6931  df-inl 6940  df-inr 6941  df-case 6977
This theorem is referenced by:  omp1eom  6988
  Copyright terms: Public domain W3C validator