MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axdc4lem Structured version   Unicode version

Theorem axdc4lem 8373
Description: Lemma for axdc4 8374. (Contributed by Mario Carneiro, 31-Jan-2013.) (Revised by Mario Carneiro, 16-Nov-2013.)
Hypotheses
Ref Expression
axdc4lem.1  |-  A  e. 
_V
axdc4lem.2  |-  G  =  ( n  e.  om ,  x  e.  A  |->  ( { suc  n }  X.  ( n F x ) ) )
Assertion
Ref Expression
axdc4lem  |-  ( ( C  e.  A  /\  F : ( om  X.  A ) --> ( ~P A  \  { (/) } ) )  ->  E. g
( g : om --> A  /\  ( g `  (/) )  =  C  /\  A. k  e.  om  (
g `  suc  k )  e.  ( k F ( g `  k
) ) ) )
Distinct variable groups:    g, k, n, x, A    C, g,
k    g, F, n, x   
k, G
Allowed substitution hints:    C( x, n)    F( k)    G( x, g, n)

Proof of Theorem axdc4lem
Dummy variables  h  i  m  s  t 
z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 peano1 4899 . . . 4  |-  (/)  e.  om
2 opelxpi 4945 . . . 4  |-  ( (
(/)  e.  om  /\  C  e.  A )  ->  <. (/) ,  C >.  e.  ( om  X.  A ) )
31, 2mpan 653 . . 3  |-  ( C  e.  A  ->  <. (/) ,  C >.  e.  ( om  X.  A ) )
4 simp2 959 . . . . . . . 8  |-  ( ( F : ( om 
X.  A ) --> ( ~P A  \  { (/)
} )  /\  n  e.  om  /\  x  e.  A )  ->  n  e.  om )
5 fovrn 6252 . . . . . . . 8  |-  ( ( F : ( om 
X.  A ) --> ( ~P A  \  { (/)
} )  /\  n  e.  om  /\  x  e.  A )  ->  (
n F x )  e.  ( ~P A  \  { (/) } ) )
6 peano2 4900 . . . . . . . . . . 11  |-  ( n  e.  om  ->  suc  n  e.  om )
76snssd 3972 . . . . . . . . . 10  |-  ( n  e.  om  ->  { suc  n }  C_  om )
8 eldifi 3458 . . . . . . . . . 10  |-  ( ( n F x )  e.  ( ~P A  \  { (/) } )  -> 
( n F x )  e.  ~P A
)
9 axdc4lem.1 . . . . . . . . . . . 12  |-  A  e. 
_V
109elpw2 4399 . . . . . . . . . . 11  |-  ( ( n F x )  e.  ~P A  <->  ( n F x )  C_  A )
11 xpss12 5016 . . . . . . . . . . 11  |-  ( ( { suc  n }  C_ 
om  /\  ( n F x )  C_  A )  ->  ( { suc  n }  X.  ( n F x ) )  C_  ( om  X.  A ) )
1210, 11sylan2b 463 . . . . . . . . . 10  |-  ( ( { suc  n }  C_ 
om  /\  ( n F x )  e. 
~P A )  -> 
( { suc  n }  X.  ( n F x ) )  C_  ( om  X.  A ) )
137, 8, 12syl2an 465 . . . . . . . . 9  |-  ( ( n  e.  om  /\  ( n F x )  e.  ( ~P A  \  { (/) } ) )  ->  ( { suc  n }  X.  ( n F x ) )  C_  ( om  X.  A ) )
14 snex 4440 . . . . . . . . . . 11  |-  { suc  n }  e.  _V
15 ovex 6142 . . . . . . . . . . 11  |-  ( n F x )  e. 
_V
1614, 15xpex 5025 . . . . . . . . . 10  |-  ( { suc  n }  X.  ( n F x ) )  e.  _V
1716elpw 3834 . . . . . . . . 9  |-  ( ( { suc  n }  X.  ( n F x ) )  e.  ~P ( om  X.  A )  <-> 
( { suc  n }  X.  ( n F x ) )  C_  ( om  X.  A ) )
1813, 17sylibr 205 . . . . . . . 8  |-  ( ( n  e.  om  /\  ( n F x )  e.  ( ~P A  \  { (/) } ) )  ->  ( { suc  n }  X.  ( n F x ) )  e.  ~P ( om  X.  A ) )
194, 5, 18syl2anc 644 . . . . . . 7  |-  ( ( F : ( om 
X.  A ) --> ( ~P A  \  { (/)
} )  /\  n  e.  om  /\  x  e.  A )  ->  ( { suc  n }  X.  ( n F x ) )  e.  ~P ( om  X.  A ) )
20 eldifn 3459 . . . . . . . 8  |-  ( ( n F x )  e.  ( ~P A  \  { (/) } )  ->  -.  ( n F x )  e.  { (/) } )
2115elsnc 3866 . . . . . . . . . . 11  |-  ( ( n F x )  e.  { (/) }  <->  ( n F x )  =  (/) )
2221necon3bbii 2639 . . . . . . . . . 10  |-  ( -.  ( n F x )  e.  { (/) }  <-> 
( n F x )  =/=  (/) )
23 vex 2968 . . . . . . . . . . . . 13  |-  n  e. 
_V
2423sucex 4826 . . . . . . . . . . . 12  |-  suc  n  e.  _V
2524snnz 3951 . . . . . . . . . . 11  |-  { suc  n }  =/=  (/)
26 xpnz 5327 . . . . . . . . . . . 12  |-  ( ( { suc  n }  =/=  (/)  /\  ( n F x )  =/=  (/) )  <->  ( { suc  n }  X.  (
n F x ) )  =/=  (/) )
2726biimpi 188 . . . . . . . . . . 11  |-  ( ( { suc  n }  =/=  (/)  /\  ( n F x )  =/=  (/) )  ->  ( { suc  n }  X.  ( n F x ) )  =/=  (/) )
2825, 27mpan 653 . . . . . . . . . 10  |-  ( ( n F x )  =/=  (/)  ->  ( { suc  n }  X.  (
n F x ) )  =/=  (/) )
2922, 28sylbi 189 . . . . . . . . 9  |-  ( -.  ( n F x )  e.  { (/) }  ->  ( { suc  n }  X.  (
n F x ) )  =/=  (/) )
3016elsnc 3866 . . . . . . . . . 10  |-  ( ( { suc  n }  X.  ( n F x ) )  e.  { (/)
}  <->  ( { suc  n }  X.  (
n F x ) )  =  (/) )
3130necon3bbii 2639 . . . . . . . . 9  |-  ( -.  ( { suc  n }  X.  ( n F x ) )  e. 
{ (/) }  <->  ( { suc  n }  X.  (
n F x ) )  =/=  (/) )
3229, 31sylibr 205 . . . . . . . 8  |-  ( -.  ( n F x )  e.  { (/) }  ->  -.  ( { suc  n }  X.  (
n F x ) )  e.  { (/) } )
335, 20, 323syl 19 . . . . . . 7  |-  ( ( F : ( om 
X.  A ) --> ( ~P A  \  { (/)
} )  /\  n  e.  om  /\  x  e.  A )  ->  -.  ( { suc  n }  X.  ( n F x ) )  e.  { (/)
} )
3419, 33eldifd 3320 . . . . . 6  |-  ( ( F : ( om 
X.  A ) --> ( ~P A  \  { (/)
} )  /\  n  e.  om  /\  x  e.  A )  ->  ( { suc  n }  X.  ( n F x ) )  e.  ( ~P ( om  X.  A )  \  { (/)
} ) )
35343expib 1157 . . . . 5  |-  ( F : ( om  X.  A ) --> ( ~P A  \  { (/) } )  ->  ( (
n  e.  om  /\  x  e.  A )  ->  ( { suc  n }  X.  ( n F x ) )  e.  ( ~P ( om 
X.  A )  \  { (/) } ) ) )
3635ralrimivv 2804 . . . 4  |-  ( F : ( om  X.  A ) --> ( ~P A  \  { (/) } )  ->  A. n  e.  om  A. x  e.  A  ( { suc  n }  X.  (
n F x ) )  e.  ( ~P ( om  X.  A
)  \  { (/) } ) )
37 axdc4lem.2 . . . . 5  |-  G  =  ( n  e.  om ,  x  e.  A  |->  ( { suc  n }  X.  ( n F x ) ) )
3837fmpt2 6454 . . . 4  |-  ( A. n  e.  om  A. x  e.  A  ( { suc  n }  X.  (
n F x ) )  e.  ( ~P ( om  X.  A
)  \  { (/) } )  <-> 
G : ( om 
X.  A ) --> ( ~P ( om  X.  A )  \  { (/)
} ) )
3936, 38sylib 190 . . 3  |-  ( F : ( om  X.  A ) --> ( ~P A  \  { (/) } )  ->  G :
( om  X.  A
) --> ( ~P ( om  X.  A )  \  { (/) } ) )
40 dcomex 8365 . . . . 5  |-  om  e.  _V
4140, 9xpex 5025 . . . 4  |-  ( om 
X.  A )  e. 
_V
4241axdc3 8372 . . 3  |-  ( (
<. (/) ,  C >.  e.  ( om  X.  A
)  /\  G :
( om  X.  A
) --> ( ~P ( om  X.  A )  \  { (/) } ) )  ->  E. h ( h : om --> ( om 
X.  A )  /\  ( h `  (/) )  = 
<. (/) ,  C >.  /\ 
A. k  e.  om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )
433, 39, 42syl2an 465 . 2  |-  ( ( C  e.  A  /\  F : ( om  X.  A ) --> ( ~P A  \  { (/) } ) )  ->  E. h
( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )
44 2ndcof 6411 . . . . . . . . 9  |-  ( h : om --> ( om 
X.  A )  -> 
( 2nd  o.  h
) : om --> A )
45443ad2ant1 979 . . . . . . . 8  |-  ( ( h : om --> ( om 
X.  A )  /\  ( h `  (/) )  = 
<. (/) ,  C >.  /\ 
A. k  e.  om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  ->  ( 2nd  o.  h ) : om --> A )
4645adantl 454 . . . . . . 7  |-  ( ( C  e.  A  /\  ( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )  ->  ( 2nd  o.  h ) : om --> A )
47 fex2 5638 . . . . . . . 8  |-  ( ( ( 2nd  o.  h
) : om --> A  /\  om  e.  _V  /\  A  e.  _V )  ->  ( 2nd  o.  h )  e. 
_V )
4840, 9, 47mp3an23 1272 . . . . . . 7  |-  ( ( 2nd  o.  h ) : om --> A  -> 
( 2nd  o.  h
)  e.  _V )
4946, 48syl 16 . . . . . 6  |-  ( ( C  e.  A  /\  ( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )  ->  ( 2nd  o.  h )  e. 
_V )
50 fvco3 5836 . . . . . . . . . . 11  |-  ( ( h : om --> ( om 
X.  A )  /\  (/) 
e.  om )  ->  (
( 2nd  o.  h
) `  (/) )  =  ( 2nd `  (
h `  (/) ) ) )
511, 50mpan2 654 . . . . . . . . . 10  |-  ( h : om --> ( om 
X.  A )  -> 
( ( 2nd  o.  h ) `  (/) )  =  ( 2nd `  (
h `  (/) ) ) )
52513ad2ant1 979 . . . . . . . . 9  |-  ( ( h : om --> ( om 
X.  A )  /\  ( h `  (/) )  = 
<. (/) ,  C >.  /\ 
A. k  e.  om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  ->  ( ( 2nd  o.  h ) `  (/) )  =  ( 2nd `  ( h `  (/) ) ) )
53 fveq2 5763 . . . . . . . . . 10  |-  ( ( h `  (/) )  = 
<. (/) ,  C >.  -> 
( 2nd `  (
h `  (/) ) )  =  ( 2nd `  <. (/)
,  C >. )
)
54533ad2ant2 980 . . . . . . . . 9  |-  ( ( h : om --> ( om 
X.  A )  /\  ( h `  (/) )  = 
<. (/) ,  C >.  /\ 
A. k  e.  om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  ->  ( 2nd `  ( h `  (/) ) )  =  ( 2nd `  <. (/)
,  C >. )
)
5552, 54eqtrd 2475 . . . . . . . 8  |-  ( ( h : om --> ( om 
X.  A )  /\  ( h `  (/) )  = 
<. (/) ,  C >.  /\ 
A. k  e.  om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  ->  ( ( 2nd  o.  h ) `  (/) )  =  ( 2nd `  <. (/) ,  C >. ) )
56 op2ndg 6396 . . . . . . . . 9  |-  ( (
(/)  e.  om  /\  C  e.  A )  ->  ( 2nd `  <. (/) ,  C >. )  =  C )
571, 56mpan 653 . . . . . . . 8  |-  ( C  e.  A  ->  ( 2nd `  <. (/) ,  C >. )  =  C )
5855, 57sylan9eqr 2497 . . . . . . 7  |-  ( ( C  e.  A  /\  ( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )  ->  (
( 2nd  o.  h
) `  (/) )  =  C )
59 nfv 1631 . . . . . . . . 9  |-  F/ k  C  e.  A
60 nfv 1631 . . . . . . . . . 10  |-  F/ k  h : om --> ( om 
X.  A )
61 nfv 1631 . . . . . . . . . 10  |-  F/ k ( h `  (/) )  = 
<. (/) ,  C >.
62 nfra1 2763 . . . . . . . . . 10  |-  F/ k A. k  e.  om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) )
6360, 61, 62nf3an 1852 . . . . . . . . 9  |-  F/ k ( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )
6459, 63nfan 1849 . . . . . . . 8  |-  F/ k ( C  e.  A  /\  ( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )
65 fveq2 5763 . . . . . . . . . . . . . . . . 17  |-  ( m  =  (/)  ->  ( h `
 m )  =  ( h `  (/) ) )
66 opeq1 4013 . . . . . . . . . . . . . . . . 17  |-  ( m  =  (/)  ->  <. m ,  z >.  =  <. (/)
,  z >. )
6765, 66eqeq12d 2457 . . . . . . . . . . . . . . . 16  |-  ( m  =  (/)  ->  ( ( h `  m )  =  <. m ,  z
>. 
<->  ( h `  (/) )  = 
<. (/) ,  z >.
) )
6867exbidv 1638 . . . . . . . . . . . . . . 15  |-  ( m  =  (/)  ->  ( E. z ( h `  m )  =  <. m ,  z >.  <->  E. z
( h `  (/) )  = 
<. (/) ,  z >.
) )
69 fveq2 5763 . . . . . . . . . . . . . . . . 17  |-  ( m  =  i  ->  (
h `  m )  =  ( h `  i ) )
70 opeq1 4013 . . . . . . . . . . . . . . . . 17  |-  ( m  =  i  ->  <. m ,  z >.  =  <. i ,  z >. )
7169, 70eqeq12d 2457 . . . . . . . . . . . . . . . 16  |-  ( m  =  i  ->  (
( h `  m
)  =  <. m ,  z >.  <->  ( h `  i )  =  <. i ,  z >. )
)
7271exbidv 1638 . . . . . . . . . . . . . . 15  |-  ( m  =  i  ->  ( E. z ( h `  m )  =  <. m ,  z >.  <->  E. z
( h `  i
)  =  <. i ,  z >. )
)
73 fveq2 5763 . . . . . . . . . . . . . . . . 17  |-  ( m  =  suc  i  -> 
( h `  m
)  =  ( h `
 suc  i )
)
74 opeq1 4013 . . . . . . . . . . . . . . . . 17  |-  ( m  =  suc  i  ->  <. m ,  z >.  =  <. suc  i , 
z >. )
7573, 74eqeq12d 2457 . . . . . . . . . . . . . . . 16  |-  ( m  =  suc  i  -> 
( ( h `  m )  =  <. m ,  z >.  <->  ( h `  suc  i )  = 
<. suc  i ,  z
>. ) )
7675exbidv 1638 . . . . . . . . . . . . . . 15  |-  ( m  =  suc  i  -> 
( E. z ( h `  m )  =  <. m ,  z
>. 
<->  E. z ( h `
 suc  i )  =  <. suc  i , 
z >. ) )
77 opeq2 4014 . . . . . . . . . . . . . . . . . . 19  |-  ( z  =  C  ->  <. (/) ,  z
>.  =  <. (/) ,  C >. )
7877eqeq2d 2454 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  C  ->  (
( h `  (/) )  = 
<. (/) ,  z >.  <->  ( h `  (/) )  = 
<. (/) ,  C >. ) )
7978spcegv 3046 . . . . . . . . . . . . . . . . 17  |-  ( C  e.  A  ->  (
( h `  (/) )  = 
<. (/) ,  C >.  ->  E. z ( h `  (/) )  =  <. (/) ,  z
>. ) )
8079imp 420 . . . . . . . . . . . . . . . 16  |-  ( ( C  e.  A  /\  ( h `  (/) )  = 
<. (/) ,  C >. )  ->  E. z ( h `
 (/) )  =  <. (/)
,  z >. )
81803ad2antr2 1124 . . . . . . . . . . . . . . 15  |-  ( ( C  e.  A  /\  ( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )  ->  E. z
( h `  (/) )  = 
<. (/) ,  z >.
)
82 fveq2 5763 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( h `  i )  =  <. i ,  z
>.  ->  ( G `  ( h `  i
) )  =  ( G `  <. i ,  z >. )
)
83 df-ov 6120 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( i G z )  =  ( G `  <. i ,  z >. )
8482, 83syl6eqr 2493 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( h `  i )  =  <. i ,  z
>.  ->  ( G `  ( h `  i
) )  =  ( i G z ) )
8584adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( h : om --> ( om  X.  A )  /\  i  e.  om )  /\  ( h `  i )  =  <. i ,  z >. )  ->  ( G `  (
h `  i )
)  =  ( i G z ) )
86 simplr 733 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( h : om --> ( om  X.  A )  /\  i  e.  om )  /\  ( h `  i )  =  <. i ,  z >. )  ->  i  e.  om )
87 ffvelrn 5904 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( h : om --> ( om 
X.  A )  /\  i  e.  om )  ->  ( h `  i
)  e.  ( om 
X.  A ) )
88 eleq1 2503 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( h `  i )  =  <. i ,  z
>.  ->  ( ( h `
 i )  e.  ( om  X.  A
)  <->  <. i ,  z
>.  e.  ( om  X.  A ) ) )
89 opelxp2 4947 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( <.
i ,  z >.  e.  ( om  X.  A
)  ->  z  e.  A )
9088, 89syl6bi 221 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( h `  i )  =  <. i ,  z
>.  ->  ( ( h `
 i )  e.  ( om  X.  A
)  ->  z  e.  A ) )
9187, 90mpan9 457 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( h : om --> ( om  X.  A )  /\  i  e.  om )  /\  ( h `  i )  =  <. i ,  z >. )  ->  z  e.  A )
92 suceq 4681 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( n  =  i  ->  suc  n  =  suc  i )
9392sneqd 3856 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( n  =  i  ->  { suc  n }  =  { suc  i } )
94 oveq1 6124 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( n  =  i  ->  (
n F x )  =  ( i F x ) )
9593, 94xpeq12d 4938 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( n  =  i  ->  ( { suc  n }  X.  ( n F x ) )  =  ( { suc  i }  X.  ( i F x ) ) )
96 oveq2 6125 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  =  z  ->  (
i F x )  =  ( i F z ) )
9796xpeq2d 4937 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  =  z  ->  ( { suc  i }  X.  ( i F x ) )  =  ( { suc  i }  X.  ( i F z ) ) )
98 snex 4440 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  { suc  i }  e.  _V
99 ovex 6142 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( i F z )  e. 
_V
10098, 99xpex 5025 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( { suc  i }  X.  ( i F z ) )  e.  _V
10195, 97, 37, 100ovmpt2 6245 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( i  e.  om  /\  z  e.  A )  ->  ( i G z )  =  ( { suc  i }  X.  ( i F z ) ) )
10286, 91, 101syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( h : om --> ( om  X.  A )  /\  i  e.  om )  /\  ( h `  i )  =  <. i ,  z >. )  ->  ( i G z )  =  ( { suc  i }  X.  ( i F z ) ) )
10385, 102eqtrd 2475 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( h : om --> ( om  X.  A )  /\  i  e.  om )  /\  ( h `  i )  =  <. i ,  z >. )  ->  ( G `  (
h `  i )
)  =  ( { suc  i }  X.  ( i F z ) ) )
104 suceq 4681 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( k  =  i  ->  suc  k  =  suc  i )
105104fveq2d 5767 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  =  i  ->  (
h `  suc  k )  =  ( h `  suc  i ) )
106 fveq2 5763 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( k  =  i  ->  (
h `  k )  =  ( h `  i ) )
107106fveq2d 5767 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  =  i  ->  ( G `  ( h `  k ) )  =  ( G `  (
h `  i )
) )
108105, 107eleq12d 2511 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( k  =  i  ->  (
( h `  suc  k )  e.  ( G `  ( h `
 k ) )  <-> 
( h `  suc  i )  e.  ( G `  ( h `
 i ) ) ) )
109108rspcv 3057 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( i  e.  om  ->  ( A. k  e.  om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) )  ->  ( h `  suc  i )  e.  ( G `  ( h `
 i ) ) ) )
