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

Theorem omp1eomlem 7087
Description: Lemma for omp1eom 7088. (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 6432 . . . . . . 7 (𝑥 ∈ 1o𝑥 = ∅)
32biimpri 133 . . . . . 6 (𝑥 = ∅ → 𝑥 ∈ 1o)
43adantl 277 . . . . 5 (((⊤ ∧ 𝑥 ∈ ω) ∧ 𝑥 = ∅) → 𝑥 ∈ 1o)
5 djurcl 7045 . . . . 5 (𝑥 ∈ 1o → (inr‘𝑥) ∈ (ω ⊔ 1o))
64, 5syl 14 . . . 4 (((⊤ ∧ 𝑥 ∈ ω) ∧ 𝑥 = ∅) → (inr‘𝑥) ∈ (ω ⊔ 1o))
7 nnpredcl 4619 . . . . . 6 (𝑥 ∈ ω → 𝑥 ∈ ω)
87ad2antlr 489 . . . . 5 (((⊤ ∧ 𝑥 ∈ ω) ∧ ¬ 𝑥 = ∅) → 𝑥 ∈ ω)
9 djulcl 7044 . . . . 5 ( 𝑥 ∈ ω → (inl‘ 𝑥) ∈ (ω ⊔ 1o))
108, 9syl 14 . . . 4 (((⊤ ∧ 𝑥 ∈ ω) ∧ ¬ 𝑥 = ∅) → (inl‘ 𝑥) ∈ (ω ⊔ 1o))
11 nndceq0 4614 . . . . 5 (𝑥 ∈ ω → DECID 𝑥 = ∅)
1211adantl 277 . . . 4 ((⊤ ∧ 𝑥 ∈ ω) → DECID 𝑥 = ∅)
136, 10, 12ifcldadc 3563 . . 3 ((⊤ ∧ 𝑥 ∈ ω) → if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) ∈ (ω ⊔ 1o))
14 omp1eom.s . . . . . . . 8 𝑆 = (𝑥 ∈ ω ↦ suc 𝑥)
15 peano2 4591 . . . . . . . 8 (𝑥 ∈ ω → suc 𝑥 ∈ ω)
1614, 15fmpti 5664 . . . . . . 7 𝑆:ω⟶ω
1716a1i 9 . . . . . 6 (⊤ → 𝑆:ω⟶ω)
18 f1oi 5495 . . . . . . . . 9 ( I ↾ 1o):1o1-1-onto→1o
19 f1of 5457 . . . . . . . . 9 (( I ↾ 1o):1o1-1-onto→1o → ( I ↾ 1o):1o⟶1o)
2018, 19ax-mp 5 . . . . . . . 8 ( I ↾ 1o):1o⟶1o
21 1onn 6515 . . . . . . . . 9 1o ∈ ω
22 omelon 4605 . . . . . . . . . 10 ω ∈ On
2322onelssi 4426 . . . . . . . . 9 (1o ∈ ω → 1o ⊆ ω)
2421, 23ax-mp 5 . . . . . . . 8 1o ⊆ ω
25 fss 5373 . . . . . . . 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 7081 . . . . 5 (⊤ → case(𝑆, ( I ↾ 1o)):(ω ⊔ 1o)⟶ω)
29 omp1eom.g . . . . . 6 𝐺 = case(𝑆, ( I ↾ 1o))
3029feq1i 5354 . . . . 5 (𝐺:(ω ⊔ 1o)⟶ω ↔ case(𝑆, ( I ↾ 1o)):(ω ⊔ 1o)⟶ω)
3128, 30sylibr 134 . . . 4 (⊤ → 𝐺:(ω ⊔ 1o)⟶ω)
3231ffvelcdmda 5647 . . 3 ((⊤ ∧ 𝑦 ∈ (ω ⊔ 1o)) → (𝐺𝑦) ∈ ω)
33 ffn 5361 . . . . . . . . . . . . . . . 16 (𝑆:ω⟶ω → 𝑆 Fn ω)
3416, 33mp1i 10 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → 𝑆 Fn ω)
35 ffun 5364 . . . . . . . . . . . . . . . 16 (( I ↾ 1o):1o⟶1o → Fun ( I ↾ 1o))
3620, 35mp1i 10 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → Fun ( I ↾ 1o))
37 simpl 109 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → 𝑧 ∈ ω)
3834, 36, 37caseinl 7084 . . . . . . . . . . . . . 14 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → (case(𝑆, ( I ↾ 1o))‘(inl‘𝑧)) = (𝑆𝑧))
3929eqcomi 2181 . . . . . . . . . . . . . . . 16 case(𝑆, ( I ↾ 1o)) = 𝐺
4039a1i 9 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → case(𝑆, ( I ↾ 1o)) = 𝐺)
41 simpr 110 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → 𝑦 = (inl‘𝑧))
4241eqcomd 2183 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → (inl‘𝑧) = 𝑦)
4340, 42fveq12d 5518 . . . . . . . . . . . . . 14 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → (case(𝑆, ( I ↾ 1o))‘(inl‘𝑧)) = (𝐺𝑦))
44 peano2 4591 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ω → suc 𝑧 ∈ ω)
45 suceq 4399 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑧 → suc 𝑥 = suc 𝑧)
4645, 14fvmptg 5588 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ ω ∧ suc 𝑧 ∈ ω) → (𝑆𝑧) = suc 𝑧)
4744, 46mpdan 421 . . . . . . . . . . . . . . 15 (𝑧 ∈ ω → (𝑆𝑧) = suc 𝑧)
4847adantr 276 . . . . . . . . . . . . . 14 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → (𝑆𝑧) = suc 𝑧)
4938, 43, 483eqtr3d 2218 . . . . . . . . . . . . 13 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → (𝐺𝑦) = suc 𝑧)
50 peano3 4592 . . . . . . . . . . . . . 14 (𝑧 ∈ ω → suc 𝑧 ≠ ∅)
5150adantr 276 . . . . . . . . . . . . 13 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → suc 𝑧 ≠ ∅)
5249, 51eqnetrd 2371 . . . . . . . . . . . 12 ((𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧)) → (𝐺𝑦) ≠ ∅)
5352adantl 277 . . . . . . . . . . 11 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (𝐺𝑦) ≠ ∅)
5453necomd 2433 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → ∅ ≠ (𝐺𝑦))
5554neneqd 2368 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → ¬ ∅ = (𝐺𝑦))
56 simplr 528 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → 𝑥 = ∅)
5756eqeq1d 2186 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (𝑥 = (𝐺𝑦) ↔ ∅ = (𝐺𝑦)))
5855, 57mtbird 673 . . . . . . . 8 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → ¬ 𝑥 = (𝐺𝑦))
59 djune 7071 . . . . . . . . . . . 12 ((𝑧 ∈ V ∧ 𝑥 ∈ V) → (inl‘𝑧) ≠ (inr‘𝑥))
6059elvd 2742 . . . . . . . . . . 11 (𝑧 ∈ V → (inl‘𝑧) ≠ (inr‘𝑥))
6160elv 2741 . . . . . . . . . 10 (inl‘𝑧) ≠ (inr‘𝑥)
6261neii 2349 . . . . . . . . 9 ¬ (inl‘𝑧) = (inr‘𝑥)
63 simprr 531 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → 𝑦 = (inl‘𝑧))
64 simpr 110 . . . . . . . . . . . 12 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) → 𝑥 = ∅)
6564iftrued 3541 . . . . . . . . . . 11 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) → if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) = (inr‘𝑥))
6665adantr 276 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) = (inr‘𝑥))
6763, 66eqeq12d 2192 . . . . . . . . 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 2595 . . . . . 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 5518 . . . . . . . . . . 11 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → (𝐺𝑦) = (case(𝑆, ( I ↾ 1o))‘(inr‘𝑧)))
7514funmpt2 5251 . . . . . . . . . . . . . 14 Fun 𝑆
7675a1i 9 . . . . . . . . . . . . 13 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → Fun 𝑆)
77 fnresi 5329 . . . . . . . . . . . . . 14 ( I ↾ 1o) Fn 1o
7877a1i 9 . . . . . . . . . . . . 13 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → ( I ↾ 1o) Fn 1o)
79 simpl 109 . . . . . . . . . . . . 13 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → 𝑧 ∈ 1o)
8076, 78, 79caseinr 7085 . . . . . . . . . . . 12 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → (case(𝑆, ( I ↾ 1o))‘(inr‘𝑧)) = (( I ↾ 1o)‘𝑧))
81 fvresi 5705 . . . . . . . . . . . . 13 (𝑧 ∈ 1o → (( I ↾ 1o)‘𝑧) = 𝑧)
8281adantr 276 . . . . . . . . . . . 12 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → (( I ↾ 1o)‘𝑧) = 𝑧)
8380, 82eqtrd 2210 . . . . . . . . . . 11 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → (case(𝑆, ( I ↾ 1o))‘(inr‘𝑧)) = 𝑧)
84 el1o 6432 . . . . . . . . . . . 12 (𝑧 ∈ 1o𝑧 = ∅)
8579, 84sylib 122 . . . . . . . . . . 11 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → 𝑧 = ∅)
8674, 83, 853eqtrd 2214 . . . . . . . . . 10 ((𝑧 ∈ 1o𝑦 = (inr‘𝑧)) → (𝐺𝑦) = ∅)
8786adantl 277 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → (𝐺𝑦) = ∅)
8871, 87eqtr4d 2213 . . . . . . . 8 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → 𝑥 = (𝐺𝑦))
8985adantl 277 . . . . . . . . . . 11 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → 𝑧 = ∅)
9071, 89eqtr4d 2213 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → 𝑥 = 𝑧)
9190fveq2d 5515 . . . . . . . . 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 2221 . . . . . . . 8 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)))
9588, 942thd 175 . . . . . . 7 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥))))
9695rexlimdvaa 2595 . . . . . 6 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ 𝑥 = ∅) → (∃𝑧 ∈ 1o 𝑦 = (inr‘𝑧) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)))))
97 djur 7062 . . . . . . . 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 2354 . . . . . . . . . . 11 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → 𝑥 ≠ ∅)
104 nnsucpred 4613 . . . . . . . . . . 11 ((𝑥 ∈ ω ∧ 𝑥 ≠ ∅) → suc 𝑥 = 𝑥)
105101, 103, 104syl2anc 411 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → suc 𝑥 = 𝑥)
106105eqeq2d 2189 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (suc 𝑧 = suc 𝑥 ↔ suc 𝑧 = 𝑥))
107 eqcom 2179 . . . . . . . . 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 3544 . . . . . . . . . . . 12 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) → if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) = (inl‘ 𝑥))
112111adantr 276 . . . . . . . . . . 11 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) = (inl‘ 𝑥))
113109, 112eqeq12d 2192 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) ↔ (inl‘𝑧) = (inl‘ 𝑥)))
114 vuniex 4435 . . . . . . . . . . . 12 𝑥 ∈ V
115 inl11 7058 . . . . . . . . . . . 12 ((𝑧 ∈ V ∧ 𝑥 ∈ V) → ((inl‘𝑧) = (inl‘ 𝑥) ↔ 𝑧 = 𝑥))
116114, 115mpan2 425 . . . . . . . . . . 11 (𝑧 ∈ V → ((inl‘𝑧) = (inl‘ 𝑥) ↔ 𝑧 = 𝑥))
117116elv 2741 . . . . . . . . . 10 ((inl‘𝑧) = (inl‘ 𝑥) ↔ 𝑧 = 𝑥)
118113, 117bitrdi 196 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)) ↔ 𝑧 = 𝑥))
119 nnon 4606 . . . . . . . . . . 11 (𝑧 ∈ ω → 𝑧 ∈ On)
120119ad2antrl 490 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → 𝑧 ∈ On)
1217ad3antrrr 492 . . . . . . . . . . 11 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → 𝑥 ∈ ω)
122 nnon 4606 . . . . . . . . . . 11 ( 𝑥 ∈ ω → 𝑥 ∈ On)
123121, 122syl 14 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → 𝑥 ∈ On)
124 suc11 4554 . . . . . . . . . 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 2189 . . . . . . . 8 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (𝑥 = (𝐺𝑦) ↔ 𝑥 = suc 𝑧))
129108, 126, 1283bitr4rd 221 . . . . . . 7 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ ω ∧ 𝑦 = (inl‘𝑧))) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥))))
130129rexlimdvaa 2595 . . . . . 6 (((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) → (∃𝑧 ∈ ω 𝑦 = (inl‘𝑧) → (𝑥 = (𝐺𝑦) ↔ 𝑦 = if(𝑥 = ∅, (inr‘𝑥), (inl‘ 𝑥)))))
131 simplr 528 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → ¬ 𝑥 = ∅)
13286adantl 277 . . . . . . . . . 10 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → (𝐺𝑦) = ∅)
133132eqeq2d 2189 . . . . . . . . 9 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → (𝑥 = (𝐺𝑦) ↔ 𝑥 = ∅))
134131, 133mtbird 673 . . . . . . . 8 ((((𝑥 ∈ ω ∧ 𝑦 ∈ (ω ⊔ 1o)) ∧ ¬ 𝑥 = ∅) ∧ (𝑧 ∈ 1o𝑦 = (inr‘𝑧))) → ¬ 𝑥 = (𝐺𝑦))
135 djune 7071 . . . . . . . . . . . 12 (( 𝑥 ∈ V ∧ 𝑧 ∈ V) → (inl‘ 𝑥) ≠ (inr‘𝑧))
136135elvd 2742 . . . . . . . . . . 11 ( 𝑥 ∈ V → (inl‘ 𝑥) ≠ (inr‘𝑧))
137114, 136ax-mp 5 . . . . . . . . . 10 (inl‘ 𝑥) ≠ (inr‘𝑧)
138137nesymi 2393 . . . . . . . . 9 ¬ (inr‘𝑧) = (inl‘ 𝑥)
13973, 111eqeqan12rd 2194 . . . . . . . . 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 2595 . . . . . 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 6070 . 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 2148  wne 2347  wrex 2456  Vcvv 2737  wss 3129  c0 3422  ifcif 3534   cuni 3807  cmpt 4061   I cid 4285  Oncon0 4360  suc csuc 4362  ωcom 4586  cres 4625  Fun wfun 5206   Fn wfn 5207  wf 5208  1-1-ontowf1o 5211  cfv 5212  1oc1o 6404  cdju 7030  inlcinl 7038  inrcinr 7039  casecdjucase 7076
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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-nul 4126  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533  ax-iinf 4584
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-if 3535  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-int 3843  df-br 4001  df-opab 4062  df-mpt 4063  df-tr 4099  df-id 4290  df-iord 4363  df-on 4365  df-suc 4368  df-iom 4587  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-ima 4636  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-f1 5217  df-fo 5218  df-f1o 5219  df-fv 5220  df-1st 6135  df-2nd 6136  df-1o 6411  df-dju 7031  df-inl 7040  df-inr 7041  df-case 7077
This theorem is referenced by:  omp1eom  7088
  Copyright terms: Public domain W3C validator