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

Theorem omp1eomlem 7107
Description: Lemma for omp1eom 7108. (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 6452 . . . . . . 7 (π‘₯ ∈ 1o ↔ π‘₯ = βˆ…)
32biimpri 133 . . . . . 6 (π‘₯ = βˆ… β†’ π‘₯ ∈ 1o)
43adantl 277 . . . . 5 (((⊀ ∧ π‘₯ ∈ Ο‰) ∧ π‘₯ = βˆ…) β†’ π‘₯ ∈ 1o)
5 djurcl 7065 . . . . 5 (π‘₯ ∈ 1o β†’ (inrβ€˜π‘₯) ∈ (Ο‰ βŠ” 1o))
64, 5syl 14 . . . 4 (((⊀ ∧ π‘₯ ∈ Ο‰) ∧ π‘₯ = βˆ…) β†’ (inrβ€˜π‘₯) ∈ (Ο‰ βŠ” 1o))
7 nnpredcl 4634 . . . . . 6 (π‘₯ ∈ Ο‰ β†’ βˆͺ π‘₯ ∈ Ο‰)
87ad2antlr 489 . . . . 5 (((⊀ ∧ π‘₯ ∈ Ο‰) ∧ Β¬ π‘₯ = βˆ…) β†’ βˆͺ π‘₯ ∈ Ο‰)
9 djulcl 7064 . . . . 5 (βˆͺ π‘₯ ∈ Ο‰ β†’ (inlβ€˜βˆͺ π‘₯) ∈ (Ο‰ βŠ” 1o))
108, 9syl 14 . . . 4 (((⊀ ∧ π‘₯ ∈ Ο‰) ∧ Β¬ π‘₯ = βˆ…) β†’ (inlβ€˜βˆͺ π‘₯) ∈ (Ο‰ βŠ” 1o))
11 nndceq0 4629 . . . . 5 (π‘₯ ∈ Ο‰ β†’ DECID π‘₯ = βˆ…)
1211adantl 277 . . . 4 ((⊀ ∧ π‘₯ ∈ Ο‰) β†’ DECID π‘₯ = βˆ…)
136, 10, 12ifcldadc 3575 . . 3 ((⊀ ∧ π‘₯ ∈ Ο‰) β†’ if(π‘₯ = βˆ…, (inrβ€˜π‘₯), (inlβ€˜βˆͺ π‘₯)) ∈ (Ο‰ βŠ” 1o))
14 omp1eom.s . . . . . . . 8 𝑆 = (π‘₯ ∈ Ο‰ ↦ suc π‘₯)
15 peano2 4606 . . . . . . . 8 (π‘₯ ∈ Ο‰ β†’ suc π‘₯ ∈ Ο‰)
1614, 15fmpti 5681 . . . . . . 7 𝑆:Ο‰βŸΆΟ‰
1716a1i 9 . . . . . 6 (⊀ β†’ 𝑆:Ο‰βŸΆΟ‰)
18 f1oi 5511 . . . . . . . . 9 ( I β†Ύ 1o):1o–1-1-ontoβ†’1o
19 f1of 5473 . . . . . . . . 9 (( I β†Ύ 1o):1o–1-1-ontoβ†’1o β†’ ( I β†Ύ 1o):1o⟢1o)
2018, 19ax-mp 5 . . . . . . . 8 ( I β†Ύ 1o):1o⟢1o
21 1onn 6535 . . . . . . . . 9 1o ∈ Ο‰
22 omelon 4620 . . . . . . . . . 10 Ο‰ ∈ On
2322onelssi 4441 . . . . . . . . 9 (1o ∈ Ο‰ β†’ 1o βŠ† Ο‰)
2421, 23ax-mp 5 . . . . . . . 8 1o βŠ† Ο‰
25 fss 5389 . . . . . . . 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 7101 . . . . 5 (⊀ β†’ case(𝑆, ( I β†Ύ 1o)):(Ο‰ βŠ” 1o)βŸΆΟ‰)
29 omp1eom.g . . . . . 6 𝐺 = case(𝑆, ( I β†Ύ 1o))
3029feq1i 5370 . . . . 5 (𝐺:(Ο‰ βŠ” 1o)βŸΆΟ‰ ↔ case(𝑆, ( I β†Ύ 1o)):(Ο‰ βŠ” 1o)βŸΆΟ‰)
3128, 30sylibr 134 . . . 4 (⊀ β†’ 𝐺:(Ο‰ βŠ” 1o)βŸΆΟ‰)
3231ffvelcdmda 5664 . . 3 ((⊀ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) β†’ (πΊβ€˜π‘¦) ∈ Ο‰)
33 ffn 5377 . . . . . . . . . . . . . . . 16 (𝑆:Ο‰βŸΆΟ‰ β†’ 𝑆 Fn Ο‰)
3416, 33mp1i 10 . . . . . . . . . . . . . . 15 ((𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§)) β†’ 𝑆 Fn Ο‰)
35 ffun 5380 . . . . . . . . . . . . . . . 16 (( I β†Ύ 1o):1o⟢1o β†’ Fun ( I β†Ύ 1o))
3620, 35mp1i 10 . . . . . . . . . . . . . . 15 ((𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§)) β†’ Fun ( I β†Ύ 1o))
37 simpl 109 . . . . . . . . . . . . . . 15 ((𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§)) β†’ 𝑧 ∈ Ο‰)
3834, 36, 37caseinl 7104 . . . . . . . . . . . . . 14 ((𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§)) β†’ (case(𝑆, ( I β†Ύ 1o))β€˜(inlβ€˜π‘§)) = (π‘†β€˜π‘§))
3929eqcomi 2191 . . . . . . . . . . . . . . . 16 case(𝑆, ( I β†Ύ 1o)) = 𝐺
4039a1i 9 . . . . . . . . . . . . . . 15 ((𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§)) β†’ case(𝑆, ( I β†Ύ 1o)) = 𝐺)
41 simpr 110 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§)) β†’ 𝑦 = (inlβ€˜π‘§))
4241eqcomd 2193 . . . . . . . . . . . . . . 15 ((𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§)) β†’ (inlβ€˜π‘§) = 𝑦)
4340, 42fveq12d 5534 . . . . . . . . . . . . . 14 ((𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§)) β†’ (case(𝑆, ( I β†Ύ 1o))β€˜(inlβ€˜π‘§)) = (πΊβ€˜π‘¦))
44 peano2 4606 . . . . . . . . . . . . . . . 16 (𝑧 ∈ Ο‰ β†’ suc 𝑧 ∈ Ο‰)
45 suceq 4414 . . . . . . . . . . . . . . . . 17 (π‘₯ = 𝑧 β†’ suc π‘₯ = suc 𝑧)
4645, 14fvmptg 5605 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ Ο‰ ∧ suc 𝑧 ∈ Ο‰) β†’ (π‘†β€˜π‘§) = suc 𝑧)
4744, 46mpdan 421 . . . . . . . . . . . . . . 15 (𝑧 ∈ Ο‰ β†’ (π‘†β€˜π‘§) = suc 𝑧)
4847adantr 276 . . . . . . . . . . . . . 14 ((𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§)) β†’ (π‘†β€˜π‘§) = suc 𝑧)
4938, 43, 483eqtr3d 2228 . . . . . . . . . . . . 13 ((𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§)) β†’ (πΊβ€˜π‘¦) = suc 𝑧)
50 peano3 4607 . . . . . . . . . . . . . 14 (𝑧 ∈ Ο‰ β†’ suc 𝑧 β‰  βˆ…)
5150adantr 276 . . . . . . . . . . . . 13 ((𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§)) β†’ suc 𝑧 β‰  βˆ…)
5249, 51eqnetrd 2381 . . . . . . . . . . . 12 ((𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§)) β†’ (πΊβ€˜π‘¦) β‰  βˆ…)
5352adantl 277 . . . . . . . . . . 11 ((((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ π‘₯ = βˆ…) ∧ (𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§))) β†’ (πΊβ€˜π‘¦) β‰  βˆ…)
5453necomd 2443 . . . . . . . . . 10 ((((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ π‘₯ = βˆ…) ∧ (𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§))) β†’ βˆ… β‰  (πΊβ€˜π‘¦))
5554neneqd 2378 . . . . . . . . 9 ((((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ π‘₯ = βˆ…) ∧ (𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§))) β†’ Β¬ βˆ… = (πΊβ€˜π‘¦))
56 simplr 528 . . . . . . . . . 10 ((((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ π‘₯ = βˆ…) ∧ (𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§))) β†’ π‘₯ = βˆ…)
5756eqeq1d 2196 . . . . . . . . 9 ((((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ π‘₯ = βˆ…) ∧ (𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§))) β†’ (π‘₯ = (πΊβ€˜π‘¦) ↔ βˆ… = (πΊβ€˜π‘¦)))
5855, 57mtbird 674 . . . . . . . 8 ((((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ π‘₯ = βˆ…) ∧ (𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§))) β†’ Β¬ π‘₯ = (πΊβ€˜π‘¦))
59 djune 7091 . . . . . . . . . . . 12 ((𝑧 ∈ V ∧ π‘₯ ∈ V) β†’ (inlβ€˜π‘§) β‰  (inrβ€˜π‘₯))
6059elvd 2754 . . . . . . . . . . 11 (𝑧 ∈ V β†’ (inlβ€˜π‘§) β‰  (inrβ€˜π‘₯))
6160elv 2753 . . . . . . . . . 10 (inlβ€˜π‘§) β‰  (inrβ€˜π‘₯)
6261neii 2359 . . . . . . . . 9 Β¬ (inlβ€˜π‘§) = (inrβ€˜π‘₯)
63 simprr 531 . . . . . . . . . 10 ((((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ π‘₯ = βˆ…) ∧ (𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§))) β†’ 𝑦 = (inlβ€˜π‘§))
64 simpr 110 . . . . . . . . . . . 12 (((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ π‘₯ = βˆ…) β†’ π‘₯ = βˆ…)
6564iftrued 3553 . . . . . . . . . . 11 (((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ π‘₯ = βˆ…) β†’ if(π‘₯ = βˆ…, (inrβ€˜π‘₯), (inlβ€˜βˆͺ π‘₯)) = (inrβ€˜π‘₯))
6665adantr 276 . . . . . . . . . 10 ((((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ π‘₯ = βˆ…) ∧ (𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§))) β†’ if(π‘₯ = βˆ…, (inrβ€˜π‘₯), (inlβ€˜βˆͺ π‘₯)) = (inrβ€˜π‘₯))
6763, 66eqeq12d 2202 . . . . . . . . 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 2605 . . . . . 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 5534 . . . . . . . . . . 11 ((𝑧 ∈ 1o ∧ 𝑦 = (inrβ€˜π‘§)) β†’ (πΊβ€˜π‘¦) = (case(𝑆, ( I β†Ύ 1o))β€˜(inrβ€˜π‘§)))
7514funmpt2 5267 . . . . . . . . . . . . . 14 Fun 𝑆
7675a1i 9 . . . . . . . . . . . . 13 ((𝑧 ∈ 1o ∧ 𝑦 = (inrβ€˜π‘§)) β†’ Fun 𝑆)
77 fnresi 5345 . . . . . . . . . . . . . 14 ( I β†Ύ 1o) Fn 1o
7877a1i 9 . . . . . . . . . . . . 13 ((𝑧 ∈ 1o ∧ 𝑦 = (inrβ€˜π‘§)) β†’ ( I β†Ύ 1o) Fn 1o)
79 simpl 109 . . . . . . . . . . . . 13 ((𝑧 ∈ 1o ∧ 𝑦 = (inrβ€˜π‘§)) β†’ 𝑧 ∈ 1o)
8076, 78, 79caseinr 7105 . . . . . . . . . . . 12 ((𝑧 ∈ 1o ∧ 𝑦 = (inrβ€˜π‘§)) β†’ (case(𝑆, ( I β†Ύ 1o))β€˜(inrβ€˜π‘§)) = (( I β†Ύ 1o)β€˜π‘§))
81 fvresi 5722 . . . . . . . . . . . . 13 (𝑧 ∈ 1o β†’ (( I β†Ύ 1o)β€˜π‘§) = 𝑧)
8281adantr 276 . . . . . . . . . . . 12 ((𝑧 ∈ 1o ∧ 𝑦 = (inrβ€˜π‘§)) β†’ (( I β†Ύ 1o)β€˜π‘§) = 𝑧)
8380, 82eqtrd 2220 . . . . . . . . . . 11 ((𝑧 ∈ 1o ∧ 𝑦 = (inrβ€˜π‘§)) β†’ (case(𝑆, ( I β†Ύ 1o))β€˜(inrβ€˜π‘§)) = 𝑧)
84 el1o 6452 . . . . . . . . . . . 12 (𝑧 ∈ 1o ↔ 𝑧 = βˆ…)
8579, 84sylib 122 . . . . . . . . . . 11 ((𝑧 ∈ 1o ∧ 𝑦 = (inrβ€˜π‘§)) β†’ 𝑧 = βˆ…)
8674, 83, 853eqtrd 2224 . . . . . . . . . 10 ((𝑧 ∈ 1o ∧ 𝑦 = (inrβ€˜π‘§)) β†’ (πΊβ€˜π‘¦) = βˆ…)
8786adantl 277 . . . . . . . . 9 ((((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ π‘₯ = βˆ…) ∧ (𝑧 ∈ 1o ∧ 𝑦 = (inrβ€˜π‘§))) β†’ (πΊβ€˜π‘¦) = βˆ…)
8871, 87eqtr4d 2223 . . . . . . . 8 ((((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ π‘₯ = βˆ…) ∧ (𝑧 ∈ 1o ∧ 𝑦 = (inrβ€˜π‘§))) β†’ π‘₯ = (πΊβ€˜π‘¦))
8985adantl 277 . . . . . . . . . . 11 ((((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ π‘₯ = βˆ…) ∧ (𝑧 ∈ 1o ∧ 𝑦 = (inrβ€˜π‘§))) β†’ 𝑧 = βˆ…)
9071, 89eqtr4d 2223 . . . . . . . . . 10 ((((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ π‘₯ = βˆ…) ∧ (𝑧 ∈ 1o ∧ 𝑦 = (inrβ€˜π‘§))) β†’ π‘₯ = 𝑧)
9190fveq2d 5531 . . . . . . . . 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 2231 . . . . . . . 8 ((((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ π‘₯ = βˆ…) ∧ (𝑧 ∈ 1o ∧ 𝑦 = (inrβ€˜π‘§))) β†’ 𝑦 = if(π‘₯ = βˆ…, (inrβ€˜π‘₯), (inlβ€˜βˆͺ π‘₯)))
9588, 942thd 175 . . . . . . 7 ((((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ π‘₯ = βˆ…) ∧ (𝑧 ∈ 1o ∧ 𝑦 = (inrβ€˜π‘§))) β†’ (π‘₯ = (πΊβ€˜π‘¦) ↔ 𝑦 = if(π‘₯ = βˆ…, (inrβ€˜π‘₯), (inlβ€˜βˆͺ π‘₯))))
9695rexlimdvaa 2605 . . . . . 6 (((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ π‘₯ = βˆ…) β†’ (βˆƒπ‘§ ∈ 1o 𝑦 = (inrβ€˜π‘§) β†’ (π‘₯ = (πΊβ€˜π‘¦) ↔ 𝑦 = if(π‘₯ = βˆ…, (inrβ€˜π‘₯), (inlβ€˜βˆͺ π‘₯)))))
97 djur 7082 . . . . . . . 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 2364 . . . . . . . . . . 11 ((((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ Β¬ π‘₯ = βˆ…) ∧ (𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§))) β†’ π‘₯ β‰  βˆ…)
104 nnsucpred 4628 . . . . . . . . . . 11 ((π‘₯ ∈ Ο‰ ∧ π‘₯ β‰  βˆ…) β†’ suc βˆͺ π‘₯ = π‘₯)
105101, 103, 104syl2anc 411 . . . . . . . . . 10 ((((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ Β¬ π‘₯ = βˆ…) ∧ (𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§))) β†’ suc βˆͺ π‘₯ = π‘₯)
106105eqeq2d 2199 . . . . . . . . 9 ((((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ Β¬ π‘₯ = βˆ…) ∧ (𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§))) β†’ (suc 𝑧 = suc βˆͺ π‘₯ ↔ suc 𝑧 = π‘₯))
107 eqcom 2189 . . . . . . . . 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 3556 . . . . . . . . . . . 12 (((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ Β¬ π‘₯ = βˆ…) β†’ if(π‘₯ = βˆ…, (inrβ€˜π‘₯), (inlβ€˜βˆͺ π‘₯)) = (inlβ€˜βˆͺ π‘₯))
112111adantr 276 . . . . . . . . . . 11 ((((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ Β¬ π‘₯ = βˆ…) ∧ (𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§))) β†’ if(π‘₯ = βˆ…, (inrβ€˜π‘₯), (inlβ€˜βˆͺ π‘₯)) = (inlβ€˜βˆͺ π‘₯))
113109, 112eqeq12d 2202 . . . . . . . . . 10 ((((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ Β¬ π‘₯ = βˆ…) ∧ (𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§))) β†’ (𝑦 = if(π‘₯ = βˆ…, (inrβ€˜π‘₯), (inlβ€˜βˆͺ π‘₯)) ↔ (inlβ€˜π‘§) = (inlβ€˜βˆͺ π‘₯)))
114 vuniex 4450 . . . . . . . . . . . 12 βˆͺ π‘₯ ∈ V
115 inl11 7078 . . . . . . . . . . . 12 ((𝑧 ∈ V ∧ βˆͺ π‘₯ ∈ V) β†’ ((inlβ€˜π‘§) = (inlβ€˜βˆͺ π‘₯) ↔ 𝑧 = βˆͺ π‘₯))
116114, 115mpan2 425 . . . . . . . . . . 11 (𝑧 ∈ V β†’ ((inlβ€˜π‘§) = (inlβ€˜βˆͺ π‘₯) ↔ 𝑧 = βˆͺ π‘₯))
117116elv 2753 . . . . . . . . . 10 ((inlβ€˜π‘§) = (inlβ€˜βˆͺ π‘₯) ↔ 𝑧 = βˆͺ π‘₯)
118113, 117bitrdi 196 . . . . . . . . 9 ((((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ Β¬ π‘₯ = βˆ…) ∧ (𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§))) β†’ (𝑦 = if(π‘₯ = βˆ…, (inrβ€˜π‘₯), (inlβ€˜βˆͺ π‘₯)) ↔ 𝑧 = βˆͺ π‘₯))
119 nnon 4621 . . . . . . . . . . 11 (𝑧 ∈ Ο‰ β†’ 𝑧 ∈ On)
120119ad2antrl 490 . . . . . . . . . 10 ((((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ Β¬ π‘₯ = βˆ…) ∧ (𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§))) β†’ 𝑧 ∈ On)
1217ad3antrrr 492 . . . . . . . . . . 11 ((((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ Β¬ π‘₯ = βˆ…) ∧ (𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§))) β†’ βˆͺ π‘₯ ∈ Ο‰)
122 nnon 4621 . . . . . . . . . . 11 (βˆͺ π‘₯ ∈ Ο‰ β†’ βˆͺ π‘₯ ∈ On)
123121, 122syl 14 . . . . . . . . . 10 ((((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ Β¬ π‘₯ = βˆ…) ∧ (𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§))) β†’ βˆͺ π‘₯ ∈ On)
124 suc11 4569 . . . . . . . . . 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 2199 . . . . . . . 8 ((((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ Β¬ π‘₯ = βˆ…) ∧ (𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§))) β†’ (π‘₯ = (πΊβ€˜π‘¦) ↔ π‘₯ = suc 𝑧))
129108, 126, 1283bitr4rd 221 . . . . . . 7 ((((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ Β¬ π‘₯ = βˆ…) ∧ (𝑧 ∈ Ο‰ ∧ 𝑦 = (inlβ€˜π‘§))) β†’ (π‘₯ = (πΊβ€˜π‘¦) ↔ 𝑦 = if(π‘₯ = βˆ…, (inrβ€˜π‘₯), (inlβ€˜βˆͺ π‘₯))))
130129rexlimdvaa 2605 . . . . . 6 (((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ Β¬ π‘₯ = βˆ…) β†’ (βˆƒπ‘§ ∈ Ο‰ 𝑦 = (inlβ€˜π‘§) β†’ (π‘₯ = (πΊβ€˜π‘¦) ↔ 𝑦 = if(π‘₯ = βˆ…, (inrβ€˜π‘₯), (inlβ€˜βˆͺ π‘₯)))))
131 simplr 528 . . . . . . . . 9 ((((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ Β¬ π‘₯ = βˆ…) ∧ (𝑧 ∈ 1o ∧ 𝑦 = (inrβ€˜π‘§))) β†’ Β¬ π‘₯ = βˆ…)
13286adantl 277 . . . . . . . . . 10 ((((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ Β¬ π‘₯ = βˆ…) ∧ (𝑧 ∈ 1o ∧ 𝑦 = (inrβ€˜π‘§))) β†’ (πΊβ€˜π‘¦) = βˆ…)
133132eqeq2d 2199 . . . . . . . . 9 ((((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ Β¬ π‘₯ = βˆ…) ∧ (𝑧 ∈ 1o ∧ 𝑦 = (inrβ€˜π‘§))) β†’ (π‘₯ = (πΊβ€˜π‘¦) ↔ π‘₯ = βˆ…))
134131, 133mtbird 674 . . . . . . . 8 ((((π‘₯ ∈ Ο‰ ∧ 𝑦 ∈ (Ο‰ βŠ” 1o)) ∧ Β¬ π‘₯ = βˆ…) ∧ (𝑧 ∈ 1o ∧ 𝑦 = (inrβ€˜π‘§))) β†’ Β¬ π‘₯ = (πΊβ€˜π‘¦))
135 djune 7091 . . . . . . . . . . . 12 ((βˆͺ π‘₯ ∈ V ∧ 𝑧 ∈ V) β†’ (inlβ€˜βˆͺ π‘₯) β‰  (inrβ€˜π‘§))
136135elvd 2754 . . . . . . . . . . 11 (βˆͺ π‘₯ ∈ V β†’ (inlβ€˜βˆͺ π‘₯) β‰  (inrβ€˜π‘§))
137114, 136ax-mp 5 . . . . . . . . . 10 (inlβ€˜βˆͺ π‘₯) β‰  (inrβ€˜π‘§)
138137nesymi 2403 . . . . . . . . 9 Β¬ (inrβ€˜π‘§) = (inlβ€˜βˆͺ π‘₯)
13973, 111eqeqan12rd 2204 . . . . . . . . 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 2605 . . . . . 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 6090 . 2 (⊀ β†’ 𝐹:ω–1-1-ontoβ†’(Ο‰ βŠ” 1o))
151150mptru 1372 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 1363  βŠ€wtru 1364   ∈ wcel 2158   β‰  wne 2357  βˆƒwrex 2466  Vcvv 2749   βŠ† wss 3141  βˆ…c0 3434  ifcif 3546  βˆͺ cuni 3821   ↦ cmpt 4076   I cid 4300  Oncon0 4375  suc csuc 4377  Ο‰com 4601   β†Ύ cres 4640  Fun wfun 5222   Fn wfn 5223  βŸΆwf 5224  β€“1-1-ontoβ†’wf1o 5227  β€˜cfv 5228  1oc1o 6424   βŠ” cdju 7050  inlcinl 7058  inrcinr 7059  casecdjucase 7096
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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2160  ax-14 2161  ax-ext 2169  ax-sep 4133  ax-nul 4141  ax-pow 4186  ax-pr 4221  ax-un 4445  ax-setind 4548  ax-iinf 4599
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3an 981  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ne 2358  df-ral 2470  df-rex 2471  df-rab 2474  df-v 2751  df-sbc 2975  df-csb 3070  df-dif 3143  df-un 3145  df-in 3147  df-ss 3154  df-nul 3435  df-if 3547  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-int 3857  df-br 4016  df-opab 4077  df-mpt 4078  df-tr 4114  df-id 4305  df-iord 4378  df-on 4380  df-suc 4383  df-iom 4602  df-xp 4644  df-rel 4645  df-cnv 4646  df-co 4647  df-dm 4648  df-rn 4649  df-res 4650  df-ima 4651  df-iota 5190  df-fun 5230  df-fn 5231  df-f 5232  df-f1 5233  df-fo 5234  df-f1o 5235  df-fv 5236  df-1st 6155  df-2nd 6156  df-1o 6431  df-dju 7051  df-inl 7060  df-inr 7061  df-case 7097
This theorem is referenced by:  omp1eom  7108
  Copyright terms: Public domain W3C validator