110109ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( h : om --> ( om  X.  A )  /\  i  e.  om )  /\  ( h `  i )  =  <. i ,  z >. )  ->  ( A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) )  ->  ( h `  suc  i )  e.  ( G `  ( h `
 i ) ) ) )
111 eleq2 2504 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( G `  ( h `
 i ) )  =  ( { suc  i }  X.  (
i F z ) )  ->  ( (
h `  suc  i )  e.  ( G `  ( h `  i
) )  <->  ( h `  suc  i )  e.  ( { suc  i }  X.  ( i F z ) ) ) )
112 elxp 4930 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( h `  suc  i
)  e.  ( { suc  i }  X.  ( i F z ) )  <->  E. s E. t ( ( h `
 suc  i )  =  <. s ,  t
>.  /\  ( s  e. 
{ suc  i }  /\  t  e.  (
i F z ) ) ) )
113 elsn 3858 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( s  e.  { suc  i } 
<->  s  =  suc  i
)
114 opeq1 4013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( s  =  suc  i  ->  <. s ,  t >.  =  <. suc  i , 
t >. )
115113, 114sylbi 189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( s  e.  { suc  i }  ->  <. s ,  t
>.  =  <. suc  i ,  t >. )
116115eqeq2d 2454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( s  e.  { suc  i }  ->  ( ( h `
 suc  i )  =  <. s ,  t
>. 
<->  ( h `  suc  i )  =  <. suc  i ,  t >.
) )
117116biimpac 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( h `  suc  i )  =  <. s ,  t >.  /\  s  e.  { suc  i } )  ->  ( h `  suc  i )  = 
<. suc  i ,  t
>. )
118117adantrr 699 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( h `  suc  i )  =  <. s ,  t >.  /\  (
s  e.  { suc  i }  /\  t  e.  ( i F z ) ) )  -> 
( h `  suc  i )  =  <. suc  i ,  t >.
)
119118eximi 1586 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( E. t ( ( h `
 suc  i )  =  <. s ,  t
>.  /\  ( s  e. 
{ suc  i }  /\  t  e.  (
i F z ) ) )  ->  E. t
( h `  suc  i )  =  <. suc  i ,  t >.
)
120119exlimiv 1646 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( E. s E. t ( ( h `  suc  i )  =  <. s ,  t >.  /\  (
s  e.  { suc  i }  /\  t  e.  ( i F z ) ) )  ->  E. t ( h `  suc  i )  =  <. suc  i ,  t >.
)
121112, 120sylbi 189 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( h `  suc  i
)  e.  ( { suc  i }  X.  ( i F z ) )  ->  E. t
( h `  suc  i )  =  <. suc  i ,  t >.
)
122111, 121syl6bi 221 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( G `  ( h `
 i ) )  =  ( { suc  i }  X.  (
i F z ) )  ->  ( (
h `  suc  i )  e.  ( G `  ( h `  i
) )  ->  E. t
( h `  suc  i )  =  <. suc  i ,  t >.
) )
123103, 110, 122sylsyld 55 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( h : om --> ( om  X.  A )  /\  i  e.  om )  /\  ( h `  i )  =  <. i ,  z >. )  ->  ( A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) )  ->  E. t ( h `
 suc  i )  =  <. suc  i , 
