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

Theorem ctiunctlemfo 11847
Description: Lemma for ctiunct 11848. (Contributed by Jim Kingdon, 28-Oct-2023.)
Hypotheses
Ref Expression
ctiunct.som  |-  ( ph  ->  S  C_  om )
ctiunct.sdc  |-  ( ph  ->  A. n  e.  om DECID  n  e.  S )
ctiunct.f  |-  ( ph  ->  F : S -onto-> A
)
ctiunct.tom  |-  ( (
ph  /\  x  e.  A )  ->  T  C_ 
om )
ctiunct.tdc  |-  ( (
ph  /\  x  e.  A )  ->  A. n  e.  om DECID  n  e.  T )
ctiunct.g  |-  ( (
ph  /\  x  e.  A )  ->  G : T -onto-> B )
ctiunct.j  |-  ( ph  ->  J : om -1-1-onto-> ( om  X.  om ) )
ctiunct.u  |-  U  =  { z  e.  om  |  ( ( 1st `  ( J `  z
) )  e.  S  /\  ( 2nd `  ( J `  z )
)  e.  [_ ( F `  ( 1st `  ( J `  z
) ) )  /  x ]_ T ) }
ctiunct.h  |-  H  =  ( n  e.  U  |->  ( [_ ( F `
 ( 1st `  ( J `  n )
) )  /  x ]_ G `  ( 2nd `  ( J `  n
) ) ) )
ctiunct.nfh  |-  F/_ x H
ctiunct.nfu  |-  F/_ x U
Assertion
Ref Expression
ctiunctlemfo  |-  ( ph  ->  H : U -onto-> U_ x  e.  A  B
)
Distinct variable groups:    A, n, x    B, n    n, F, x, z    n, G    n, J, x, z    z, S   
z, T    U, n    ph, n, x    z, n
Allowed substitution hints:    ph( z)    A( z)    B( x, z)    S( x, n)    T( x, n)    U( x, z)    G( x, z)    H( x, z, n)

Proof of Theorem ctiunctlemfo
Dummy variables  r  w  u  v are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ctiunct.som . . 3  |-  ( ph  ->  S  C_  om )
2 ctiunct.sdc . . 3  |-  ( ph  ->  A. n  e.  om DECID  n  e.  S )
3 ctiunct.f . . 3  |-  ( ph  ->  F : S -onto-> A
)
4 ctiunct.tom . . 3  |-  ( (
ph  /\  x  e.  A )  ->  T  C_ 
om )
5 ctiunct.tdc . . 3  |-  ( (
ph  /\  x  e.  A )  ->  A. n  e.  om DECID  n  e.  T )
6 ctiunct.g . . 3  |-  ( (
ph  /\  x  e.  A )  ->  G : T -onto-> B )
7 ctiunct.j . . 3  |-  ( ph  ->  J : om -1-1-onto-> ( om  X.  om ) )
8 ctiunct.u . . 3  |-  U  =  { z  e.  om  |  ( ( 1st `  ( J `  z
) )  e.  S  /\  ( 2nd `  ( J `  z )
)  e.  [_ ( F `  ( 1st `  ( J `  z
) ) )  /  x ]_ T ) }
9 ctiunct.h . . 3  |-  H  =  ( n  e.  U  |->  ( [_ ( F `
 ( 1st `  ( J `  n )
) )  /  x ]_ G `  ( 2nd `  ( J `  n
) ) ) )
101, 2, 3, 4, 5, 6, 7, 8, 9ctiunctlemf 11846 . 2  |-  ( ph  ->  H : U --> U_ x  e.  A  B )
11 nfv 1491 . . . . 5  |-  F/ x ph
12 nfiu1 3811 . . . . . 6  |-  F/_ x U_ x  e.  A  B
1312nfcri 2250 . . . . 5  |-  F/ x  u  e.  U_ x  e.  A  B
1411, 13nfan 1527 . . . 4  |-  F/ x
( ph  /\  u  e.  U_ x  e.  A  B )
15 ctiunct.nfu . . . . 5  |-  F/_ x U
16 ctiunct.nfh . . . . . . 7  |-  F/_ x H
17 nfcv 2256 . . . . . . 7  |-  F/_ x
v
1816, 17nffv 5397 . . . . . 6  |-  F/_ x
( H `  v
)
1918nfeq2 2268 . . . . 5  |-  F/ x  u  =  ( H `  v )
2015, 19nfrexxy 2447 . . . 4  |-  F/ x E. v  e.  U  u  =  ( H `  v )
21 simplll 505 . . . . . . 7  |-  ( ( ( ( ph  /\  u  e.  U_ x  e.  A  B )  /\  x  e.  A )  /\  u  e.  B
)  ->  ph )
22 simplr 502 . . . . . . 7  |-  ( ( ( ( ph  /\  u  e.  U_ x  e.  A  B )  /\  x  e.  A )  /\  u  e.  B
)  ->  x  e.  A )
2321, 22, 6syl2anc 406 . . . . . 6  |-  ( ( ( ( ph  /\  u  e.  U_ x  e.  A  B )  /\  x  e.  A )  /\  u  e.  B
)  ->  G : T -onto-> B )
24 foelrn 5620 . . . . . 6  |-  ( ( G : T -onto-> B  /\  u  e.  B
)  ->  E. w  e.  T  u  =  ( G `  w ) )
2523, 24sylancom 414 . . . . 5  |-  ( ( ( ( ph  /\  u  e.  U_ x  e.  A  B )  /\  x  e.  A )  /\  u  e.  B
)  ->  E. w  e.  T  u  =  ( G `  w ) )
263ad4antr 483 . . . . . . 7  |-  ( ( ( ( ( ph  /\  u  e.  U_ x  e.  A  B )  /\  x  e.  A
)  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  ->  F : S -onto-> A )
27 simpllr 506 . . . . . . 7  |-  ( ( ( ( ( ph  /\  u  e.  U_ x  e.  A  B )  /\  x  e.  A
)  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  ->  x  e.  A
)
28 foelrn 5620 . . . . . . 7  |-  ( ( F : S -onto-> A  /\  x  e.  A
)  ->  E. r  e.  S  x  =  ( F `  r ) )
2926, 27, 28syl2anc 406 . . . . . 6  |-  ( ( ( ( ( ph  /\  u  e.  U_ x  e.  A  B )  /\  x  e.  A
)  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  ->  E. r  e.  S  x  =  ( F `  r ) )
30 f1ocnv 5346 . . . . . . . . . . . 12  |-  ( J : om -1-1-onto-> ( om  X.  om )  ->  `' J :
( om  X.  om )
-1-1-onto-> om )
317, 30syl 14 . . . . . . . . . . 11  |-  ( ph  ->  `' J : ( om 
X.  om ) -1-1-onto-> om )
32 f1of 5333 . . . . . . . . . . 11  |-  ( `' J : ( om 
X.  om ) -1-1-onto-> om  ->  `' J : ( om  X.  om ) --> om )
3331, 32syl 14 . . . . . . . . . 10  |-  ( ph  ->  `' J : ( om 
X.  om ) --> om )
3433ad5antr 485 . . . . . . . . 9  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  ->  `' J : ( om 
X.  om ) --> om )
351ad5antr 485 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  ->  S  C_  om )
36 simprl 503 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  -> 
r  e.  S )
3735, 36sseldd 3066 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  -> 
r  e.  om )
38 simp-5l 515 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  ->  ph )
3927adantr 272 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  ->  x  e.  A )
4038, 39, 4syl2anc 406 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  ->  T  C_  om )
41 simplrl 507 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  ->  w  e.  T )
4240, 41sseldd 3066 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  ->  w  e.  om )
4337, 42opelxpd 4540 . . . . . . . . 9  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  ->  <. r ,  w >.  e.  ( om  X.  om ) )
4434, 43ffvelrnd 5522 . . . . . . . 8  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  -> 
( `' J `  <. r ,  w >. )  e.  om )
4538, 7syl 14 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  ->  J : om -1-1-onto-> ( om  X.  om ) )
46 f1ocnvfv2 5645 . . . . . . . . . . . . 13  |-  ( ( J : om -1-1-onto-> ( om  X.  om )  /\  <. r ,  w >.  e.  ( om  X.  om ) )  ->  ( J `  ( `' J `  <. r ,  w >. ) )  = 
<. r ,  w >. )
4745, 43, 46syl2anc 406 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  -> 
( J `  ( `' J `  <. r ,  w >. ) )  = 
<. r ,  w >. )
4847fveq2d 5391 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  -> 
( 1st `  ( J `  ( `' J `  <. r ,  w >. ) ) )  =  ( 1st `  <. r ,  w >. )
)
49 vex 2661 . . . . . . . . . . . 12  |-  r  e. 
_V
50 vex 2661 . . . . . . . . . . . 12  |-  w  e. 
_V
5149, 50op1st 6010 . . . . . . . . . . 11  |-  ( 1st `  <. r ,  w >. )  =  r
5248, 51syl6eq 2164 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  -> 
( 1st `  ( J `  ( `' J `  <. r ,  w >. ) ) )  =  r )
5352, 36eqeltrd 2192 . . . . . . . . 9  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  -> 
( 1st `  ( J `  ( `' J `  <. r ,  w >. ) ) )  e.  S )
5447fveq2d 5391 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  -> 
( 2nd `  ( J `  ( `' J `  <. r ,  w >. ) ) )  =  ( 2nd `  <. r ,  w >. )
)
5549, 50op2nd 6011 . . . . . . . . . . 11  |-  ( 2nd `  <. r ,  w >. )  =  w
5654, 55syl6eq 2164 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  -> 
( 2nd `  ( J `  ( `' J `  <. r ,  w >. ) ) )  =  w )
5752fveq2d 5391 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  -> 
( F `  ( 1st `  ( J `  ( `' J `  <. r ,  w >. ) ) ) )  =  ( F `
 r ) )
