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

Theorem omp1eomlem 7123
Description: Lemma for omp1eom 7124. (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 6462 . . . . . . 7 (𝑥 ∈ 1o𝑥 = ∅)
32biimpri 133 . . . . . 6 (𝑥 = ∅ → 𝑥 ∈ 1o)
43adantl 277 . . . . 5 (((⊤ ∧ 𝑥 ∈ ω) ∧ 𝑥 = ∅) → 𝑥 ∈ 1o)
5 djurcl 7081 . . . . 5 (𝑥 ∈ 1o → (inr‘𝑥) ∈ (ω ⊔ 1o))
64, 5syl 14 . . . 4 (((⊤ ∧ 𝑥 ∈ ω) ∧ 𝑥 = ∅) → (inr‘𝑥) ∈ (ω ⊔ 1o))
7 nnpredcl 4640 . . . . . 6 (𝑥 ∈ ω → 𝑥 ∈ ω)
87ad2antlr 489 . . . . 5 (((⊤ ∧ 𝑥 ∈ ω) ∧ ¬ 𝑥 = ∅) → 𝑥 ∈ ω)
9 djulcl 7080 . . . . 5 ( 𝑥 ∈ ω → (inl‘ 𝑥) ∈ (ω ⊔ 1o))
108, 9syl 14 . . . 4 (((⊤ ∧ 𝑥 ∈ ω) ∧ ¬ 𝑥 = ∅) → (inl‘ 𝑥) ∈ (ω ⊔ 1o))
11 nndceq0 4635 . . . . 5 (𝑥 ∈ ω → DECID 𝑥 = ∅)
1211adantl 277 . . . 4 ((⊤ ∧ 𝑥 ∈ ω) → DECID 𝑥 = ∅)
136, 10, 12ifcldadc 3578 . . 3 ((⊤ ∧ 𝑥 ∈ ω) → if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) ∈ (ω ⊔ 1o))
14 omp1eom.s . . . . . . . 8 𝑆 = (𝑥 ∈ ω ↦ suc 𝑥)
15 peano2 4612 . . . . . . . 8 (𝑥 ∈ ω → suc 𝑥 ∈ ω)
1614, 15fmpti 5689 . . . . . . 7 𝑆:ω⟶ω
1716a1i 9 . . . . . 6 (⊤ → 𝑆:ω⟶ω)
18 f1oi 5518 . . . . . . . . 9 ( I ↾ 1o):1o1-1-onto→1o
19 f1of 5480 . . . . . . . . 9 (( I ↾ 1o):1o1-1-onto→1o → ( I ↾ 1o):1o⟶1o)
2018, 19ax-mp 5 . . . . . . . 8 ( I ↾ 1o):1o⟶1o
21 1onn 6545 . . . . . . . . 9 1o ∈ ω
22 omelon 4626 . . . . . . . . . 10 ω ∈ On
2322onelssi 4447 . . . . . . . . 9 (1o ∈ ω → 1o ⊆ ω)
2421, 23ax-mp 5 . . . . . . . 8 1o ⊆ ω
25 fss 5396 . . . . . . . 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 7117 . . . . 5 (⊤ → case(𝑆, ( I ↾ 1o)):(ω ⊔ 1o)⟶ω)
29 omp1eom.g . . . . . 6 𝐺 = case(𝑆, ( I ↾ 1o))
3029feq1i 5377 . . . . 5 (𝐺:(ω ⊔ 1o)⟶ω ↔ case(𝑆, ( I ↾ 1o)):(ω ⊔ 1o)⟶ω)
3128, 30sylibr 134 . . . 4 (⊤ → 𝐺:(ω ⊔ 1o)⟶ω)
3231ffvelcdmda 5672 . . 3 ((⊤ ∧ 𝑦 ∈ (ω ⊔ 1o)) → (𝐺𝑦) ∈ ω)
33 ffn 5384 . . . . . . . . . . . . . . . 16 (𝑆:ω⟶ω → 𝑆 Fn ω)
3416, 33mp1i 10 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → 𝑆 Fn ω)
35 ffun 5387 . . . . . . . . . . . . . . . 16 (( I ↾ 1o):1o⟶1o → Fun ( I ↾ 1o))
3620, 35mp1i 10 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → Fun ( I ↾ 1o))
37 simpl 109 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → 𝑧 ∈ ω)
3834, 36, 37caseinl 7120 . . . . . . . . . . . . . 14 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → (case(𝑆, ( I ↾ 1o))‘(inl‘𝑧)) = (𝑆𝑧))
3929eqcomi 2193 . . . . . . . . . . . . . . . 16 case(𝑆, ( I ↾ 1o)) = 𝐺
4039a1i 9 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → case(𝑆, ( I ↾ 1o)) = 𝐺)
41 simpr 110 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → 𝑦 = (inl‘𝑧))
4241eqcomd 2195 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → (inl‘𝑧) = 𝑦)
4340, 42fveq12d 5541 . . . . . . . . . . . . . 14 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → (case(𝑆, ( I ↾ 1o))‘(inl‘𝑧)) = (𝐺𝑦))
44 peano2 4612 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ω → suc 𝑧 ∈ ω)
45 suceq 4420 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑧 → suc 𝑥 = suc 𝑧)
4645, 14fvmptg 5613 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ ω ∧ suc 𝑧 ∈ ω) → (𝑆𝑧) = suc 𝑧)
4744, 46mpdan 421 . . . . . . . . . . . . . . 15 (𝑧 ∈ ω → (𝑆𝑧) = suc 𝑧)
4847adantr 276 . . . . . . . . . . . . . 14 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → (𝑆𝑧) = suc 𝑧)
4938, 43, 483eqtr3d 2230 . . . . . . . . . . . . 13 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → (𝐺𝑦) = suc 𝑧)
50 peano3 4613 . . . . . . . . . . . . . 14 (𝑧 ∈ ω → suc 𝑧 ≠ ∅)
5150adantr 276 . . . . . . . . . . . . 13 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → suc 𝑧 ≠ ∅)
5249, 51eqnetrd 2384 . . . . . . . . . . . 12 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → (𝐺𝑦) ≠ ∅)
5352adantl 277 . . . . . . . . . . 11 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (𝐺𝑦) ≠ ∅)
5453necomd 2446 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → ∅ ≠ (𝐺𝑦))
5554neneqd 2381 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → ¬ ∅ = (𝐺𝑦))
56 simplr 528 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → 𝑥 = ∅)
5756eqeq1d 2198 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (𝑥 = (𝐺𝑦) ↔ ∅ = (𝐺𝑦)))
5855, 57mtbird 674 . . . . . . . 8 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → ¬ 𝑥 = (𝐺𝑦))
59 djune 7107 . . . . . . . . . . . 12 ((𝑧 ∈ V ∧ 𝑥 ∈ V) → (inl‘𝑧) ≠ (inr‘𝑥))
6059elvd 2757 . . . . . . . . . . 11 (𝑧 ∈ V → (inl‘𝑧) ≠ (inr‘𝑥))
6160elv 2756 . . . . . . . . . 10 (inl‘𝑧) ≠ (inr‘𝑥)
6261neii 2362 . . . . . . . . 9 ¬ (inl‘𝑧) = (inr‘𝑥)
63 simprr 531 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → 𝑦 = (inl‘𝑧))
64 simpr 110 . . . . . . . . . . . 12 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) → 𝑥 = ∅)
6564iftrued 3556 . . . . . . . . . . 11 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) → if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) = (inr‘𝑥))
6665adantr 276 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) = (inr‘𝑥))
6763, 66eqeq12d 2204 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) ↔ (inl‘𝑧) = (inr‘𝑥)))
6862, 67mtbiri 676 . . . . . . . 8 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → ¬ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)))
6958, 682falsed 703 . . . . . . 7 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥))))
7069rexlimdvaa 2608 . . . . . 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 5541 . . . . . . . . . . 11 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → (𝐺𝑦) = (case(𝑆, ( I ↾ 1o))‘(inr‘𝑧)))
7514funmpt2 5274 . . . . . . . . . . . . . 14 Fun 𝑆
7675a1i 9 . . . . . . . . . . . . 13 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → Fun 𝑆)
77 fnresi 5352 . . . . . . . . . . . . . 14 ( I ↾ 1o) Fn 1o
7877a1i 9 . . . . . . . . . . . . 13 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → ( I ↾ 1o) Fn 1o)
79 simpl 109 . . . . . . . . . . . . 13 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → 𝑧 ∈ 1o)
8076, 78, 79caseinr 7121 . . . . . . . . . . . 12 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → (case(𝑆, ( I ↾ 1o))‘(inr‘𝑧)) = (( I ↾ 1o)‘𝑧))
81 fvresi 5730 . . . . . . . . . . . . 13 (𝑧 ∈ 1o → (( I ↾ 1o)‘𝑧) = 𝑧)
8281adantr 276 . . . . . . . . . . . 12 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → (( I ↾ 1o)‘𝑧) = 𝑧)
8380, 82eqtrd 2222 . . . . . . . . . . 11 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → (case(𝑆, ( I ↾ 1o))‘(inr‘𝑧)) = 𝑧)
84 el1o 6462 . . . . . . . . . . . 12 (𝑧 ∈ 1o𝑧 = ∅)
8579, 84sylib 122 . . . . . . . . . . 11 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → 𝑧 = ∅)
8674, 83, 853eqtrd 2226 . . . . . . . . . 10 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → (𝐺𝑦) = ∅)
8786adantl 277 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → (𝐺𝑦) = ∅)
8871, 87eqtr4d 2225 . . . . . . . 8 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → 𝑥 = (𝐺𝑦))
8985adantl 277 . . . . . . . . . . 11 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → 𝑧 = ∅)
9071, 89eqtr4d 2225 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → 𝑥 = 𝑧)
9190fveq2d 5538 . . . . . . . . 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 2233 . . . . . . . 8 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)))
9588, 942thd 175 . . . . . . 7 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥))))
9695rexlimdvaa 2608 . . . . . 6 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) → (∃𝑧 ∈ 1o 𝑦 = (inr‘𝑧) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)))))
97 djur 7098 . . . . . . . 8 (𝑦 ∈ (ω ⊔ 1o) ↔ (∃𝑧 ∈ ω 𝑦 = (inl‘𝑧) ∨ ∃𝑧 ∈ 1o 𝑦 = (inr‘𝑧)))
9897biimpi 120 . . . . . . 7 (𝑦 ∈ (ω ⊔ 1o) → (∃𝑧 ∈ ω 𝑦 = (inl‘𝑧) ∨ ∃𝑧 ∈ 1o 𝑦 = (inr‘𝑧)))
9998ad2antlr 489 . . . . . 6 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) → (∃𝑧 ∈ ω 𝑦 = (inl‘𝑧) ∨ ∃𝑧 ∈ 1o 𝑦 = (inr‘𝑧)))
10070, 96, 99mpjaod 719 . . . . 5 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥))))
101 simplll 533 . . . . . . . . . . 11 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → 𝑥 ∈ ω)
102 simplr 528 . . . . . . . . . . . 12 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → ¬ 𝑥 = ∅)
103102neqned 2367 . . . . . . . . . . 11 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → 𝑥 ≠ ∅)
104 nnsucpred 4634 . . . . . . . . . . 11 ((𝑥 ∈ ω ∧ 𝑥 ≠ ∅) → suc 𝑥 = 𝑥)
105101, 103, 104syl2anc 411 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → suc 𝑥 = 𝑥)
106105eqeq2d 2201 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (suc 𝑧 = suc 𝑥 ↔ suc 𝑧 = 𝑥))
107 eqcom 2191 . . . . . . . . 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 3559 . . . . . . . . . . . 12 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) → if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) = (inl‘ 𝑥))
112111adantr 276 . . . . . . . . . . 11 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) = (inl‘ 𝑥))
113109, 112eqeq12d 2204 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) ↔ (inl‘𝑧) = (inl‘ 𝑥)))
114 vuniex 4456 . . . . . . . . . . . 12 𝑥 ∈ V
115 inl11 7094 . . . . . . . . . . . 12 ((𝑧 ∈ V ∧ 𝑥 ∈ V) → ((inl‘𝑧) = (inl‘ 𝑥) ↔ 𝑧 = 𝑥))
116114, 115mpan2 425 . . . . . . . . . . 11 (𝑧 ∈ V → ((inl‘𝑧) = (inl‘ 𝑥) ↔ 𝑧 = 𝑥))
117116elv 2756 . . . . . . . . . 10 ((inl‘𝑧) = (inl‘ 𝑥) ↔ 𝑧 = 𝑥)
118113, 117bitrdi 196 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) ↔ 𝑧 = 𝑥))
119 nnon 4627 . . . . . . . . . . 11 (𝑧 ∈ ω → 𝑧 ∈ On)
120119ad2antrl 490 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → 𝑧 ∈ On)
1217ad3antrrr 492 . . . . . . . . . . 11 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → 𝑥 ∈ ω)
122 nnon 4627 . . . . . . . . . . 11 ( 𝑥 ∈ ω → 𝑥 ∈ On)
123121, 122syl 14 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → 𝑥 ∈ On)
124 suc11 4575 . . . . . . . . . 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 2201 . . . . . . . 8 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (𝑥 = (𝐺𝑦) ↔ 𝑥 = suc 𝑧))
129108, 126, 1283bitr4rd 221 . . . . . . 7 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥))))
130129rexlimdvaa 2608 . . . . . 6 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) → (∃𝑧 ∈ ω 𝑦 = (inl‘𝑧) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)))))
131 simplr 528 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → ¬ 𝑥 = ∅)
13286adantl 277 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → (𝐺𝑦) = ∅)
133132eqeq2d 2201 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → (𝑥 = (𝐺𝑦) ↔ 𝑥 = ∅))
134131, 133mtbird 674 . . . . . . . 8 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → ¬ 𝑥 = (𝐺𝑦))
135 djune 7107 . . . . . . . . . . . 12 (( 𝑥 ∈ V ∧ 𝑧 ∈ V) → (inl‘ 𝑥) ≠ (inr‘𝑧))
136135elvd 2757 . . . . . . . . . . 11 ( 𝑥 ∈ V → (inl‘ 𝑥) ≠ (inr‘𝑧))
137114, 136ax-mp 5 . . . . . . . . . 10 (inl‘ 𝑥) ≠ (inr‘𝑧)
138137nesymi 2406 . . . . . . . . 9 ¬ (inr‘𝑧) = (inl‘ 𝑥)
13973, 111eqeqan12rd 2206 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → (𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) ↔ (inr‘𝑧) = (inl‘ 𝑥)))
140138, 139mtbiri 676 . . . . . . . 8 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → ¬ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)))
141134, 1402falsed 703 . . . . . . 7 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥))))
142141rexlimdvaa 2608 . . . . . 6 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) → (∃𝑧 ∈ 1o 𝑦 = (inr‘𝑧) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)))))
14398ad2antlr 489 . . . . . 6 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) → (∃𝑧 ∈ ω 𝑦 = (inl‘𝑧) ∨ ∃𝑧 ∈ 1o 𝑦 = (inr‘𝑧)))
144130, 142, 143mpjaod 719 . . . . 5 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥))))
145 exmiddc 837 . . . . . . 7 (DECID 𝑥 = ∅ → (𝑥 = ∅ ∨ ¬ 𝑥 = ∅))
14611, 145syl 14 . . . . . 6 (𝑥 ∈ ω → (𝑥 = ∅ ∨ ¬ 𝑥 = ∅))
147146adantr 276 . . . . 5 ((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) → (𝑥 = ∅ ∨ ¬ 𝑥 = ∅))
148100, 144, 147mpjaodan 799 . . . 4 ((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥))))
149148adantl 277 . . 3 ((⊤ ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o))) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥))))
1501, 13, 32, 149f1o2d 6099 . 2 (⊤ → 𝐹:ω–1-1-onto→(ω ⊔ 1o))
151150mptru 1373 1 𝐹:ω–1-1-onto→(ω ⊔ 1o)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wa 104  wb 105  wo 709  DECID wdc 835   = wceq 1364  wtru 1365  wcel 2160  wne 2360  wrex 2469  Vcvv 2752  wss 3144  c0 3437  ifcif 3549   cuni 3824  cmpt 4079   I cid 4306  Oncon0 4381  suc csuc 4383  ωcom 4607  cres 4646  Fun wfun 5229   Fn wfn 5230  wf 5231  1-1-ontowf1o 5234  cfv 5235  1oc1o 6434  cdju 7066  inlcinl 7074  inrcinr 7075  casecdjucase 7112
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 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-sep 4136  ax-nul 4144  ax-pow 4192  ax-pr 4227  ax-un 4451  ax-setind 4554  ax-iinf 4605
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-ral 2473  df-rex 2474  df-rab 2477  df-v 2754  df-sbc 2978  df-csb 3073  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-nul 3438  df-if 3550  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-int 3860  df-br 4019  df-opab 4080  df-mpt 4081  df-tr 4117  df-id 4311  df-iord 4384  df-on 4386  df-suc 4389  df-iom 4608  df-xp 4650  df-rel 4651  df-cnv 4652  df-co 4653  df-dm 4654  df-rn 4655  df-res 4656  df-ima 4657  df-iota 5196  df-fun 5237  df-fn 5238  df-f 5239  df-f1 5240  df-fo 5241  df-f1o 5242  df-fv 5243  df-1st 6165  df-2nd 6166  df-1o 6441  df-dju 7067  df-inl 7076  df-inr 7077  df-case 7113
This theorem is referenced by:  omp1eom  7124
  Copyright terms: Public domain W3C validator