t >. ) )
124123expcom 426 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( h `  i )  =  <. i ,  z
>.  ->  ( ( h : om --> ( om 
X.  A )  /\  i  e.  om )  ->  ( A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) )  ->  E. t ( h `
 suc  i )  =  <. suc  i , 
t >. ) ) )
125124exlimiv 1646 . . . . . . . . . . . . . . . . . . . . 21  |-  ( E. z ( h `  i )  =  <. i ,  z >.  ->  (
( h : om --> ( om  X.  A )  /\  i  e.  om )  ->  ( A. k  e.  om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) )  ->  E. t ( h `
 suc  i )  =  <. suc  i , 
t >. ) ) )
126125com3l 78 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( h : om --> ( om 
X.  A )  /\  i  e.  om )  ->  ( A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) )  ->  ( E. z
( h `  i
)  =  <. i ,  z >.  ->  E. t
( h `  suc  i )  =  <. suc  i ,  t >.
) ) )
127 opeq2 4014 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( t  =  z  ->  <. suc  i ,  t >.  =  <. suc  i ,  z >.
)
128127eqeq2d 2454 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  =  z  ->  (
( h `  suc  i )  =  <. suc  i ,  t >.  <->  ( h `  suc  i
)  =  <. suc  i ,  z >. )
)
129128cbvexv 1989 . . . . . . . . . . . . . . . . . . . 20  |-  ( E. t ( h `  suc  i )  =  <. suc  i ,  t >.  <->  E. z ( h `  suc  i )  =  <. suc  i ,  z >.
)
130126, 129syl8ib 224 . . . . . . . . . . . . . . . . . . 19  |-  ( ( h : om --> ( om 
X.  A )  /\  i  e.  om )  ->  ( A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) )  ->  ( E. z
( h `  i
)  =  <. i ,  z >.  ->  E. z
( h `  suc  i )  =  <. suc  i ,  z >.
) ) )
131130impancom 429 . . . . . . . . . . . . . . . . . 18  |-  ( ( h : om --> ( om 
X.  A )  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( i  e.  om  ->  ( E. z ( h `  i )  =  <. i ,  z
>.  ->  E. z ( h `
 suc  i )  =  <. suc  i , 
z >. ) ) )
1321313adant2 977 . . . . . . . . . . . . . . . . 17  |-  ( ( h : om --> ( om 
X.  A )  /\  ( h `  (/) )  = 
<. (/) ,  C >.  /\ 
A. k  e.  om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  ->  ( i  e.  om  ->  ( E. z ( h `  i )  =  <. i ,  z >.  ->  E. z
( h `  suc  i )  =  <. suc  i ,  z >.
) ) )
133132adantl 454 . . . . . . . . . . . . . . . 16  |-  ( ( C  e.  A  /\  ( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )  ->  (
i  e.  om  ->  ( E. z ( h `
 i )  = 
<. i ,  z >.  ->  E. z ( h `
 suc  i )  =  <. suc  i , 
z >. ) ) )
134133com12 30 . . . . . . . . . . . . . . 15  |-  ( i  e.  om  ->  (
( C  e.  A  /\  ( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )  ->  ( E. z ( h `  i )  =  <. i ,  z >.  ->  E. z
( h `  suc  i )  =  <. suc  i ,  z >.
) ) )
13568, 72, 76, 81, 134finds2 4908 . . . . . . . . . . . . . 14  |-  ( m  e.  om  ->  (
( C  e.  A  /\  ( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )  ->  E. z
( h `  m
)  =  <. m ,  z >. )
)
136135com12 30 . . . . . . . . . . . . 13  |-  ( ( C  e.  A  /\  ( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )  ->  (
m  e.  om  ->  E. z ( h `  m )  =  <. m ,  z >. )
)
137136ralrimiv 2795 . . . . . . . . . . . 12  |-  ( ( C  e.  A  /\  ( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )  ->  A. m  e.  om  E. z ( h `  m )  =  <. m ,  z
>. )
138 fveq2 5763 . . . . . . . . . . . . . . 15  |-  ( m  =  k  ->  (
h `  m )  =  ( h `  k ) )
139 opeq1 4013 . . . . . . . . . . . . . . 15  |-  ( m  =  k  ->  <. m ,  z >.  =  <. k ,  z >. )
140138, 139eqeq12d 2457 . . . . . . . . . . . . . 14  |-  ( m  =  k  ->  (
( h `  m
)  =  <. m ,  z >.  <->  ( h `  k )  =  <. k ,  z >. )
)
141140exbidv 1638 . . . . . . . . . . . . 13  |-  ( m  =  k  ->  ( E. z ( h `  m )  =  <. m ,  z >.  <->  E. z
( h `  k
)  =  <. k ,  z >. )
)
142141rspccv 3058 . . . . . . . . . . . 12  |-  ( A. m  e.  om  E. z
( h `  m
)  =  <. m ,  z >.  ->  (
k  e.  om  ->  E. z ( h `  k )  =  <. k ,  z >. )
)
143137, 142syl 16 . . . . . . . . . . 11  |-  ( ( C  e.  A  /\  ( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )  ->  (
k  e.  om  ->  E. z ( h `  k )  =  <. k ,  z >. )
)
1441433impia 1151 . . . . . . . . . 10  |-  ( ( C  e.  A  /\  ( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  /\  k  e. 
om )  ->  E. z
( h `  k
)  =  <. k ,  z >. )
145 simp21 991 . . . . . . . . . 10  |-  ( ( C  e.  A  /\  ( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  /\  k  e. 
om )  ->  h : om --> ( om  X.  A ) )
146 simp3 960 . . . . . . . . . 10  |-  ( ( C  e.  A  /\  ( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  /\  k  e. 
om )  ->  k  e.  om )
147 rsp 2773 . . . . . . . . . . . . 13  |-  ( A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) )  ->  (
k  e.  om  ->  ( h `  suc  k
)  e.  ( G `
 ( h `  k ) ) ) )
148147imp 420 . . . . . . . . . . . 12  |-  ( ( A. k  e.  om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) )  /\  k  e.  om )  ->  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )
1491483ad2antl3 1122 . . . . . . . . . . 11  |-  ( ( ( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  /\  k  e. 
om )  ->  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )
1501493adant1 976 . . . . . . . . . 10  |-  ( ( C  e.  A  /\  ( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  /\  k  e. 
om )  ->  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )
151 simpl 445 . . . . . . . . . . . . . . . . 17  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( h `  k )  =  <. k ,  z >. )
152151fveq2d 5767 . . . . . . . . . . . . . . . 16  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( G `  ( h `  k
) )  =  ( G `  <. k ,  z >. )
)
153 simprr 735 . . . . . . . . . . . . . . . . 17  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  k  e.  om )
154 ffvelrn 5904 . . . . . . . . . . . . . . . . . . 19  |-  ( ( h : om --> ( om 
X.  A )  /\  k  e.  om )  ->  ( h `  k
)  e.  ( om 
X.  A ) )
155 eleq1 2503 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( h `  k )  =  <. k ,  z
>.  ->  ( ( h `
 k )  e.  ( om  X.  A
)  <->  <. k ,  z
>.  e.  ( om  X.  A ) ) )
156 opelxp2 4947 . . . . . . . . . . . . . . . . . . . 20  |-  ( <.
k ,  z >.  e.  ( om  X.  A
)  ->  z  e.  A )
157155, 156syl6bi 221 . . . . . . . . . . . . . . . . . . 19  |-  ( ( h `  k )  =  <. k ,  z
>.  ->  ( ( h `
 k )  e.  ( om  X.  A
)  ->  z  e.  A ) )
158154, 157syl5 31 . . . . . . . . . . . . . . . . . 18  |-  ( ( h `  k )  =  <. k ,  z
>.  ->  ( ( h : om --> ( om 
X.  A )  /\  k  e.  om )  ->  z  e.  A ) )
159158imp 420 . . . . . . . . . . . . . . . . 17  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  z  e.  A )
160 df-ov 6120 . . . . . . . . . . . . . . . . . 18  |-  ( k G z )  =  ( G `  <. k ,  z >. )
161 suceq 4681 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  k  ->  suc  n  =  suc  k )
162161sneqd 3856 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  k  ->  { suc  n }  =  { suc  k } )
163 oveq1 6124 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  k  ->  (
n F x )  =  ( k F x ) )
164162, 163xpeq12d 4938 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  k  ->  ( { suc  n }  X.  ( n F x ) )  =  ( { suc  k }  X.  ( k F x ) ) )
165 oveq2 6125 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  z  ->  (
k F x )  =  ( k F z ) )
166165xpeq2d 4937 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  z  ->  ( { suc  k }  X.  ( k F x ) )  =  ( { suc  k }  X.  ( k F z ) ) )
167 snex 4440 . . . . . . . . . . . . . . . . . . . 20  |-  { suc  k }  e.  _V
168 ovex 6142 . . . . . . . . . . . . . . . . . . . 20  |-  ( k F z )  e. 
_V
169167, 168xpex 5025 . . . . . . . . . . . . . . . . . . 19  |-  ( { suc  k }  X.  ( k F z ) )  e.  _V
170164, 166, 37, 169ovmpt2 6245 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  om  /\  z  e.  A )  ->  ( k G z )  =  ( { suc  k }  X.  ( k F z ) ) )
171160, 170syl5eqr 2489 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  om  /\  z  e.  A )  ->  ( G `  <. k ,  z >. )  =  ( { suc  k }  X.  (
k F z ) ) )
172153, 159, 171syl2anc 644 . . . . . . . . . . . . . . . 16  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( G `  <. k ,  z
>. )  =  ( { suc  k }  X.  ( k F z ) ) )
173152, 172eqtrd 2475 . . . . . . . . . . . . . . 15  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( G `  ( h `  k
) )  =  ( { suc  k }  X.  ( k F z ) ) )
174173eleq2d 2510 . . . . . . . . . . . . . 14  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( (
h `  suc  k )  e.  ( G `  ( h `  k
) )  <->  ( h `  suc  k )  e.  ( { suc  k }  X.  ( k F z ) ) ) )
175 elxp 4930 . . . . . . . . . . . . . . . . 17  |-  ( ( h `  suc  k
)  e.  ( { suc  k }  X.  ( k F z ) )  <->  E. s E. t ( ( h `
 suc  k )  =  <. s ,  t
>.  /\  ( s  e. 
{ suc  k }  /\  t  e.  (
k F z ) ) ) )
176 peano2 4900 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  e.  om  ->  suc  k  e.  om )
177 fvco3 5836 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( h : om --> ( om 
X.  A )  /\  suc  k  e.  om )  ->  ( ( 2nd 
o.  h ) `  suc  k )  =  ( 2nd `  ( h `
 suc  k )
) )
178176, 177sylan2 462 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( h : om --> ( om 
X.  A )  /\  k  e.  om )  ->  ( ( 2nd  o.  h ) `  suc  k )  =  ( 2nd `  ( h `
 suc  k )
) )
179178adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( ( 2nd  o.  h ) `  suc  k )  =  ( 2nd `  ( h `
 suc  k )
) )
180 simpll 732 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( h `  suc  k )  = 
<. s ,  t >.
)
181180fveq2d 5767 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( 2nd `  ( h `  suc  k ) )  =  ( 2nd `  <. s ,  t >. )
)
182179, 181eqtrd 2475 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( ( 2nd  o.  h ) `  suc  k )  =  ( 2nd `  <. s ,  t >. )
)
183 vex 2968 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  s  e. 
_V
184 vex 2968 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  t  e. 
_V
185183, 184op2nd 6392 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 2nd `  <. s ,  t
>. )  =  t
186182, 185syl6eq 2491 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( ( 2nd  o.  h ) `  suc  k )  =  t )
187 fvco3 5836 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( h : om --> ( om 
X.  A )  /\  k  e.  om )  ->  ( ( 2nd  o.  h ) `  k
)  =  ( 2nd `  ( h `  k
) ) )
188187adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( ( 2nd  o.  h ) `  k )  =  ( 2nd `  ( h `
 k ) ) )
189 simplr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( h `  k )  =  <. k ,  z >. )
190189fveq2d 5767 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( 2nd `  ( h `  k
) )  =  ( 2nd `  <. k ,  z >. )
)
191188, 190eqtrd 2475 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( ( 2nd  o.  h ) `  k )  =  ( 2nd `  <. k ,  z >. )
)
192 vex 2968 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  k  e. 
_V
193 vex 2968 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  z  e. 
_V
194192, 193op2nd 6392 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 2nd `  <. k ,  z
>. )  =  z
195191, 194syl6eq 2491 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( ( 2nd  o.  h ) `  k )  =  z )
196195oveq2d 6133 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( k F ( ( 2nd 
o.  h ) `  k ) )  =  ( k F z ) )
197186, 196eleq12d 2511 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( (
( 2nd  o.  h
) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `  k
) )  <->  t  e.  ( k F z ) ) )
198197biimprcd 218 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  e.  ( k F z )  ->  (
( ( ( h `
 suc  k )  =  <. s ,  t
>.  /\  ( h `  k )  =  <. k ,  z >. )  /\  ( h : om --> ( om  X.  A )  /\  k  e.  om ) )  ->  (
( 2nd  o.  h
) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `  k
) ) ) )
199198exp4c 593 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  e.  ( k F z )  ->  (
( h `  suc  k )  =  <. s ,  t >.  ->  (
( h `  k
)  =  <. k ,  z >.  ->  (
( h : om --> ( om  X.  A )  /\  k  e.  om )  ->  ( ( 2nd 
o.  h ) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `
 k ) ) ) ) ) )
200199adantl 454 . . . . . . . . . . . . . . . . . . 19  |-  ( ( s  e.  { suc  k }  /\  t  e.  ( k F z ) )  ->  (
( h `  suc  k )  =  <. s ,  t >.  ->  (
( h `  k
)  =  <. k ,  z >.  ->  (
( h : om --> ( om  X.  A )  /\  k  e.  om )  ->  ( ( 2nd 
o.  h ) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `
 k ) ) ) ) ) )
