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

Theorem omp1eomlem 6986
Description: Lemma for omp1eom 6987. (Contributed by Jim Kingdon, 11-Jul-2023.)
Hypotheses
Ref Expression
omp1eom.f  |-  F  =  ( x  e.  om  |->  if ( x  =  (/) ,  (inr `  x ) ,  (inl `  U. x ) ) )
omp1eom.s  |-  S  =  ( x  e.  om  |->  suc  x )
omp1eom.g  |-  G  = case ( S ,  (  _I  |`  1o )
)
Assertion
Ref Expression
omp1eomlem  |-  F : om
-1-1-onto-> ( om 1o )
Distinct variable group:    x, G
Allowed substitution hints:    S( x)    F( x)

Proof of Theorem omp1eomlem
Dummy variables  z  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 omp1eom.f . . 3  |-  F  =  ( x  e.  om  |->  if ( x  =  (/) ,  (inr `  x ) ,  (inl `  U. x ) ) )
2 el1o 6341 . . . . . . 7  |-  ( x  e.  1o  <->  x  =  (/) )
32biimpri 132 . . . . . 6  |-  ( x  =  (/)  ->  x  e.  1o )
43adantl 275 . . . . 5  |-  ( ( ( T.  /\  x  e.  om )  /\  x  =  (/) )  ->  x  e.  1o )
5 djurcl 6944 . . . . 5  |-  ( x  e.  1o  ->  (inr `  x )  e.  ( om 1o ) )
64, 5syl 14 . . . 4  |-  ( ( ( T.  /\  x  e.  om )  /\  x  =  (/) )  ->  (inr `  x )  e.  ( om 1o ) )
7 nnpredcl 4543 . . . . . 6  |-  ( x  e.  om  ->  U. x  e.  om )
87ad2antlr 481 . . . . 5  |-  ( ( ( T.  /\  x  e.  om )  /\  -.  x  =  (/) )  ->  U. x  e.  om )
9 djulcl 6943 . . . . 5  |-  ( U. x  e.  om  ->  (inl
`  U. x )  e.  ( om 1o ) )
108, 9syl 14 . . . 4  |-  ( ( ( T.  /\  x  e.  om )  /\  -.  x  =  (/) )  -> 
(inl `  U. x )  e.  ( om 1o ) )
11 nndceq0 4538 . . . . 5  |-  ( x  e.  om  -> DECID  x  =  (/) )
1211adantl 275 . . . 4  |-  ( ( T.  /\  x  e. 
om )  -> DECID  x  =  (/) )
136, 10, 12ifcldadc 3505 . . 3  |-  ( ( T.  /\  x  e. 
om )  ->  if ( x  =  (/) ,  (inr
`  x ) ,  (inl `  U. x ) )  e.  ( om 1o ) )
14 omp1eom.s . . . . . . . 8  |-  S  =  ( x  e.  om  |->  suc  x )
15 peano2 4516 . . . . . . . 8  |-  ( x  e.  om  ->  suc  x  e.  om )
1614, 15fmpti 5579 . . . . . . 7  |-  S : om
--> om
1716a1i 9 . . . . . 6  |-  ( T. 
->  S : om --> om )
18 f1oi 5412 . . . . . . . . 9  |-  (  _I  |`  1o ) : 1o -1-1-onto-> 1o
19 f1of 5374 . . . . . . . . 9  |-  ( (  _I  |`  1o ) : 1o -1-1-onto-> 1o  ->  (  _I  |`  1o ) : 1o --> 1o )
2018, 19ax-mp 5 . . . . . . . 8  |-  (  _I  |`  1o ) : 1o --> 1o
21 1onn 6423 . . . . . . . . 9  |-  1o  e.  om
22 omelon 4529 . . . . . . . . . 10  |-  om  e.  On
2322onelssi 4358 . . . . . . . . 9  |-  ( 1o  e.  om  ->  1o  C_ 
om )
2421, 23ax-mp 5 . . . . . . . 8  |-  1o  C_  om
25 fss 5291 . . . . . . . 8  |-  ( ( (  _I  |`  1o ) : 1o --> 1o  /\  1o  C_  om )  -> 
(  _I  |`  1o ) : 1o --> om )
2620, 24, 25mp2an 423 . . . . . . 7  |-  (  _I  |`  1o ) : 1o --> om
2726a1i 9 . . . . . 6  |-  ( T. 
->  (  _I  |`  1o ) : 1o --> om )
2817, 27casef 6980 . . . . 5  |-  ( T. 
-> case ( S ,  (  _I  |`  1o )
) : ( om 1o ) --> om )
29 omp1eom.g . . . . . 6  |-  G  = case ( S ,  (  _I  |`  1o )
)
3029feq1i 5272 . . . . 5  |-  ( G : ( om 1o ) --> om  <-> case ( S ,  (  _I  |`  1o )
) : ( om 1o ) --> om )
3128, 30sylibr 133 . . . 4  |-  ( T. 
->  G : ( om 1o ) --> om )
3231ffvelrnda 5562 . . 3  |-  ( ( T.  /\  y  e.  ( om 1o ) )  ->  ( G `  y )  e.  om )
33 ffn 5279 . . . . . . . . . . . . . . . 16  |-  ( S : om --> om  ->  S  Fn  om )
3416, 33mp1i 10 . . . . . . . . . . . . . . 15  |-  ( ( z  e.  om  /\  y  =  (inl `  z
) )  ->  S  Fn  om )
35 ffun 5282 . . . . . . . . . . . . . . . 16  |-  ( (  _I  |`  1o ) : 1o --> 1o  ->  Fun  (  _I  |`  1o ) )
3620, 35mp1i 10 . . . . . . . . . . . . . . 15  |-  ( ( z  e.  om  /\  y  =  (inl `  z
) )  ->  Fun  (  _I  |`  1o ) )
37 simpl 108 . . . . . . . . . . . . . . 15  |-  ( ( z  e.  om  /\  y  =  (inl `  z
) )  ->  z  e.  om )
3834, 36, 37caseinl 6983 . . . . . . . . . . . . . 14  |-  ( ( z  e.  om  /\  y  =  (inl `  z
) )  ->  (case ( S ,  (  _I  |`  1o ) ) `  (inl `  z ) )  =  ( S `  z ) )
3929eqcomi 2144 . . . . . . . . . . . . . . . 16  |- case ( S ,  (  _I  |`  1o ) )  =  G
4039a1i 9 . . . . . . . . . . . . . . 15  |-  ( ( z  e.  om  /\  y  =  (inl `  z
) )  -> case ( S ,  (  _I  |`  1o ) )  =  G )
41 simpr 109 . . . . . . . . . . . . . . . 16  |-  ( ( z  e.  om  /\  y  =  (inl `  z
) )  ->  y  =  (inl `  z )
)
4241eqcomd 2146 . . . . . . . . . . . . . . 15  |-  ( ( z  e.  om  /\  y  =  (inl `  z
) )  ->  (inl `  z )  =  y )
4340, 42fveq12d 5435 . . . . . . . . . . . . . 14  |-  ( ( z  e.  om  /\  y  =  (inl `  z
) )  ->  (case ( S ,  (  _I  |`  1o ) ) `  (inl `  z ) )  =  ( G `  y ) )
44 peano2 4516 . . . . . . . . . . . . . . . 16  |-  ( z  e.  om  ->  suc  z  e.  om )
45 suceq 4331 . . . . . . . . . . . . . . . . 17  |-  ( x  =  z  ->  suc  x  =  suc  z )
4645, 14fvmptg 5504 . . . . . . . . . . . . . . . 16  |-  ( ( z  e.  om  /\  suc  z  e.  om )  ->  ( S `  z )  =  suc  z )
4744, 46mpdan 418 . . . . . . . . . . . . . . 15  |-  ( z  e.  om  ->  ( S `  z )  =  suc  z )
4847adantr 274 . . . . . . . . . . . . . 14  |-  ( ( z  e.  om  /\  y  =  (inl `  z
) )  ->  ( S `  z )  =  suc  z )
4938, 43, 483eqtr3d 2181 . . . . . . . . . . . . 13  |-  ( ( z  e.  om  /\  y  =  (inl `  z
) )  ->  ( G `  y )  =  suc  z )
50 peano3 4517 . . . . . . . . . . . . . 14  |-  ( z  e.  om  ->  suc  z  =/=  (/) )
5150adantr 274 . . . . . . . . . . . . 13  |-  ( ( z  e.  om  /\  y  =  (inl `  z
) )  ->  suc  z  =/=  (/) )
5249, 51eqnetrd 2333 . . . . . . . . . . . 12  |-  ( ( z  e.  om  /\  y  =  (inl `  z
) )  ->  ( G `  y )  =/=  (/) )
5352adantl 275 . . . . . . . . . . 11  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  x  =  (/) )  /\  ( z  e.  om  /\  y  =  (inl `  z ) ) )  ->  ( G `  y )  =/=  (/) )
5453necomd 2395 . . . . . . . . . 10  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  x  =  (/) )  /\  ( z  e.  om  /\  y  =  (inl `  z ) ) )  ->  (/)  =/=  ( G `
 y ) )
5554neneqd 2330 . . . . . . . . 9  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  x  =  (/) )  /\  ( z  e.  om  /\  y  =  (inl `  z ) ) )  ->  -.  (/)  =  ( G `  y ) )
56 simplr 520 . . . . . . . . . 10  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  x  =  (/) )  /\  ( z  e.  om  /\  y  =  (inl `  z ) ) )  ->  x  =  (/) )
5756eqeq1d 2149 . . . . . . . . 9  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  x  =  (/) )  /\  ( z  e.  om  /\  y  =  (inl `  z ) ) )  ->  ( x  =  ( G `  y
)  <->  (/)  =  ( G `
 y ) ) )
5855, 57mtbird 663 . . . . . . . 8  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  x  =  (/) )  /\  ( z  e.  om  /\  y  =  (inl `  z ) ) )  ->  -.  x  =  ( G `  y ) )
59 djune 6970 . . . . . . . . . . . 12  |-  ( ( z  e.  _V  /\  x  e.  _V )  ->  (inl `  z )  =/=  (inr `  x )
)
6059elvd 2694 . . . . . . . . . . 11  |-  ( z  e.  _V  ->  (inl `  z )  =/=  (inr `  x ) )
6160elv 2693 . . . . . . . . . 10  |-  (inl `  z )  =/=  (inr `  x )
6261neii 2311 . . . . . . . . 9  |-  -.  (inl `  z )  =  (inr
`  x )
63 simprr 522 . . . . . . . . . 10  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  x  =  (/) )  /\  ( z  e.  om  /\  y  =  (inl `  z ) ) )  ->  y  =  (inl
`  z ) )
64 simpr 109 . . . . . . . . . . . 12  |-  ( ( ( x  e.  om  /\  y  e.  ( om 1o ) )  /\  x  =  (/) )  ->  x  =  (/) )
6564iftrued 3485 . . . . . . . . . . 11  |-  ( ( ( x  e.  om  /\  y  e.  ( om 1o ) )  /\  x  =  (/) )  ->  if ( x  =  (/) ,  (inr
`  x ) ,  (inl `  U. x ) )  =  (inr `  x ) )
6665adantr 274 . . . . . . . . . 10  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  x  =  (/) )  /\  ( z  e.  om  /\  y  =  (inl `  z ) ) )  ->  if ( x  =  (/) ,  (inr `  x ) ,  (inl
`  U. x ) )  =  (inr `  x
) )
6763, 66eqeq12d 2155 . . . . . . . . 9  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  x  =  (/) )  /\  ( z  e.  om  /\  y  =  (inl `  z ) ) )  ->  ( y  =  if ( x  =  (/) ,  (inr `  x
) ,  (inl `  U. x ) )  <->  (inl `  z
)  =  (inr `  x ) ) )
6862, 67mtbiri 665 . . . . . . . 8  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  x  =  (/) )  /\  ( z  e.  om  /\  y  =  (inl `  z ) ) )  ->  -.  y  =  if ( x  =  (/) ,  (inr `  x ) ,  (inl `  U. x ) ) )
6958, 682falsed 692 . . . . . . 7  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  x  =  (/) )  /\  ( z  e.  om  /\  y  =  (inl `  z ) ) )  ->  ( x  =  ( G `  y
)  <->  y  =  if ( x  =  (/) ,  (inr `  x ) ,  (inl `  U. x ) ) ) )
7069rexlimdvaa 2553 . . . . . 6  |-  ( ( ( x  e.  om  /\  y  e.  ( om 1o ) )  /\  x  =  (/) )  ->  ( E. z  e.  om  y  =  (inl `  z
)  ->  ( x  =  ( G `  y )  <->  y  =  if ( x  =  (/) ,  (inr `  x ) ,  (inl `  U. x ) ) ) ) )
71 simplr 520 . . . . . . . . 9  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  x  =  (/) )  /\  ( z  e.  1o  /\  y  =  (inr `  z ) ) )  ->  x  =  (/) )
7229a1i 9 . . . . . . . . . . . 12  |-  ( ( z  e.  1o  /\  y  =  (inr `  z
) )  ->  G  = case ( S ,  (  _I  |`  1o )
) )
73 simpr 109 . . . . . . . . . . . 12  |-  ( ( z  e.  1o  /\  y  =  (inr `  z
) )  ->  y  =  (inr `  z )
)
7472, 73fveq12d 5435 . . . . . . . . . . 11  |-  ( ( z  e.  1o  /\  y  =  (inr `  z
) )  ->  ( G `  y )  =  (case ( S , 
(  _I  |`  1o ) ) `  (inr `  z ) ) )
7514funmpt2 5169 . . . . . . . . . . . . . 14  |-  Fun  S
7675a1i 9 . . . . . . . . . . . . 13  |-  ( ( z  e.  1o  /\  y  =  (inr `  z
) )  ->  Fun  S )
77 fnresi 5247 . . . . . . . . . . . . . 14  |-  (  _I  |`  1o )  Fn  1o
7877a1i 9 . . . . . . . . . . . . 13  |-  ( ( z  e.  1o  /\  y  =  (inr `  z
) )  ->  (  _I  |`  1o )  Fn  1o )
79 simpl 108 . . . . . . . . . . . . 13  |-  ( ( z  e.  1o  /\  y  =  (inr `  z
) )  ->  z  e.  1o )
8076, 78, 79caseinr 6984 . . . . . . . . . . . 12  |-  ( ( z  e.  1o  /\  y  =  (inr `  z
) )  ->  (case ( S ,  (  _I  |`  1o ) ) `  (inr `  z ) )  =  ( (  _I  |`  1o ) `  z
) )
81 fvresi 5620 . . . . . . . . . . . . 13  |-  ( z  e.  1o  ->  (
(  _I  |`  1o ) `
 z )  =  z )
8281adantr 274 . . . . . . . . . . . 12  |-  ( ( z  e.  1o  /\  y  =  (inr `  z
) )  ->  (
(  _I  |`  1o ) `
 z )  =  z )
8380, 82eqtrd 2173 . . . . . . . . . . 11  |-  ( ( z  e.  1o  /\  y  =  (inr `  z
) )  ->  (case ( S ,  (  _I  |`  1o ) ) `  (inr `  z ) )  =  z )
84 el1o 6341 . . . . . . . . . . . 12  |-  ( z  e.  1o  <->  z  =  (/) )
8579, 84sylib 121 . . . . . . . . . . 11  |-  ( ( z  e.  1o  /\  y  =  (inr `  z
) )  ->  z  =  (/) )
8674, 83, 853eqtrd 2177 . . . . . . . . . 10  |-  ( ( z  e.  1o  /\  y  =  (inr `  z
) )  ->  ( G `  y )  =  (/) )
8786adantl 275 . . . . . . . . 9  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  x  =  (/) )  /\  ( z  e.  1o  /\  y  =  (inr `  z ) ) )  ->  ( G `  y )  =  (/) )
8871, 87eqtr4d 2176 . . . . . . . 8  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  x  =  (/) )  /\  ( z  e.  1o  /\  y  =  (inr `  z ) ) )  ->  x  =  ( G `  y ) )
8985adantl 275 . . . . . . . . . . 11  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  x  =  (/) )  /\  ( z  e.  1o  /\  y  =  (inr `  z ) ) )  ->  z  =  (/) )
9071, 89eqtr4d 2176 . . . . . . . . . 10  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  x  =  (/) )  /\  ( z  e.  1o  /\  y  =  (inr `  z ) ) )  ->  x  =  z )
9190fveq2d 5432 . . . . . . . . 9  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  x  =  (/) )  /\  ( z  e.  1o  /\  y  =  (inr `  z ) ) )  ->  (inr `  x
)  =  (inr `  z ) )
9265adantr 274 . . . . . . . . 9  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  x  =  (/) )  /\  ( z  e.  1o  /\  y  =  (inr `  z ) ) )  ->  if ( x  =  (/) ,  (inr `  x ) ,  (inl
`  U. x ) )  =  (inr `  x
) )
93 simprr 522 . . . . . . . . 9  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  x  =  (/) )  /\  ( z  e.  1o  /\  y  =  (inr `  z ) ) )  ->  y  =  (inr
`  z ) )
9491, 92, 933eqtr4rd 2184 . . . . . . . 8  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  x  =  (/) )  /\  ( z  e.  1o  /\  y  =  (inr `  z ) ) )  ->  y  =  if ( x  =  (/) ,  (inr `  x ) ,  (inl `  U. x ) ) )
9588, 942thd 174 . . . . . . 7  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  x  =  (/) )  /\  ( z  e.  1o  /\  y  =  (inr `  z ) ) )  ->  ( x  =  ( G `  y
)  <->  y  =  if ( x  =  (/) ,  (inr `  x ) ,  (inl `  U. x ) ) ) )
9695rexlimdvaa 2553 . . . . . 6  |-  ( ( ( x  e.  om  /\  y  e.  ( om 1o ) )  /\  x  =  (/) )  ->  ( E. z  e.  1o  y  =  (inr `  z
)  ->  ( x  =  ( G `  y )  <->  y  =  if ( x  =  (/) ,  (inr `  x ) ,  (inl `  U. x ) ) ) ) )
97 djur 6961 . . . . . . . 8  |-  ( y  e.  ( om 1o )  <-> 
( E. z  e. 
om  y  =  (inl
`  z )  \/ 
E. z  e.  1o  y  =  (inr `  z
) ) )
9897biimpi 119 . . . . . . 7  |-  ( y  e.  ( om 1o )  ->  ( E. z  e.  om  y  =  (inl
`  z )  \/ 
E. z  e.  1o  y  =  (inr `  z
) ) )
9998ad2antlr 481 . . . . . 6  |-  ( ( ( x  e.  om  /\  y  e.  ( om 1o ) )  /\  x  =  (/) )  ->  ( E. z  e.  om  y  =  (inl `  z
)  \/  E. z  e.  1o  y  =  (inr
`  z ) ) )
10070, 96, 99mpjaod 708 . . . . 5  |-  ( ( ( x  e.  om  /\  y  e.  ( om 1o ) )  /\  x  =  (/) )  ->  (
x  =  ( G `
 y )  <->  y  =  if ( x  =  (/) ,  (inr `  x ) ,  (inl `  U. x ) ) ) )
