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

Theorem axdc4lem 8081
Description: Lemma for axdc4 8082. (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 4675 . . . 4  |-  (/)  e.  om
2 opelxpi 4721 . . . 4  |-  ( (
(/)  e.  om  /\  C  e.  A )  ->  <. (/) ,  C >.  e.  ( om  X.  A ) )
31, 2mpan 651 . . 3  |-  ( C  e.  A  ->  <. (/) ,  C >.  e.  ( om  X.  A ) )
4 simp2 956 . . . . . . . 8  |-  ( ( F : ( om 
X.  A ) --> ( ~P A  \  { (/)
} )  /\  n  e.  om  /\  x  e.  A )  ->  n  e.  om )
5 fovrn 5990 . . . . . . . 8  |-  ( ( F : ( om 
X.  A ) --> ( ~P A  \  { (/)
} )  /\  n  e.  om  /\  x  e.  A )  ->  (
n F x )  e.  ( ~P A  \  { (/) } ) )
6 peano2 4676 . . . . . . . . . . 11  |-  ( n  e.  om  ->  suc  n  e.  om )
76snssd 3760 . . . . . . . . . 10  |-  ( n  e.  om  ->  { suc  n }  C_  om )
8 eldifi 3298 . . . . . . . . . 10  |-  ( ( n F x )  e.  ( ~P A  \  { (/) } )  -> 
( n F x )  e.  ~P A
)
9 axdc4lem.1 . . . . . . . . . . . 12  |-  A  e. 
_V
109elpw2 4175 . . . . . . . . . . 11  |-  ( ( n F x )  e.  ~P A  <->  ( n F x )  C_  A )
11 xpss12 4792 . . . . . . . . . . 11  |-  ( ( { suc  n }  C_ 
om  /\  ( n F x )  C_  A )  ->  ( { suc  n }  X.  ( n F x ) )  C_  ( om  X.  A ) )
1210, 11sylan2b 461 . . . . . . . . . 10  |-  ( ( { suc  n }  C_ 
om  /\  ( n F x )  e. 
~P A )  -> 
( { suc  n }  X.  ( n F x ) )  C_  ( om  X.  A ) )
137, 8, 12syl2an 463 . . . . . . . . 9  |-  ( ( n  e.  om  /\  ( n F x )  e.  ( ~P A  \  { (/) } ) )  ->  ( { suc  n }  X.  ( n F x ) )  C_  ( om  X.  A ) )
14 snex 4216 . . . . . . . . . . 11  |-  { suc  n }  e.  _V
15 ovex 5883 . . . . . . . . . . 11  |-  ( n F x )  e. 
_V
1614, 15xpex 4801 . . . . . . . . . 10  |-  ( { suc  n }  X.  ( n F x ) )  e.  _V
1716elpw 3631 . . . . . . . . 9  |-  ( ( { suc  n }  X.  ( n F x ) )  e.  ~P ( om  X.  A )  <-> 
( { suc  n }  X.  ( n F x ) )  C_  ( om  X.  A ) )
1813, 17sylibr 203 . . . . . . . 8  |-  ( ( n  e.  om  /\  ( n F x )  e.  ( ~P A  \  { (/) } ) )  ->  ( { suc  n }  X.  ( n F x ) )  e.  ~P ( om  X.  A ) )
194, 5, 18syl2anc 642 . . . . . . 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 3299 . . . . . . . 8  |-  ( ( n F x )  e.  ( ~P A  \  { (/) } )  ->  -.  ( n F x )  e.  { (/) } )
2115elsnc 3663 . . . . . . . . . . 11  |-  ( ( n F x )  e.  { (/) }  <->  ( n F x )  =  (/) )
2221necon3bbii 2477 . . . . . . . . . 10  |-  ( -.  ( n F x )  e.  { (/) }  <-> 
( n F x )  =/=  (/) )
23 vex 2791 . . . . . . . . . . . . 13  |-  n  e. 
_V
2423sucex 4602 . . . . . . . . . . . 12  |-  suc  n  e.  _V
2524snnz 3744 . . . . . . . . . . 11  |-  { suc  n }  =/=  (/)
26 xpnz 5099 . . . . . . . . . . . 12  |-  ( ( { suc  n }  =/=  (/)  /\  ( n F x )  =/=  (/) )  <->  ( { suc  n }  X.  (
n F x ) )  =/=  (/) )
2726biimpi 186 . . . . . . . . . . 11  |-  ( ( { suc  n }  =/=  (/)  /\  ( n F x )  =/=  (/) )  ->  ( { suc  n }  X.  ( n F x ) )  =/=  (/) )
2825, 27mpan 651 . . . . . . . . . 10  |-  ( ( n F x )  =/=  (/)  ->  ( { suc  n }  X.  (
n F x ) )  =/=  (/) )
2922, 28sylbi 187 . . . . . . . . 9  |-  ( -.  ( n F x )  e.  { (/) }  ->  ( { suc  n }  X.  (
n F x ) )  =/=  (/) )
3016elsnc 3663 . . . . . . . . . 10  |-  ( ( { suc  n }  X.  ( n F x ) )  e.  { (/)
}  <->  ( { suc  n }  X.  (
n F x ) )  =  (/) )
3130necon3bbii 2477 . . . . . . . . 9  |-  ( -.  ( { suc  n }  X.  ( n F x ) )  e. 
{ (/) }  <->  ( { suc  n }  X.  (
n F x ) )  =/=  (/) )
3229, 31sylibr 203 . . . . . . . 8  |-  ( -.  ( n F x )  e.  { (/) }  ->  -.  ( { suc  n }  X.  (
n F x ) )  e.  { (/) } )
335, 20, 323syl 18 . . . . . . 7  |-  ( ( F : ( om 
X.  A ) --> ( ~P A  \  { (/)
} )  /\  n  e.  om  /\  x  e.  A )  ->  -.  ( { suc  n }  X.  ( n F x ) )  e.  { (/)
} )
34 eldif 3162 . . . . . . 7  |-  ( ( { suc  n }  X.  ( n F x ) )  e.  ( ~P ( om  X.  A )  \  { (/)
} )  <->  ( ( { suc  n }  X.  ( n F x ) )  e.  ~P ( om  X.  A )  /\  -.  ( { suc  n }  X.  ( n F x ) )  e.  { (/)
} ) )
3519, 33, 34sylanbrc 645 . . . . . 6  |-  ( ( F : ( om 
X.  A ) --> ( ~P A  \  { (/)
} )  /\  n  e.  om  /\  x  e.  A )  ->  ( { suc  n }  X.  ( n F x ) )  e.  ( ~P ( om  X.  A )  \  { (/)
} ) )
36353expib 1154 . . . . 5  |-  ( F : ( om  X.  A ) --> ( ~P A  \  { (/) } )  ->  ( (
n  e.  om  /\  x  e.  A )  ->  ( { suc  n }  X.  ( n F x ) )  e.  ( ~P ( om 
X.  A )  \  { (/) } ) ) )
3736ralrimivv 2634 . . . 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
)  \  { (/) } ) )
38 axdc4lem.2 . . . . 5  |-  G  =  ( n  e.  om ,  x  e.  A  |->  ( { suc  n }  X.  ( n F x ) ) )
3938fmpt2 6191 . . . 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 )  \  { (/)
} ) )
4037, 39sylib 188 . . 3  |-  ( F : ( om  X.  A ) --> ( ~P A  \  { (/) } )  ->  G :
( om  X.  A
) --> ( ~P ( om  X.  A )  \  { (/) } ) )
41 dcomex 8073 . . . . 5  |-  om  e.  _V
4241, 9xpex 4801 . . . 4  |-  ( om 
X.  A )  e. 
_V
4342axdc3 8080 . . 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 ) ) ) )
443, 40, 43syl2an 463 . 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 ) ) ) )
45 2ndcof 6148 . . . . . . . . 9  |-  ( h : om --> ( om 
X.  A )  -> 
( 2nd  o.  h
) : om --> A )
46453ad2ant1 976 . . . . . . . 8  |-  ( ( h : om --> ( om 
X.  A )  /\  ( h `  (/) )  = 
<. (/) ,  C >.  /\ 
A. k  e.  om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  ->  ( 2nd  o.  h ) : om --> A )
4746adantl 452 . . . . . . 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 )
48 fex2 5401 . . . . . . . 8  |-  ( ( ( 2nd  o.  h
) : om --> A  /\  om  e.  _V  /\  A  e.  _V )  ->  ( 2nd  o.  h )  e. 
_V )
4941, 9, 48mp3an23 1269 . . . . . . 7  |-  ( ( 2nd  o.  h ) : om --> A  -> 
( 2nd  o.  h
)  e.  _V )
5047, 49syl 15 . . . . . 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 )
51 fvco3 5596 . . . . . . . . . . 11  |-  ( ( h : om --> ( om 
X.  A )  /\  (/) 
e.  om )  ->  (
( 2nd  o.  h
) `  (/) )  =  ( 2nd `  (
h `  (/) ) ) )
521, 51mpan2 652 . . . . . . . . . 10  |-  ( h : om --> ( om 
X.  A )  -> 
( ( 2nd  o.  h ) `  (/) )  =  ( 2nd `  (
h `  (/) ) ) )
53523ad2ant1 976 . . . . . . . . 9  |-  ( ( h : om --> ( om 
X.  A )  /\  ( h `  (/) )  = 
<. (/) ,  C >.  /\ 
A. k  e.  om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  ->  ( ( 2nd  o.  h ) `  (/) )  =  ( 2nd `  ( h `  (/) ) ) )
54 fveq2 5525 . . . . . . . . . 10  |-  ( ( h `  (/) )  = 
<. (/) ,  C >.  -> 
( 2nd `  (
h `  (/) ) )  =  ( 2nd `  <. (/)
,  C >. )
)
55543ad2ant2 977 . . . . . . . . 9  |-  ( ( h : om --> ( om 
X.  A )  /\  ( h `  (/) )  = 
<. (/) ,  C >.  /\ 
A. k  e.  om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  ->  ( 2nd `  ( h `  (/) ) )  =  ( 2nd `  <. (/)
,  C >. )
)
5653, 55eqtrd 2315 . . . . . . . 8  |-  ( ( h : om --> ( om 
X.  A )  /\  ( h `  (/) )  = 
<. (/) ,  C >.  /\ 
A. k  e.  om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  ->  ( ( 2nd  o.  h ) `  (/) )  =  ( 2nd `  <. (/) ,  C >. ) )
57 op2ndg 6133 . . . . . . . . 9  |-  ( (
(/)  e.  om  /\  C  e.  A )  ->  ( 2nd `  <. (/) ,  C >. )  =  C )
581, 57mpan 651 . . . . . . . 8  |-  ( C  e.  A  ->  ( 2nd `  <. (/) ,  C >. )  =  C )
5956, 58sylan9eqr 2337 . . . . . . 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 )
60 nfv 1605 . . . . . . . . 9  |-  F/ k  C  e.  A
61 nfv 1605 . . . . . . . . . 10  |-  F/ k  h : om --> ( om 
X.  A )
62 nfv 1605 . . . . . . . . . 10  |-  F/ k ( h `  (/) )  = 
<. (/) ,  C >.
63 nfra1 2593 . . . . . . . . . 10  |-  F/ k A. k  e.  om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) )
6461, 62, 63nf3an 1774 . . . . . . . . 9  |-  F/ k ( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )
6560, 64nfan 1771 . . . . . . . 8  |-  F/ k ( C  e.  A  /\  ( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )
66 fveq2 5525 . . . . . . . . . . . . . . . . 17  |-  ( m  =  (/)  ->  ( h `
 m )  =  ( h `  (/) ) )
67 opeq1 3796 . . . . . . . . . . . . . . . . 17  |-  ( m  =  (/)  ->  <. m ,  z >.  =  <. (/)
,  z >. )
6866, 67eqeq12d 2297 . . . . . . . . . . . . . . . 16  |-  ( m  =  (/)  ->  ( ( h `  m )  =  <. m ,  z
>. 
<->  ( h `  (/) )  = 
<. (/) ,  z >.
) )
6968exbidv 1612 . . . . . . . . . . . . . . 15  |-  ( m  =  (/)  ->  ( E. z ( h `  m )  =  <. m ,  z >.  <->  E. z
( h `  (/) )  = 
<. (/) ,  z >.
) )
70 fveq2 5525 . . . . . . . . . . . . . . . . 17  |-  ( m  =  i  ->  (
h `  m )  =  ( h `  i ) )
71 opeq1 3796 . . . . . . . . . . . . . . . . 17  |-  ( m  =  i  ->  <. m ,  z >.  =  <. i ,  z >. )
7270, 71eqeq12d 2297 . . . . . . . . . . . . . . . 16  |-  ( m  =  i  ->  (
( h `  m
)  =  <. m ,  z >.  <->  ( h `  i )  =  <. i ,  z >. )
)
7372exbidv 1612 . . . . . . . . . . . . . . 15  |-  ( m  =  i  ->  ( E. z ( h `  m )  =  <. m ,  z >.  <->  E. z
( h `  i
)  =  <. i ,  z >. )
)
74 fveq2 5525 . . . . . . . . . . . . . . . . 17  |-  ( m  =  suc  i  -> 
( h `  m
)  =  ( h `
 suc  i )
)
75 opeq1 3796 . . . . . . . . . . . . . . . . 17  |-  ( m  =  suc  i  ->  <. m ,  z >.  =  <. suc  i , 
z >. )
7674, 75eqeq12d 2297 . . . . . . . . . . . . . . . 16  |-  ( m  =  suc  i  -> 
( ( h `  m )  =  <. m ,  z >.  <->  ( h `  suc  i )  = 
<. suc  i ,  z
>. ) )
7776exbidv 1612 . . . . . . . . . . . . . . 15  |-  ( m  =  suc  i  -> 
( E. z ( h `  m )  =  <. m ,  z
>. 
<->  E. z ( h `
 suc  i )  =  <. suc  i , 
z >. ) )
78 opeq2 3797 . . . . . . . . . . . . . . . . . . 19  |-  ( z  =  C  ->  <. (/) ,  z
>.  =  <. (/) ,  C >. )
7978eqeq2d 2294 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  C  ->  (
( h `  (/) )  = 
<. (/) ,  z >.  <->  ( h `  (/) )  = 
<. (/) ,  C >. ) )
8079spcegv 2869 . . . . . . . . . . . . . . . . 17  |-  ( C  e.  A  ->  (
( h `  (/) )  = 
<. (/) ,  C >.  ->  E. z ( h `  (/) )  =  <. (/) ,  z
>. ) )
8180imp 418 . . . . . . . . . . . . . . . 16  |-  ( ( C  e.  A  /\  ( h `  (/) )  = 
<. (/) ,  C >. )  ->  E. z ( h `
 (/) )  =  <. (/)
,  z >. )
82813ad2antr2 1121 . . . . . . . . . . . . . . 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 >.
)
83 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( h `  i )  =  <. i ,  z
>.  ->  ( G `  ( h `  i
) )  =  ( G `  <. i ,  z >. )
)
84 df-ov 5861 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( i G z )  =  ( G `  <. i ,  z >. )
8583, 84syl6eqr 2333 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( h `  i )  =  <. i ,  z
>.  ->  ( G `  ( h `  i
) )  =  ( i G z ) )
8685adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( h : om --> ( om  X.  A )  /\  i  e.  om )  /\  ( h `  i )  =  <. i ,  z >. )  ->  ( G `  (
h `  i )
)  =  ( i G z ) )
87 simplr 731 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( h : om --> ( om  X.  A )  /\  i  e.  om )  /\  ( h `  i )  =  <. i ,  z >. )  ->  i  e.  om )
88 ffvelrn 5663 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( h : om --> ( om 
X.  A )  /\  i  e.  om )  ->  ( h `  i
)  e.  ( om 
X.  A ) )
89 eleq1 2343 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( h `  i )  =  <. i ,  z
>.  ->  ( ( h `
 i )  e.  ( om  X.  A
)  <->  <. i ,  z
>.  e.  ( om  X.  A ) ) )
90 opelxp2 4723 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( <.
i ,  z >.  e.  ( om  X.  A
)  ->  z  e.  A )
9189, 90syl6bi 219 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( h `  i )  =  <. i ,  z
>.  ->  ( ( h `
 i )  e.  ( om  X.  A
)  ->  z  e.  A ) )
9288, 91mpan9 455 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( h : om --> ( om  X.  A )  /\  i  e.  om )  /\  ( h `  i )  =  <. i ,  z >. )  ->  z  e.  A )
93 suceq 4457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( n  =  i  ->  suc  n  =  suc  i )
9493sneqd 3653 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( n  =  i  ->  { suc  n }  =  { suc  i } )
95 oveq1 5865 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( n  =  i  ->  (
n F x )  =  ( i F x ) )
9694, 95xpeq12d 4714 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( n  =  i  ->  ( { suc  n }  X.  ( n F x ) )  =  ( { suc  i }  X.  ( i F x ) ) )
97 oveq2 5866 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  =  z  ->  (
i F x )  =  ( i F z ) )
9897xpeq2d 4713 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  =  z  ->  ( { suc  i }  X.  ( i F x ) )  =  ( { suc  i }  X.  ( i F z ) ) )
99 snex 4216 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  { suc  i }  e.  _V
100 ovex 5883 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( i F z )  e. 
_V
10199, 100xpex 4801 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( { suc  i }  X.  ( i F z ) )  e.  _V
10296, 98, 38, 101ovmpt2 5983 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( i  e.  om  /\  z  e.  A )  ->  ( i G z )  =  ( { suc  i }  X.  ( i F z ) ) )
10387, 92, 102syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( h : om --> ( om  X.  A )  /\  i  e.  om )  /\  ( h `  i )  =  <. i ,  z >. )  ->  ( i G z )  =  ( { suc  i }  X.  ( i F z ) ) )
10486, 103eqtrd 2315 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( h : om --> ( om  X.  A )  /\  i  e.  om )  /\  ( h `  i )  =  <. i ,  z >. )  ->  ( G `  (
h `  i )
)  =  ( { suc  i }  X.  ( i F z ) ) )
105 suceq 4457 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( k  =  i  ->  suc  k  =  suc  i )
106105fveq2d 5529 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  =  i  ->  (
h `  suc  k )  =  ( h `  suc  i ) )
107 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( k  =  i  ->  (
h `  k )  =  ( h `  i ) )
108107fveq2d 5529 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  =  i  ->  ( G `  ( h `  k ) )  =  ( G `  (
h `  i )
) )
109106, 108eleq12d 2351 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( k  =  i  ->  (
( h `  suc  k )  e.  ( G `  ( h `
 k ) )  <-> 
( h `  suc  i )  e.  ( G `  ( h `
 i ) ) ) )
110109rspcv 2880 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( i  e.  om  ->  ( A. k  e.  om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) )  ->  ( h `  suc  i )  e.  ( G `  ( h `
 i ) ) ) )