201200impcom 421 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
s  e.  { suc  k }  /\  t  e.  ( k F z ) ) )  -> 
( ( h `  k )  =  <. k ,  z >.  ->  (
( h : om --> ( om  X.  A )  /\  k  e.  om )  ->  ( ( 2nd 
o.  h ) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `
 k ) ) ) ) )
202201exlimivv 1647 . . . . . . . . . . . . . . . . 17  |-  ( E. s E. t ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
s  e.  { suc  k }  /\  t  e.  ( k F z ) ) )  -> 
( ( h `  k )  =  <. k ,  z >.  ->  (
( h : om --> ( om  X.  A )  /\  k  e.  om )  ->  ( ( 2nd 
o.  h ) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `
 k ) ) ) ) )
203175, 202sylbi 189 . . . . . . . . . . . . . . . 16  |-  ( ( h `  suc  k
)  e.  ( { suc  k }  X.  ( k F z ) )  ->  (
( h `  k
)  =  <. k ,  z >.  ->  (
( h : om --> ( om  X.  A )  /\  k  e.  om )  ->  ( ( 2nd 
o.  h ) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `
 k ) ) ) ) )
204203com3l 78 . . . . . . . . . . . . . . 15  |-  ( ( h `  k )  =  <. k ,  z
>.  ->  ( ( h : om --> ( om 
X.  A )  /\  k  e.  om )  ->  ( ( h `  suc  k )  e.  ( { suc  k }  X.  ( k F z ) )  -> 
( ( 2nd  o.  h ) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `
 k ) ) ) ) )