58 simprr 504 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  ->  x  =  ( F `  r ) )
5957, 58eqtr4d 2151 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  -> 
( F `  ( 1st `  ( J `  ( `' J `  <. r ,  w >. ) ) ) )  =  x )
6059csbeq1d 2979 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  ->  [_ ( F `  ( 1st `  ( J `  ( `' J `  <. r ,  w >. ) ) ) )  /  x ]_ T  =  [_ x  /  x ]_ T )
61 csbid 2980 . . . . . . . . . . 11  |-  [_ x  /  x ]_ T  =  T
6260, 61syl6eq 2164 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  ->  [_ ( F `  ( 1st `  ( J `  ( `' J `  <. r ,  w >. ) ) ) )  /  x ]_ T  =  T )
6341, 56, 623eltr4d 2199 . . . . . . . . 9  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  -> 
( 2nd `  ( J `  ( `' J `  <. r ,  w >. ) ) )  e.  [_ ( F `
 ( 1st `  ( J `  ( `' J `  <. r ,  w >. ) ) ) )  /  x ]_ T )
6453, 63jca 302 . . . . . . . 8  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  -> 
( ( 1st `  ( J `  ( `' J `  <. r ,  w >. ) ) )  e.  S  /\  ( 2nd `  ( J `  ( `' J `  <. r ,  w >. ) ) )  e.  [_ ( F `
 ( 1st `  ( J `  ( `' J `  <. r ,  w >. ) ) ) )  /  x ]_ T ) )
65 2fveq3 5392 . . . . . . . . . . 11  |-  ( z  =  ( `' J `  <. r ,  w >. )  ->  ( 1st `  ( J `  z
) )  =  ( 1st `  ( J `
 ( `' J `  <. r ,  w >. ) ) ) )
6665eleq1d 2184 . . . . . . . . . 10  |-  ( z  =  ( `' J `  <. r ,  w >. )  ->  ( ( 1st `  ( J `  z ) )  e.  S  <->  ( 1st `  ( J `  ( `' J `  <. r ,  w >. ) ) )  e.  S ) )
67 2fveq3 5392 . . . . . . . . . . 11  |-  ( z  =  ( `' J `  <. r ,  w >. )  ->  ( 2nd `  ( J `  z
) )  =  ( 2nd `  ( J `
 ( `' J `  <. r ,  w >. ) ) ) )
6865fveq2d 5391 . . . . . . . . . . . 12  |-  ( z  =  ( `' J `  <. r ,  w >. )  ->  ( F `  ( 1st `  ( J `  z )
) )  =  ( F `  ( 1st `  ( J `  ( `' J `  <. r ,  w >. ) ) ) ) )
6968csbeq1d 2979 . . . . . . . . . . 11  |-  ( z  =  ( `' J `  <. r ,  w >. )  ->  [_ ( F `
 ( 1st `  ( J `  z )
) )  /  x ]_ T  =  [_ ( F `  ( 1st `  ( J `  ( `' J `  <. r ,  w >. ) ) ) )  /  x ]_ T )
7067, 69eleq12d 2186 . . . . . . . . . 10  |-  ( z  =  ( `' J `  <. r ,  w >. )  ->  ( ( 2nd `  ( J `  z ) )  e. 
[_ ( F `  ( 1st `  ( J `
 z ) ) )  /  x ]_ T 
<->  ( 2nd `  ( J `  ( `' J `  <. r ,  w >. ) ) )  e.  [_ ( F `
 ( 1st `  ( J `  ( `' J `  <. r ,  w >. ) ) ) )  /  x ]_ T ) )
7166, 70anbi12d 462 . . . . . . . . 9  |-  ( z  =  ( `' J `  <. r ,  w >. )  ->  ( (
( 1st `  ( J `  z )
)  e.  S  /\  ( 2nd `  ( J `
 z ) )  e.  [_ ( F `
 ( 1st `  ( J `  z )
) )  /  x ]_ T )  <->  ( ( 1st `  ( J `  ( `' J `  <. r ,  w >. ) ) )  e.  S  /\  ( 2nd `  ( J `  ( `' J `  <. r ,  w >. ) ) )  e.  [_ ( F `
 ( 1st `  ( J `  ( `' J `  <. r ,  w >. ) ) ) )  /  x ]_ T ) ) )
7271, 8elrab2 2814 . . . . . . . 8  |-  ( ( `' J `  <. r ,  w >. )  e.  U  <->  ( ( `' J `  <. r ,  w >. )  e.  om  /\  (
( 1st `  ( J `  ( `' J `  <. r ,  w >. ) ) )  e.  S  /\  ( 2nd `  ( J `  ( `' J `  <. r ,  w >. ) ) )  e.  [_ ( F `
 ( 1st `  ( J `  ( `' J `  <. r ,  w >. ) ) ) )  /  x ]_ T ) ) )
7344, 64, 72sylanbrc 411 . . . . . . 7  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  -> 
( `' J `  <. r ,  w >. )  e.  U )
7459csbeq1d 2979 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  ->  [_ ( F `  ( 1st `  ( J `  ( `' J `  <. r ,  w >. ) ) ) )  /  x ]_ G  =  [_ x  /  x ]_ G )
75 csbid 2980 . . . . . . . . . 10  |-  [_ x  /  x ]_ G  =  G
7674, 75syl6eq 2164 . . . . . . . . 9  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  ->  [_ ( F `  ( 1st `  ( J `  ( `' J `  <. r ,  w >. ) ) ) )  /  x ]_ G  =  G )
7776, 56fveq12d 5394 . . . . . . . 8  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  -> 
( [_ ( F `  ( 1st `  ( J `
 ( `' J `  <. r ,  w >. ) ) ) )  /  x ]_ G `  ( 2nd `  ( J `  ( `' J `  <. r ,  w >. ) ) ) )  =  ( G `
 w ) )
78 2fveq3 5392 . . . . . . . . . . . 12  |-  ( n  =  ( `' J `  <. r ,  w >. )  ->  ( 1st `  ( J `  n
) )  =  ( 1st `  ( J `
 ( `' J `  <. r ,  w >. ) ) ) )
7978fveq2d 5391 . . . . . . . . . . 11  |-  ( n  =  ( `' J `  <. r ,  w >. )  ->  ( F `  ( 1st `  ( J `  n )
) )  =  ( F `  ( 1st `  ( J `  ( `' J `  <. r ,  w >. ) ) ) ) )
8079csbeq1d 2979 . . . . . . . . . 10  |-  ( n  =  ( `' J `  <. r ,  w >. )  ->  [_ ( F `
 ( 1st `  ( J `  n )
) )  /  x ]_ G  =  [_ ( F `  ( 1st `  ( J `  ( `' J `  <. r ,  w >. ) ) ) )  /  x ]_ G )
81 2fveq3 5392 . . . . . . . . . 10  |-  ( n  =  ( `' J `  <. r ,  w >. )  ->  ( 2nd `  ( J `  n
) )  =  ( 2nd `  ( J `
 ( `' J `  <. r ,  w >. ) ) ) )
8280, 81fveq12d 5394 . . . . . . . . 9  |-  ( n  =  ( `' J `  <. r ,  w >. )  ->  ( [_ ( F `  ( 1st `  ( J `  n
) ) )  /  x ]_ G `  ( 2nd `  ( J `  n ) ) )  =  ( [_ ( F `  ( 1st `  ( J `  ( `' J `  <. r ,  w >. ) ) ) )  /  x ]_ G `  ( 2nd `  ( J `  ( `' J `  <. r ,  w >. ) ) ) ) )
83 simplrr 508 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  ->  u  =  ( G `  w ) )
8483, 77eqtr4d 2151 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  ->  u  =  ( [_ ( F `  ( 1st `  ( J `  ( `' J `  <. r ,  w >. ) ) ) )  /  x ]_ G `  ( 2nd `  ( J `  ( `' J `  <. r ,  w >. ) ) ) ) )
85 simpllr 506 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  ->  u  e.  B )
8684, 85eqeltrrd 2193 . . . . . . . . 9  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  -> 
( [_ ( F `  ( 1st `  ( J `
 ( `' J `  <. r ,  w >. ) ) ) )  /  x ]_ G `  ( 2nd `  ( J `  ( `' J `  <. r ,  w >. ) ) ) )  e.  B )
879, 82, 73, 86fvmptd3 5480 . . . . . . . 8  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  -> 
( H `  ( `' J `  <. r ,  w >. ) )  =  ( [_ ( F `
 ( 1st `  ( J `  ( `' J `  <. r ,  w >. ) ) ) )  /  x ]_ G `  ( 2nd `  ( J `  ( `' J `  <. r ,  w >. ) ) ) ) )
8877, 87, 833eqtr4rd 2159 . . . . . . 7  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  ->  u  =  ( H `  ( `' J `  <. r ,  w >. ) ) )
89 fveq2 5387 . . . . . . . 8  |-  ( v  =  ( `' J `  <. r ,  w >. )  ->  ( H `  v )  =  ( H `  ( `' J `  <. r ,  w >. ) ) )
9089rspceeqv 2779 . . . . . . 7  |-  ( ( ( `' J `  <. r ,  w >. )  e.  U  /\  u  =  ( H `  ( `' J `  <. r ,  w >. ) ) )  ->  E. v  e.  U  u  =  ( H `  v ) )
9173, 88, 90syl2anc 406 . . . . . 6  |-  ( ( ( ( ( (
ph  /\  u  e.  U_ x  e.  A  B
)  /\  x  e.  A )  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  /\  ( r  e.  S  /\  x  =  ( F `  r
) ) )  ->  E. v  e.  U  u  =  ( H `  v ) )
9229, 91rexlimddv 2529 . . . . 5  |-  ( ( ( ( ( ph  /\  u  e.  U_ x  e.  A  B )  /\  x  e.  A
)  /\  u  e.  B )  /\  (
w  e.  T  /\  u  =  ( G `  w ) ) )  ->  E. v  e.  U  u  =  ( H `  v ) )
9325, 92rexlimddv 2529 . . . 4  |-  ( ( ( ( ph  /\  u  e.  U_ x  e.  A  B )  /\  x  e.  A )  /\  u  e.  B
)  ->  E. v  e.  U  u  =  ( H `  v ) )
94 eliun 3785 . . . . . 6  |-  ( u  e.  U_ x  e.  A  B  <->  E. x  e.  A  u  e.  B )
9594biimpi 119 . . . . 5  |-  ( u  e.  U_ x  e.  A  B  ->  E. x  e.  A  u  e.  B )
9695adantl 273 . . . 4  |-  ( (
ph  /\  u  e.  U_ x  e.  A  B
)  ->  E. x  e.  A  u  e.  B )
9714, 20, 93, 96r19.29af2 2547 . . 3  |-  ( (
ph  /\  u  e.  U_ x  e.  A  B
)  ->  E. v  e.  U  u  =  ( H `  v ) )
9897ralrimiva 2480 . 2  |-  ( ph  ->  A. u  e.  U_  x  e.  A  B E. v  e.  U  u  =  ( H `  v ) )
99 dffo3 5533 . 2  |-  ( H : U -onto-> U_ x  e.  A  B  <->  ( H : U --> U_ x  e.  A  B  /\  A. u  e. 
U_  x  e.  A  B E. v  e.  U  u  =  ( H `  v ) ) )
10010, 98, 99sylanbrc 411 1  |-  ( ph  ->  H : U -onto-> U_ x  e.  A  B
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103  DECID wdc 802    = wceq 1314    e. wcel 1463   F/_wnfc 2243   A.wral 2391   E.wrex 2392   {crab 2395   [_csb 2973    C_ wss 3039   <.cop 3498   U_ciun 3781    |-> cmpt 3957   omcom 4472    X. cxp 4505   `'ccnv 4506   -->wf 5087   -onto->wfo 5089   -1-1-onto->wf1o 5090   ` cfv 5091   1stc1st 6002   2ndc2nd 6003
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-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4014  ax-pow 4066  ax-pr 4099  ax-un 4323
This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ral 2396  df-rex 2397  df-rab 2400  df-v 2660  df-sbc 2881  df-csb 2974  df-un 3043  df-in 3045  df-ss 3052  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-uni 3705  df-iun 3783  df-br 3898  df-opab 3958  df-mpt 3959  df-id 4183  df-xp 4513  df-rel 4514  df-cnv 4515  df-co 4516  df-dm 4517  df-rn 4518  df-res 4519  df-ima 4520  df-iota 5056  df-fun 5093  df-fn 5094  df-f 5095  df-f1 5096  df-fo 5097  df-f1o 5098  df-fv 5099  df-1st 6004  df-2nd 6005
This theorem is referenced by:  ctiunct  11848
  Copyright terms: Public domain W3C validator