111110ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
112 eleq2 2344 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
113 elxp 4706 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
114 elsn 3655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( s  e.  { suc  i } 
<->  s  =  suc  i
)
115 opeq1 3796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( s  =  suc  i  ->  <. s ,  t >.  =  <. suc  i , 
t >. )
116114, 115sylbi 187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( s  e.  { suc  i }  ->  <. s ,  t
>.  =  <. suc  i ,  t >. )
117116eqeq2d 2294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( s  e.  { suc  i }  ->  ( ( h `
 suc  i )  =  <. s ,  t
>. 
<->  ( h `  suc  i )  =  <. suc  i ,  t >.
) )
118117biimpac 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( h `  suc  i )  =  <. s ,  t >.  /\  s  e.  { suc  i } )  ->  ( h `  suc  i )  = 
<. suc  i ,  t
>. )
119118adantrr 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( h `  suc  i )  =  <. s ,  t >.  /\  (
s  e.  { suc  i }  /\  t  e.  ( i F z ) ) )  -> 
( h `  suc  i )  =  <. suc  i ,  t >.
)
120119eximi 1563 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 >.
)
121120exlimiv 1666 . . . . . . . . . . . . . . . . . . . . . . . . . 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 >.
)
122113, 121sylbi 187 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( h `  suc  i
)  e.  ( { suc  i }  X.  ( i F z ) )  ->  E. t
( h `  suc  i )  =  <. suc  i ,  t >.
)
123112, 122syl6bi 219 . . . . . . . . . . . . . . . . . . . . . . . 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 >.
) )
124104, 111, 123sylsyld 52 . . . . . . . . . . . . . . . . . . . . . . 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 >. ) )
125124expcom 424 . . . . . . . . . . . . . . . . . . . . . 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 >. ) ) )
126125exlimiv 1666 . . . . . . . . . . . . . . . . . . . . 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 >. ) ) )
127126com3l 75 . . . . . . . . . . . . . . . . . . . 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 >.
) ) )
128 opeq2 3797 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( t  =  z  ->  <. suc  i ,  t >.  =  <. suc  i ,  z >.
)
129128eqeq2d 2294 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  =  z  ->  (
( h `  suc  i )  =  <. suc  i ,  t >.  <->  ( h `  suc  i
)  =  <. suc  i ,  z >. )
)
130129cbvexv 1943 . . . . . . . . . . . . . . . . . . . 20  |-  ( E. t ( h `  suc  i )  =  <. suc  i ,  t >.  <->  E. z ( h `  suc  i )  =  <. suc  i ,  z >.
)
131127, 130syl8ib 222 . . . . . . . . . . . . . . . . . . 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 >.
) ) )
132131impancom 427 . . . . . . . . . . . . . . . . . 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 >. ) ) )
1331323adant2 974 . . . . . . . . . . . . . . . . 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 >.
) ) )
134133adantl 452 . . . . . . . . . . . . . . . 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 >. ) ) )
135134com12 27 . . . . . . . . . . . . . . 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 >.
) ) )
13669, 73, 77, 82, 135finds2 4684 . . . . . . . . . . . . . 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 >. )
)
137136com12 27 . . . . . . . . . . . . 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 >. )
)
138137ralrimiv 2625 . . . . . . . . . . . 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
>. )
139 fveq2 5525 . . . . . . . . . . . . . . 15  |-  ( m  =  k  ->  (
h `  m )  =  ( h `  k ) )
140 opeq1 3796 . . . . . . . . . . . . . . 15  |-  ( m  =  k  ->  <. m ,  z >.  =  <. k ,  z >. )
141139, 140eqeq12d 2297 . . . . . . . . . . . . . 14  |-  ( m  =  k  ->  (
( h `  m
)  =  <. m ,  z >.  <->  ( h `  k )  =  <. k ,  z >. )
)
142141exbidv 1612 . . . . . . . . . . . . 13  |-  ( m  =  k  ->  ( E. z ( h `  m )  =  <. m ,  z >.  <->  E. z
( h `  k
)  =  <. k ,  z >. )
)
143142rspccv 2881 . . . . . . . . . . . 12  |-  ( A. m  e.  om  E. z
( h `  m
)  =  <. m ,  z >.  ->  (
k  e.  om  ->  E. z ( h `  k )  =  <. k ,  z >. )
)
144138, 143syl 15 . . . . . . . . . . 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 >. )
)
1451443impia 1148 . . . . . . . . . 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 >. )
146 simp21 988 . . . . . . . . . 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 ) )
147 simp3 957 . . . . . . . . . 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 )
148 rsp 2603 . . . . . . . . . . . . 13  |-  ( A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) )  ->  (
k  e.  om  ->  ( h `  suc  k
)  e.  ( G `
 ( h `  k ) ) ) )
149148imp 418 . . . . . . . . . . . 12  |-  ( ( A. k  e.  om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) )  /\  k  e.  om )  ->  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )
1501493ad2antl3 1119 . . . . . . . . . . 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
) ) )
1511503adant1 973 . . . . . . . . . 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
) ) )
152 simpl 443 . . . . . . . . . . . . . . . . 17  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( h `  k )  =  <. k ,  z >. )
153152fveq2d 5529 . . . . . . . . . . . . . . . 16  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( G `  ( h `  k
) )  =  ( G `  <. k ,  z >. )
)
154 simprr 733 . . . . . . . . . . . . . . . . 17  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  k  e.  om )
155 ffvelrn 5663 . . . . . . . . . . . . . . . . . . 19  |-  ( ( h : om --> ( om 
X.  A )  /\  k  e.  om )  ->  ( h `  k
)  e.  ( om 
X.  A ) )
156 eleq1 2343 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( h `  k )  =  <. k ,  z
>.  ->  ( ( h `
 k )  e.  ( om  X.  A
)  <->  <. k ,  z
>.  e.  ( om  X.  A ) ) )
157 opelxp2 4723 . . . . . . . . . . . . . . . . . . . 20  |-  ( <.
k ,  z >.  e.  ( om  X.  A
)  ->  z  e.  A )
158156, 157syl6bi 219 . . . . . . . . . . . . . . . . . . 19  |-  ( ( h `  k )  =  <. k ,  z
>.  ->  ( ( h `
 k )  e.  ( om  X.  A
)  ->  z  e.  A ) )
159155, 158syl5 28 . . . . . . . . . . . . . . . . . 18  |-  ( ( h `  k )  =  <. k ,  z
>.  ->  ( ( h : om --> ( om 
X.  A )  /\  k  e.  om )  ->  z  e.  A ) )
160159imp 418 . . . . . . . . . . . . . . . . 17  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  z  e.  A )
161 df-ov 5861 . . . . . . . . . . . . . . . . . 18  |-  ( k G z )  =  ( G `  <. k ,  z >. )
162 suceq 4457 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  k  ->  suc  n  =  suc  k )
163162sneqd 3653 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  k  ->  { suc  n }  =  { suc  k } )
164 oveq1 5865 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  k  ->  (
n F x )  =  ( k F x ) )
165163, 164xpeq12d 4714 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  k  ->  ( { suc  n }  X.  ( n F x ) )  =  ( { suc  k }  X.  ( k F x ) ) )
166 oveq2 5866 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  z  ->  (
k F x )  =  ( k F z ) )
167166xpeq2d 4713 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  z  ->  ( { suc  k }  X.  ( k F x ) )  =  ( { suc  k }  X.  ( k F z ) ) )
168 snex 4216 . . . . . . . . . . . . . . . . . . . 20  |-  { suc  k }  e.  _V
169 ovex 5883 . . . . . . . . . . . . . . . . . . . 20  |-  ( k F z )  e. 
_V
170168, 169xpex 4801 . . . . . . . . . . . . . . . . . . 19  |-  ( { suc  k }  X.  ( k F z ) )  e.  _V
171165, 167, 38, 170ovmpt2 5983 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  om  /\  z  e.  A )  ->  ( k G z )  =  ( { suc  k }  X.  ( k F z ) ) )
172161, 171syl5eqr 2329 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  om  /\  z  e.  A )  ->  ( G `  <. k ,  z >. )  =  ( { suc  k }  X.  (
k F z ) ) )
173154, 160, 172syl2anc 642 . . . . . . . . . . . . . . . 16  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( G `  <. k ,  z
>. )  =  ( { suc  k }  X.  ( k F z ) ) )
174153, 173eqtrd 2315 . . . . . . . . . . . . . . 15  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( G `  ( h `  k
) )  =  ( { suc  k }  X.  ( k F z ) ) )
175174eleq2d 2350 . . . . . . . . . . . . . 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 ) ) ) )
176 elxp 4706 . . . . . . . . . . . . . . . . 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 ) ) ) )
177 peano2 4676 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  e.  om  ->  suc  k  e.  om )
178 fvco3 5596 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( h : om --> ( om 
X.  A )  /\  suc  k  e.  om )  ->  ( ( 2nd 
o.  h ) `  suc  k )  =  ( 2nd `  ( h `
 suc  k )
) )
179177, 178sylan2 460 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( h : om --> ( om 
X.  A )  /\  k  e.  om )  ->  ( ( 2nd  o.  h ) `  suc  k )  =  ( 2nd `  ( h `
 suc  k )
) )
180179adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
181 simpll 730 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( h `  suc  k )  = 
<. s ,  t >.
)
182181fveq2d 5529 . . . . . . . . . . . . . . . . . . . . . . . . 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 >. )
)
183180, 182eqtrd 2315 . . . . . . . . . . . . . . . . . . . . . . . 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 >. )
)
184 vex 2791 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  s  e. 
_V
185 vex 2791 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  t  e. 
_V
186184, 185op2nd 6129 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 2nd `  <. s ,  t
>. )  =  t
187183, 186syl6eq 2331 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( ( 2nd  o.  h ) `  suc  k )  =  t )
188 fvco3 5596 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( h : om --> ( om 
X.  A )  /\  k  e.  om )  ->  ( ( 2nd  o.  h ) `  k
)  =  ( 2nd `  ( h `  k
) ) )
189188adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
190 simplr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( h `  k )  =  <. k ,  z >. )
191190fveq2d 5529 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( 2nd `  ( h `  k
) )  =  ( 2nd `  <. k ,  z >. )
)
192189, 191eqtrd 2315 . . . . . . . . . . . . . . . . . . . . . . . . 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 >. )
)
193 vex 2791 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  k  e. 
_V
194 vex 2791 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  z  e. 
_V
195193, 194op2nd 6129 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 2nd `  <. k ,  z
>. )  =  z
196192, 195syl6eq 2331 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( ( 2nd  o.  h ) `  k )  =  z )
197196oveq2d 5874 . . . . . . . . . . . . . . . . . . . . . . 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 ) )
198187, 197eleq12d 2351 . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
199198biimprcd 216 . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
200199exp4c 591 . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
201200adantl 452 . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
202201impcom 419 . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
203202exlimivv 1667 . . . . . . . . . . . . . . . . 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 ) ) ) ) )
204176, 203sylbi 187 . . . . . . . . . . . . . . . 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 ) ) ) ) )
205204com3l 75 . . . . . . . . . . . . . . 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 ) ) ) ) )
206205imp 418 . . . . . . . . . . . . . 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 ) ) ) )
207175, 206sylbid 206 . . . . . . . . . . . . 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
) ) ) )
208207ex 423 . . . . . . . . . . . 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 ) ) ) ) )
209208exlimiv 1666 . . . . . . . . . . 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 ) ) ) ) )
2102093imp 1145 . . . . . . . . . 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 ) ) )
211145, 146, 147, 151, 210syl121anc 1187 . . . . . . . . 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
) ) )
2122113expia 1153 . . . . . . . 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
) ) ) )
21365, 212ralrimi 2624 . . . . . . 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 ) ) )
21447, 59, 2133jca 1132 . . . . . 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 ) ) ) )
215 feq1 5375 . . . . . . . 8  |-  ( g  =  ( 2nd  o.  h )  ->  (
g : om --> A  <->  ( 2nd  o.  h ) : om --> A ) )
216 fveq1 5524 . . . . . . . . 9  |-  ( g  =  ( 2nd  o.  h )  ->  (
g `  (/) )  =  ( ( 2nd  o.  h ) `  (/) ) )
217216eqeq1d 2291 . . . . . . . 8  |-  ( g  =  ( 2nd  o.  h )  ->  (
( g `  (/) )  =  C  <->  ( ( 2nd 
o.  h ) `  (/) )  =  C ) )
218 fveq1 5524 . . . . . . . . . 10  |-  ( g  =  ( 2nd  o.  h )  ->  (
g `  suc  k )  =  ( ( 2nd 
o.  h ) `  suc  k ) )
219 fveq1 5524 . . . . . . . . . . 11  |-  ( g  =  ( 2nd  o.  h )  ->  (
g `  k )  =  ( ( 2nd 
o.  h ) `  k ) )
220219oveq2d 5874 . . . . . . . . . 10  |-  ( g  =  ( 2nd  o.  h )  ->  (
k F ( g `
 k ) )  =  ( k F ( ( 2nd  o.  h ) `  k
) ) )
221218, 220eleq12d 2351 . . . . . . . . 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 ) ) ) )
222221ralbidv 2563 . . . . . . . 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 ) ) ) )
223215, 217, 2223anbi123d 1252 . . . . . . 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 ) ) ) ) )
224223spcegv 2869 . . . . . 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 ) ) ) ) )
22550, 214, 224sylc 56 . . . . 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
) ) ) )
226225ex 423 . . . 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
) ) ) ) )
227226exlimdv 1664 . . 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
) ) ) ) )
228227adantr 451 . 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
) ) ) ) )
22944, 228mpd 14 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 358    /\ w3a 934   E.wex 1528    = wceq 1623    e. wcel 1684    =/= wne 2446   A.wral 2543   _Vcvv 2788    \ cdif 3149    C_ wss 3152   (/)c0 3455   ~Pcpw 3625   {csn 3640   <.cop 3643   suc csuc 4394   omcom 4656    X. cxp 4687    o. ccom 4693   -->wf 5251   ` cfv 5255  (class class class)co 5858    e. cmpt2 5860   2ndc2nd 6121
This theorem is referenced by:  axdc4  8082
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-dc 8072
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-reu 2550  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-1st 6122  df-2nd 6123  df-1o 6479
  Copyright terms: Public domain W3C validator