205204imp 420 . . . . . . . . . . . . . 14  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( (
h `  suc  k )  e.  ( { suc  k }  X.  (
k F z ) )  ->  ( ( 2nd  o.  h ) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `
 k ) ) ) )
206174, 205sylbid 208 . . . . . . . . . . . . 13  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( (
h `  suc  k )  e.  ( G `  ( h `  k
) )  ->  (
( 2nd  o.  h
) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `  k
) ) ) )
207206ex 425 . . . . . . . . . . . 12  |-  ( ( h `  k )  =  <. k ,  z
>.  ->  ( ( h : om --> ( om 
X.  A )  /\  k  e.  om )  ->  ( ( h `  suc  k )  e.  ( G `  ( h `
 k ) )  ->  ( ( 2nd 
o.  h ) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `
 k ) ) ) ) )
208207exlimiv 1646 . . . . . . . . . . 11  |-  ( E. z ( h `  k )  =  <. k ,  z >.  ->  (
( h : om --> ( om  X.  A )  /\  k  e.  om )  ->  ( ( h `
 suc  k )  e.  ( G `  (
h `  k )
)  ->  ( ( 2nd  o.  h ) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `
 k ) ) ) ) )
2092083imp 1148 . . . . . . . . . 10  |-  ( ( E. z ( h `
 k )  = 
<. k ,  z >.  /\  ( h : om --> ( om  X.  A )  /\  k  e.  om )  /\  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  ->  ( ( 2nd  o.  h ) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `
 k ) ) )