101 simplll 523 . . . . . . . . . . 11  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  -.  x  =  (/) )  /\  ( z  e.  om  /\  y  =  (inl `  z ) ) )  ->  x  e.  om )
102 simplr 520 . . . . . . . . . . . 12  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  -.  x  =  (/) )  /\  ( z  e.  om  /\  y  =  (inl `  z ) ) )  ->  -.  x  =  (/) )
103102neqned 2316 . . . . . . . . . . 11  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  -.  x  =  (/) )  /\  ( z  e.  om  /\  y  =  (inl `  z ) ) )  ->  x  =/=  (/) )
104 nnsucpred 4537 . . . . . . . . . . 11  |-  ( ( x  e.  om  /\  x  =/=  (/) )  ->  suc  U. x  =  x )
105101, 103, 104syl2anc 409 . . . . . . . . . 10  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  -.  x  =  (/) )  /\  ( z  e.  om  /\  y  =  (inl `  z ) ) )  ->  suc  U. x  =  x )
106105eqeq2d 2152 . . . . . . . . 9  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  -.  x  =  (/) )  /\  ( z  e.  om  /\  y  =  (inl `  z ) ) )  ->  ( suc  z  =  suc  U. x  <->  suc  z  =  x ) )
107 eqcom 2142 . . . . . . . . 9  |-  ( suc  z  =  x  <->  x  =  suc  z )
108106, 107syl6bb 195 . . . . . . . 8  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  -.  x  =  (/) )  /\  ( z  e.  om  /\  y  =  (inl `  z ) ) )  ->  ( suc  z  =  suc  U. x  <->  x  =  suc  z ) )
109 simprr 522 . . . . . . . . . . 11  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  -.  x  =  (/) )  /\  ( z  e.  om  /\  y  =  (inl `  z ) ) )  ->  y  =  (inl
`  z ) )
110 simpr 109 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  om  /\  y  e.  ( om 1o ) )  /\  -.  x  =  (/) )  ->  -.  x  =  (/) )
111110iffalsed 3488 . . . . . . . . . . . 12  |-  ( ( ( x  e.  om  /\  y  e.  ( om 1o ) )  /\  -.  x  =  (/) )  ->  if ( x  =  (/) ,  (inr `  x ) ,  (inl `  U. x ) )  =  (inl `  U. x ) )
112111adantr 274 . . . . . . . . . . 11  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  -.  x  =  (/) )  /\  ( z  e.  om  /\  y  =  (inl `  z ) ) )  ->  if ( x  =  (/) ,  (inr `  x ) ,  (inl
`  U. x ) )  =  (inl `  U. x ) )
113109, 112eqeq12d 2155 . . . . . . . . . 10  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  -.  x  =  (/) )  /\  ( z  e.  om  /\  y  =  (inl `  z ) ) )  ->  ( y  =  if ( x  =  (/) ,  (inr `  x
) ,  (inl `  U. x ) )  <->  (inl `  z
)  =  (inl `  U. x ) ) )
114 vuniex 4367 . . . . . . . . . . . 12  |-  U. x  e.  _V
115 inl11 6957 . . . . . . . . . . . 12  |-  ( ( z  e.  _V  /\  U. x  e.  _V )  ->  ( (inl `  z
)  =  (inl `  U. x )  <->  z  =  U. x ) )
116114, 115mpan2 422 . . . . . . . . . . 11  |-  ( z  e.  _V  ->  (
(inl `  z )  =  (inl `  U. x )  <-> 
z  =  U. x
) )
117116elv 2693 . . . . . . . . . 10  |-  ( (inl
`  z )  =  (inl `  U. x )  <-> 
z  =  U. x
)
118113, 117syl6bb 195 . . . . . . . . 9  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  -.  x  =  (/) )  /\  ( z  e.  om  /\  y  =  (inl `  z ) ) )  ->  ( y  =  if ( x  =  (/) ,  (inr `  x
) ,  (inl `  U. x ) )  <->  z  =  U. x ) )
119 nnon 4530 . . . . . . . . . . 11  |-  ( z  e.  om  ->  z  e.  On )
120119ad2antrl 482 . . . . . . . . . 10  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  -.  x  =  (/) )  /\  ( z  e.  om  /\  y  =  (inl `  z ) ) )  ->  z  e.  On )
1217ad3antrrr 484 . . . . . . . . . . 11  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  -.  x  =  (/) )  /\  ( z  e.  om  /\  y  =  (inl `  z ) ) )  ->  U. x  e.  om )
122 nnon 4530 . . . . . . . . . . 11  |-  ( U. x  e.  om  ->  U. x  e.  On )
123121, 122syl 14 . . . . . . . . . 10  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  -.  x  =  (/) )  /\  ( z  e.  om  /\  y  =  (inl `  z ) ) )  ->  U. x  e.  On )
124 suc11 4480 . . . . . . . . . 10  |-  ( ( z  e.  On  /\  U. x  e.  On )  ->  ( suc  z  =  suc  U. x  <->  z  =  U. x ) )
125120, 123, 124syl2anc 409 . . . . . . . . 9  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  -.  x  =  (/) )  /\  ( z  e.  om  /\  y  =  (inl `  z ) ) )  ->  ( suc  z  =  suc  U. x  <->  z  =  U. x ) )
126118, 125bitr4d 190 . . . . . . . 8  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  -.  x  =  (/) )  /\  ( z  e.  om  /\  y  =  (inl `  z ) ) )  ->  ( y  =  if ( x  =  (/) ,  (inr `  x
) ,  (inl `  U. x ) )  <->  suc  z  =  suc  U. x ) )
12749adantl 275 . . . . . . . . 9  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  -.  x  =  (/) )  /\  ( z  e.  om  /\  y  =  (inl `  z ) ) )  ->  ( G `  y )  =  suc  z )
128127eqeq2d 2152 . . . . . . . 8  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  -.  x  =  (/) )  /\  ( z  e.  om  /\  y  =  (inl `  z ) ) )  ->  ( x  =  ( G `  y
)  <->  x  =  suc  z ) )
129108, 126, 1283bitr4rd 220 . . . . . . 7  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  -.  x  =  (/) )  /\  ( z  e.  om  /\  y  =  (inl `  z ) ) )  ->  ( x  =  ( G `  y
)  <->  y  =  if ( x  =  (/) ,  (inr `  x ) ,  (inl `  U. x ) ) ) )
130129rexlimdvaa 2553 . . . . . 6  |-  ( ( ( x  e.  om  /\  y  e.  ( om 1o ) )  /\  -.  x  =  (/) )  -> 
( E. z  e. 
om  y  =  (inl
`  z )  -> 
( x  =  ( G `  y )  <-> 
y  =  if ( x  =  (/) ,  (inr
`  x ) ,  (inl `  U. x ) ) ) ) )
131 simplr 520 . . . . . . . . 9  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  -.  x  =  (/) )  /\  ( z  e.  1o  /\  y  =  (inr `  z ) ) )  ->  -.  x  =  (/) )
13286adantl 275 . . . . . . . . . 10  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  -.  x  =  (/) )  /\  ( z  e.  1o  /\  y  =  (inr `  z ) ) )  ->  ( G `  y )  =  (/) )
133132eqeq2d 2152 . . . . . . . . 9  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  -.  x  =  (/) )  /\  ( z  e.  1o  /\  y  =  (inr `  z ) ) )  ->  ( x  =  ( G `  y
)  <->  x  =  (/) ) )
134131, 133mtbird 663 . . . . . . . 8  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  -.  x  =  (/) )  /\  ( z  e.  1o  /\  y  =  (inr `  z ) ) )  ->  -.  x  =  ( G `  y ) )
135 djune 6970 . . . . . . . . . . . 12  |-  ( ( U. x  e.  _V  /\  z  e.  _V )  ->  (inl `  U. x )  =/=  (inr `  z
) )
136135elvd 2694 . . . . . . . . . . 11  |-  ( U. x  e.  _V  ->  (inl
`  U. x )  =/=  (inr `  z )
)
137114, 136ax-mp 5 . . . . . . . . . 10  |-  (inl `  U. x )  =/=  (inr `  z )
138137nesymi 2355 . . . . . . . . 9  |-  -.  (inr `  z )  =  (inl
`  U. x )
13973, 111eqeqan12rd 2157 . . . . . . . . 9  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  -.  x  =  (/) )  /\  ( z  e.  1o  /\  y  =  (inr `  z ) ) )  ->  ( y  =  if ( x  =  (/) ,  (inr `  x
) ,  (inl `  U. x ) )  <->  (inr `  z
)  =  (inl `  U. x ) ) )
140138, 139mtbiri 665 . . . . . . . 8  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  -.  x  =  (/) )  /\  ( z  e.  1o  /\  y  =  (inr `  z ) ) )  ->  -.  y  =  if ( x  =  (/) ,  (inr `  x ) ,  (inl `  U. x ) ) )
141134, 1402falsed 692 . . . . . . 7  |-  ( ( ( ( x  e. 
om  /\  y  e.  ( om 1o ) )  /\  -.  x  =  (/) )  /\  ( z  e.  1o  /\  y  =  (inr `  z ) ) )  ->  ( x  =  ( G `  y
)  <->  y  =  if ( x  =  (/) ,  (inr `  x ) ,  (inl `  U. x ) ) ) )
142141rexlimdvaa 2553 . . . . . 6  |-  ( ( ( x  e.  om  /\  y  e.  ( om 1o ) )  /\  -.  x  =  (/) )  -> 
( E. z  e.  1o  y  =  (inr
`  z )  -> 
( x  =  ( G `  y )  <-> 
y  =  if ( x  =  (/) ,  (inr
`  x ) ,  (inl `  U. x ) ) ) ) )
14398ad2antlr 481 . . . . . 6  |-  ( ( ( x  e.  om  /\  y  e.  ( om 1o ) )  /\  -.  x  =  (/) )  -> 
( E. z  e. 
om  y  =  (inl
`  z )  \/ 
E. z  e.  1o  y  =  (inr `  z
) ) )
144130, 142, 143mpjaod 708 . . . . 5  |-  ( ( ( x  e.  om  /\  y  e.  ( om 1o ) )  /\  -.  x  =  (/) )  -> 
( x  =  ( G `  y )  <-> 
y  =  if ( x  =  (/) ,  (inr
`  x ) ,  (inl `  U. x ) ) ) )
145 exmiddc 822 . . . . . . 7  |-  (DECID  x  =  (/)  ->  ( x  =  (/)  \/  -.  x  =  (/) ) )
14611, 145syl 14 . . . . . 6  |-  ( x  e.  om  ->  (
x  =  (/)  \/  -.  x  =  (/) ) )
147146adantr 274 . . . . 5  |-  ( ( x  e.  om  /\  y  e.  ( om 1o ) )  ->  (
x  =  (/)  \/  -.  x  =  (/) ) )
148100, 144, 147mpjaodan 788 . . . 4  |-  ( ( x  e.  om  /\  y  e.  ( om 1o ) )  ->  (
x  =  ( G `
 y )  <->  y  =  if ( x  =  (/) ,  (inr `  x ) ,  (inl `  U. x ) ) ) )
149148adantl 275 . . 3  |-  ( ( T.  /\  ( x  e.  om  /\  y  e.  ( om 1o ) ) )  ->  ( x  =  ( G `  y )  <->  y  =  if ( x  =  (/) ,  (inr `  x ) ,  (inl `  U. x ) ) ) )
1501, 13, 32, 149f1o2d 5982 . 2  |-  ( T. 
->  F : om -1-1-onto-> ( om 1o ) )
151150mptru 1341 1  |-  F : om
-1-1-onto-> ( om 1o )
Colors of variables: wff set class
Syntax hints:   -. wn 3    /\ wa 103    <-> wb 104    \/ wo 698  DECID wdc 820    = wceq 1332   T. wtru 1333    e. wcel 1481    =/= wne 2309   E.wrex 2418   _Vcvv 2689    C_ wss 3075   (/)c0 3367   ifcif 3478   U.cuni 3743    |-> cmpt 3996    _I cid 4217   Oncon0 4292   suc csuc 4294   omcom 4511    |` cres 4548   Fun wfun 5124    Fn wfn 5125   -->wf 5126   -1-1-onto->wf1o 5129   ` cfv 5130   1oc1o 6313   ⊔ cdju 6929  inlcinl 6937  inrcinr 6938  casecdjucase 6975
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 4053  ax-nul 4061  ax-pow 4105  ax-pr 4138  ax-un 4362  ax-setind 4459  ax-iinf 4509
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 2913  df-csb 3007  df-dif 3077  df-un 3079  df-in 3081  df-ss 3088  df-nul 3368  df-if 3479  df-pw 3516  df-sn 3537  df-pr 3538  df-op 3540  df-uni 3744  df-int 3779  df-br 3937  df-opab 3997  df-mpt 3998  df-tr 4034  df-id 4222  df-iord 4295  df-on 4297  df-suc 4300  df-iom 4512  df-xp 4552  df-rel 4553  df-cnv 4554  df-co 4555  df-dm 4556  df-rn 4557  df-res 4558  df-ima 4559  df-iota 5095  df-fun 5132  df-fn 5133  df-f 5134  df-f1 5135  df-fo 5136  df-f1o 5137  df-fv 5138  df-1st 6045  df-2nd 6046  df-1o 6320  df-dju 6930  df-inl 6939  df-inr 6940  df-case 6976
This theorem is referenced by:  omp1eom  6987
  Copyright terms: Public domain W3C validator