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

Theorem omp1eomlem 7095
Description: Lemma for omp1eom 7096. (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 6440 . . . . . . 7 (π‘₯ ∈ 1o ↔ π‘₯ = βˆ…)
32biimpri 133 . . . . . 6 (π‘₯ = βˆ… β†’ π‘₯ ∈ 1o)
43adantl 277 . . . . 5 (((⊀ ∧ π‘₯ ∈ Ο‰) ∧ π‘₯ = βˆ…) β†’ π‘₯ ∈ 1o)
5 djurcl 7053 . . . . 5 (π‘₯ ∈ 1o β†’ (inrβ€˜π‘₯) ∈ (Ο‰ βŠ” 1o))
64, 5syl 14 . . . 4 (((⊀ ∧ π‘₯ ∈ Ο‰) ∧ π‘₯ = βˆ…) β†’ (inrβ€˜π‘₯) ∈ (Ο‰ βŠ” 1o))
7 nnpredcl 4624 . . . . . 6 (π‘₯ ∈ Ο‰ β†’ βˆͺ π‘₯ ∈ Ο‰)
87ad2antlr 489 . . . . 5 (((⊀ ∧ π‘₯ ∈ Ο‰) ∧ Β¬ π‘₯ = βˆ…) β†’ βˆͺ π‘₯ ∈ Ο‰)
9 djulcl 7052 . . . . 5 (βˆͺ π‘₯ ∈ Ο‰ β†’ (inlβ€˜βˆͺ π‘₯) ∈ (Ο‰ βŠ” 1o))
108, 9syl 14 . . . 4 (((⊀ ∧ π‘₯ ∈ Ο‰) ∧ Β¬ π‘₯ = βˆ…) β†’ (inlβ€˜βˆͺ π‘₯) ∈ (Ο‰ βŠ” 1o))
11 nndceq0 4619 . . . . 5 (π‘₯ ∈ Ο‰ β†’ DECID π‘₯ = βˆ…)
1211adantl 277 . . . 4 ((⊀ ∧ π‘₯ ∈ Ο‰) β†’ DECID π‘₯ = βˆ…)
136, 10, 12ifcldadc 3565 . . 3 ((⊀ ∧ π‘₯ ∈ Ο‰) β†’ if(π‘₯ = βˆ…, (inrβ€˜π‘₯), (inlβ€˜βˆͺ π‘₯)) ∈ (Ο‰ βŠ” 1o))
14 omp1eom.s . . . . . . . 8 𝑆 = (π‘₯ ∈ Ο‰ ↦ suc π‘₯)
15 peano2 4596 . . . . . . . 8 (π‘₯ ∈ Ο‰ β†’ suc π‘₯ ∈ Ο‰)
1614, 15fmpti 5670 . . . . . . 7 𝑆:Ο‰βŸΆΟ‰
1716a1i 9 . . . . . 6 (⊀ β†’ 𝑆:Ο‰βŸΆΟ‰)
18 f1oi 5501 . . . . . . . . 9 ( I β†Ύ 1o):1o–1-1-ontoβ†’1o
19 f1of 5463 . . . . . . . . 9 (( I β†Ύ 1o):1o–1-1-ontoβ†’1o β†’ ( I β†Ύ 1o):1o⟢1o)
2018, 19ax-mp 5 . . . . . . . 8 ( I β†Ύ 1o):1o⟢1o
21 1onn 6523 . . . . . . . . 9 1o ∈ Ο‰
22 omelon 4610 . . . . . . . . . 10 Ο‰ ∈ On
2322onelssi 4431 . . . . . . . . 9 (1o ∈ Ο‰ β†’ 1o βŠ† Ο‰)
2421, 23ax-mp 5 . . . . . . . 8 1o βŠ† Ο‰
25 fss 5379 . . . . . . . 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 7089 . . . . 5 (⊀ β†’ case(𝑆, ( I β†Ύ 1o)):(Ο‰ βŠ” 1o)βŸΆΟ‰)
29 omp1eom.g . . . . . 6 𝐺 = case(𝑆, ( I β†Ύ 1o))
3029feq1i 5360 . . . . 5 (𝐺:(Ο‰ βŠ” 1o)βŸΆΟ‰ ↔ case(𝑆, ( I β†Ύ 1o)):(Ο‰ βŠ” 1o)βŸΆΟ‰)
3128, 30sylibr 134 . . . 4 (⊀ β†’ 𝐺:(Ο‰ βŠ” 1o)βŸΆΟ‰)
3231ffvelcdmda 5653 . . 3 ((⊀ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) β†’ (πΊβ€˜π‘¦) ∈ Ο‰)
33 ffn 5367 . . . . . . . . . . . . . . . 16 (𝑆:Ο‰βŸΆΟ‰ β†’ 𝑆 Fn Ο‰)
3416, 33mp1i 10 . . . . . . . . . . . . . . 15 ((𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§)) β†’ 𝑆 Fn Ο‰)
35 ffun 5370 . . . . . . . . . . . . . . . 16 (( I β†Ύ 1o):1o⟢1o β†’ Fun ( I β†Ύ 1o))
3620, 35mp1i 10 . . . . . . . . . . . . . . 15 ((𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§)) β†’ Fun ( I β†Ύ 1o))
37 simpl 109 . . . . . . . . . . . . . . 15 ((𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§)) β†’ 𝑧 ∈ Ο‰)
3834, 36, 37caseinl 7092 . . . . . . . . . . . . . 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 5524 . . . . . . . . . . . . . 14 ((𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§)) β†’ (case(𝑆, ( I β†Ύ 1o))β€˜(inlβ€˜π‘§)) = (πΊβ€˜π‘¦))
44 peano2 4596 . . . . . . . . . . . . . . . 16 (𝑧 ∈ Ο‰ β†’ suc 𝑧 ∈ Ο‰)
45 suceq 4404 . . . . . . . . . . . . . . . . 17 (π‘₯ = 𝑧 β†’ suc π‘₯ = suc 𝑧)
4645, 14fvmptg 5594 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ Ο‰ ∧ suc 𝑧 ∈ Ο‰) β†’ (π‘†β€˜π‘§) = suc 𝑧)
4744, 46mpdan 421 . . . . . . . . . . . . . . 15 (𝑧 ∈ Ο‰ β†’ (π‘†β€˜π‘§) = suc 𝑧)
4847adantr 276 . . . . . . . . . . . . . 14 ((𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§)) β†’ (π‘†β€˜π‘§) = suc 𝑧)
4938, 43, 483eqtr3d 2218 . . . . . . . . . . . . 13 ((𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§)) β†’ (πΊβ€˜π‘¦) = suc 𝑧)
50 peano3 4597 . . . . . . . . . . . . . 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 7079 . . . . . . . . . . . 12 ((𝑧 ∈ V ∧ π‘₯ ∈ V) β†’ (inlβ€˜π‘§) β‰  (inrβ€˜π‘₯))
6059elvd 2744 . . . . . . . . . . 11 (𝑧 ∈ V β†’ (inlβ€˜π‘§) β‰  (inrβ€˜π‘₯))
6160elv 2743 . . . . . . . . . 10 (inlβ€˜π‘§) β‰  (inrβ€˜π‘₯)
6261neii 2349 . . . . . . . . 9 Β¬ (inlβ€˜π‘§) = (inrβ€˜π‘₯)
63 simprr 531 . . . . . . . . . 10 ((((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ π‘₯ = βˆ…) ∧ (𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§))) β†’ 𝑦 = (inlβ€˜π‘§))
64 simpr 110 . . . . . . . . . . . 12 (((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ π‘₯ = βˆ…) β†’ π‘₯ = βˆ…)
6564iftrued 3543 . . . . . . . . . . 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 5524 . . . . . . . . . . 11 ((𝑧 ∈ 1o ∧ 𝑦 = (inrβ€˜π‘§)) β†’ (πΊβ€˜π‘¦) = (case(𝑆, ( I β†Ύ 1o))β€˜(inrβ€˜π‘§)))
7514funmpt2 5257 . . . . . . . . . . . . . 14 Fun 𝑆
7675a1i 9 . . . . . . . . . . . . 13 ((𝑧 ∈ 1o ∧ 𝑦 = (inrβ€˜π‘§)) β†’ Fun 𝑆)
77 fnresi 5335 . . . . . . . . . . . . . 14 ( I β†Ύ 1o) Fn 1o
7877a1i 9 . . . . . . . . . . . . 13 ((𝑧 ∈ 1o ∧ 𝑦 = (inrβ€˜π‘§)) β†’ ( I β†Ύ 1o) Fn 1o)
79 simpl 109 . . . . . . . . . . . . 13 ((𝑧 ∈ 1o ∧ 𝑦 = (inrβ€˜π‘§)) β†’ 𝑧 ∈ 1o)
8076, 78, 79caseinr 7093 . . . . . . . . . . . 12 ((𝑧 ∈ 1o ∧ 𝑦 = (inrβ€˜π‘§)) β†’ (case(𝑆, ( I β†Ύ 1o))β€˜(inrβ€˜π‘§)) = (( I β†Ύ 1o)β€˜π‘§))
81 fvresi 5711 . . . . . . . . . . . . 13 (𝑧 ∈ 1o β†’ (( I β†Ύ 1o)β€˜π‘§) = 𝑧)
8281adantr 276 . . . . . . . . . . . 12 ((𝑧 ∈ 1o ∧ 𝑦 = (inrβ€˜π‘§)) β†’ (( I β†Ύ 1o)β€˜π‘§) = 𝑧)
8380, 82eqtrd 2210 . . . . . . . . . . 11 ((𝑧 ∈ 1o ∧ 𝑦 = (inrβ€˜π‘§)) β†’ (case(𝑆, ( I β†Ύ 1o))β€˜(inrβ€˜π‘§)) = 𝑧)
84 el1o 6440 . . . . . . . . . . . 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 5521 . . . . . . . . 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 7070 . . . . . . . 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 4618 . . . . . . . . . . 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 3546 . . . . . . . . . . . 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 4440 . . . . . . . . . . . 12 βˆͺ π‘₯ ∈ V
115 inl11 7066 . . . . . . . . . . . 12 ((𝑧 ∈ V ∧ βˆͺ π‘₯ ∈ V) β†’ ((inlβ€˜π‘§) = (inlβ€˜βˆͺ π‘₯) ↔ 𝑧 = βˆͺ π‘₯))
116114, 115mpan2 425 . . . . . . . . . . 11 (𝑧 ∈ V β†’ ((inlβ€˜π‘§) = (inlβ€˜βˆͺ π‘₯) ↔ 𝑧 = βˆͺ π‘₯))
117116elv 2743 . . . . . . . . . 10 ((inlβ€˜π‘§) = (inlβ€˜βˆͺ π‘₯) ↔ 𝑧 = βˆͺ π‘₯)
118113, 117bitrdi 196 . . . . . . . . 9 ((((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ Β¬ π‘₯ = βˆ…) ∧ (𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§))) β†’ (𝑦 = if(π‘₯ = βˆ…, (inrβ€˜π‘₯), (inlβ€˜βˆͺ π‘₯)) ↔ 𝑧 = βˆͺ π‘₯))
119 nnon 4611 . . . . . . . . . . 11 (𝑧 ∈ Ο‰ β†’ 𝑧 ∈ On)
120119ad2antrl 490 . . . . . . . . . 10 ((((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ Β¬ π‘₯ = βˆ…) ∧ (𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§))) β†’ 𝑧 ∈ On)
1217ad3antrrr 492 . . . . . . . . . . 11 ((((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ Β¬ π‘₯ = βˆ…) ∧ (𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§))) β†’ βˆͺ π‘₯ ∈ Ο‰)
122 nnon 4611 . . . . . . . . . . 11 (βˆͺ π‘₯ ∈ Ο‰ β†’ βˆͺ π‘₯ ∈ On)
123121, 122syl 14 . . . . . . . . . 10 ((((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ Β¬ π‘₯ = βˆ…) ∧ (𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§))) β†’ βˆͺ π‘₯ ∈ On)
124 suc11 4559 . . . . . . . . . 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 7079 . . . . . . . . . . . 12 ((βˆͺ π‘₯ ∈ V ∧ 𝑧 ∈ V) β†’ (inlβ€˜βˆͺ π‘₯) β‰  (inrβ€˜π‘§))
136135elvd 2744 . . . . . . . . . . 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 6078 . 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 2739   βŠ† wss 3131  βˆ…c0 3424  ifcif 3536  βˆͺ cuni 3811   ↦ cmpt 4066   I cid 4290  Oncon0 4365  suc csuc 4367  Ο‰com 4591   β†Ύ cres 4630  Fun wfun 5212   Fn wfn 5213  βŸΆwf 5214  β€“1-1-ontoβ†’wf1o 5217  β€˜cfv 5218  1oc1o 6412   βŠ” cdju 7038  inlcinl 7046  inrcinr 7047  casecdjucase 7084
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 4123  ax-nul 4131  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538  ax-iinf 4589
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 2741  df-sbc 2965  df-csb 3060  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-if 3537  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-int 3847  df-br 4006  df-opab 4067  df-mpt 4068  df-tr 4104  df-id 4295  df-iord 4368  df-on 4370  df-suc 4373  df-iom 4592  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-1st 6143  df-2nd 6144  df-1o 6419  df-dju 7039  df-inl 7048  df-inr 7049  df-case 7085
This theorem is referenced by:  omp1eom  7096
  Copyright terms: Public domain W3C validator