210144, 145, 146, 150, 209syl121anc 1190 . . . . . . . . 9  |-  ( ( C  e.  A  /\  ( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  /\  k  e. 
om )  ->  (
( 2nd  o.  h
) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `  k
) ) )
2112103expia 1156 . . . . . . . 8  |-  ( ( C  e.  A  /\  ( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )  ->  (
k  e.  om  ->  ( ( 2nd  o.  h
) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `  k
) ) ) )
21264, 211ralrimi 2794 . . . . . . 7  |-  ( ( C  e.  A  /\  ( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )  ->  A. k  e.  om  ( ( 2nd 
o.  h ) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `
 k ) ) )
21346, 58, 2123jca 1135 . . . . . 6  |-  ( ( C  e.  A  /\  ( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )  ->  (
( 2nd  o.  h
) : om --> A  /\  ( ( 2nd  o.  h ) `  (/) )  =  C  /\  A. k  e.  om  ( ( 2nd 
o.  h ) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `
 k ) ) ) )
214 feq1 5611 . . . . . . . 8  |-  ( g  =  ( 2nd  o.  h )  ->  (
g : om --> A  <->  ( 2nd  o.  h ) : om --> A ) )
215 fveq1 5762 . . . . . . . . 9  |-  ( g  =  ( 2nd  o.  h )  ->  (
g `  (/) )  =  ( ( 2nd  o.  h ) `  (/) ) )
216215eqeq1d 2451 . . . . . . . 8  |-  ( g  =  ( 2nd  o.  h )  ->  (
( g `  (/) )  =  C  <->  ( ( 2nd 
o.  h ) `  (/) )  =  C ) )
217 fveq1 5762 . . . . . . . . . 10  |-  ( g  =  ( 2nd  o.  h )  ->  (
g `  suc  k )  =  ( ( 2nd 
o.  h ) `  suc  k ) )
218 fveq1 5762 . . . . . . . . . . 11  |-  ( g  =  ( 2nd  o.  h )  ->  (
g `  k )  =  ( ( 2nd 
o.  h ) `  k ) )
219218oveq2d 6133 . . . . . . . . . 10  |-  ( g  =  ( 2nd  o.  h )  ->  (
k F ( g `
 k ) )  =  ( k F ( ( 2nd  o.  h ) `  k
) ) )
220217, 219eleq12d 2511 . . . . . . . . 9  |-  ( g  =  ( 2nd  o.  h )  ->  (
( g `  suc  k )  e.  ( k F ( g `
 k ) )  <-> 
( ( 2nd  o.  h ) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `
 k ) ) ) )
221220ralbidv 2732 . . . . . . . 8  |-  ( g  =  ( 2nd  o.  h )  ->  ( A. k  e.  om  ( g `  suc  k )  e.  ( k F ( g `
 k ) )  <->  A. k  e.  om  ( ( 2nd  o.  h ) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `
 k ) ) ) )
222214, 216, 2213anbi123d 1255 . . . . . . 7  |-  ( g  =  ( 2nd  o.  h )  ->  (
( g : om --> A  /\  ( g `  (/) )  =  C  /\  A. k  e.  om  (
g `  suc  k )  e.  ( k F ( g `  k
) ) )  <->  ( ( 2nd  o.  h ) : om --> A  /\  (
( 2nd  o.  h
) `  (/) )  =  C  /\  A. k  e.  om  ( ( 2nd 
o.  h ) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `
 k ) ) ) ) )
223222spcegv 3046 . . . . . 6  |-  ( ( 2nd  o.  h )  e.  _V  ->  (
( ( 2nd  o.  h ) : om --> A  /\  ( ( 2nd 
o.  h ) `  (/) )  =  C  /\  A. k  e.  om  (
( 2nd  o.  h
) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `  k
) ) )  ->  E. g ( g : om --> A  /\  (
g `  (/) )  =  C  /\  A. k  e.  om  ( g `  suc  k )  e.  ( k F ( g `
 k ) ) ) ) )
22449, 213, 223sylc 59 . . . . 5  |-  ( ( C  e.  A  /\  ( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )  ->  E. g
( g : om --> A  /\  ( g `  (/) )  =  C  /\  A. k  e.  om  (
g `  suc  k )  e.  ( k F ( g `  k
) ) ) )
225224ex 425 . . . 4  |-  ( C  e.  A  ->  (
( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  ->  E. g
( g : om --> A  /\  ( g `  (/) )  =  C  /\  A. k  e.  om  (
g `  suc  k )  e.  ( k F ( g `  k
) ) ) ) )
226225exlimdv 1648 . . 3  |-  ( C  e.  A  ->  ( E. h ( h : om --> ( om  X.  A )  /\  (
h `  (/) )  = 
<. (/) ,  C >.  /\ 
A. k  e.  om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  ->  E. g
( g : om --> A  /\  ( g `  (/) )  =  C  /\  A. k  e.  om  (
g `  suc  k )  e.  ( k F ( g `  k
) ) ) ) )
227226adantr 453 . 2  |-  ( ( C  e.  A  /\  F : ( om  X.  A ) --> ( ~P A  \  { (/) } ) )  ->  ( E. h ( h : om --> ( om  X.  A )  /\  (
h `  (/) )  = 
<. (/) ,  C >.  /\ 
A. k  e.  om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  ->  E. g
( g : om --> A  /\  ( g `  (/) )  =  C  /\  A. k  e.  om  (
g `  suc  k )  e.  ( k F ( g `  k
) ) ) ) )
22843, 227mpd 15 1  |-  ( ( C  e.  A  /\  F : ( om  X.  A ) --> ( ~P A  \  { (/) } ) )  ->  E. g
( g : om --> A  /\  ( g `  (/) )  =  C  /\  A. k  e.  om  (
g `  suc  k )  e.  ( k F ( g `  k
) ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 360    /\ w3a 937   E.wex 1551    = wceq 1654    e. wcel 1728    =/= wne 2606   A.wral 2712   _Vcvv 2965    \ cdif 3306    C_ wss 3309   (/)c0 3616   ~Pcpw 3828   {csn 3843   <.cop 3846   suc csuc 4618   omcom 4880    X. cxp 4911    o. ccom 4917   -->wf 5485   ` cfv 5489  (class class class)co 6117    e. cmpt2 6119   2ndc2nd 6384
This theorem is referenced by:  axdc4  8374
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-13 1730  ax-14 1732  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424  ax-sep 4361  ax-nul 4369  ax-pow 4412  ax-pr 4438  ax-un 4736  ax-dc 8364
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-eu 2292  df-mo 2293  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2717  df-rex 2718  df-reu 2719  df-rab 2721  df-v 2967  df-sbc 3171  df-csb 3271  df-dif 3312  df-un 3314  df-in 3316  df-ss 3323  df-pss 3325  df-nul 3617  df-if 3768  df-pw 3830  df-sn 3849  df-pr 3850  df-tp 3851  df-op 3852  df-uni 4045  df-iun 4124  df-br 4244  df-opab 4298  df-mpt 4299  df-tr 4334  df-eprel 4529  df-id 4533  df-po 4538  df-so 4539  df-fr 4576  df-we 4578  df-ord 4619  df-on 4620  df-lim 4621  df-suc 4622  df-om 4881  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5453  df-fun 5491  df-fn 5492  df-f 5493  df-f1 5494  df-fo 5495  df-f1o 5496  df-fv 5497  df-ov 6120  df-oprab 6121  df-mpt2 6122  df-1st 6385  df-2nd 6386  df-1o 6760
  Copyright terms: Public domain W3C validator