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

Theorem axdc4lem 8836
Description: Lemma for axdc4 8837. (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 6670 . . . 4  |-  (/)  e.  om
2 opelxpi 4828 . . . 4  |-  ( (
(/)  e.  om  /\  C  e.  A )  ->  <. (/) ,  C >.  e.  ( om  X.  A ) )
31, 2mpan 674 . . 3  |-  ( C  e.  A  ->  <. (/) ,  C >.  e.  ( om  X.  A ) )
4 simp2 1006 . . . . . . . 8  |-  ( ( F : ( om 
X.  A ) --> ( ~P A  \  { (/)
} )  /\  n  e.  om  /\  x  e.  A )  ->  n  e.  om )
5 fovrn 6397 . . . . . . . 8  |-  ( ( F : ( om 
X.  A ) --> ( ~P A  \  { (/)
} )  /\  n  e.  om  /\  x  e.  A )  ->  (
n F x )  e.  ( ~P A  \  { (/) } ) )
6 peano2 6671 . . . . . . . . . . 11  |-  ( n  e.  om  ->  suc  n  e.  om )
76snssd 4088 . . . . . . . . . 10  |-  ( n  e.  om  ->  { suc  n }  C_  om )
8 eldifi 3530 . . . . . . . . . 10  |-  ( ( n F x )  e.  ( ~P A  \  { (/) } )  -> 
( n F x )  e.  ~P A
)
9 axdc4lem.1 . . . . . . . . . . . 12  |-  A  e. 
_V
109elpw2 4531 . . . . . . . . . . 11  |-  ( ( n F x )  e.  ~P A  <->  ( n F x )  C_  A )
11 xpss12 4902 . . . . . . . . . . 11  |-  ( ( { suc  n }  C_ 
om  /\  ( n F x )  C_  A )  ->  ( { suc  n }  X.  ( n F x ) )  C_  ( om  X.  A ) )
1210, 11sylan2b 477 . . . . . . . . . 10  |-  ( ( { suc  n }  C_ 
om  /\  ( n F x )  e. 
~P A )  -> 
( { suc  n }  X.  ( n F x ) )  C_  ( om  X.  A ) )
137, 8, 12syl2an 479 . . . . . . . . 9  |-  ( ( n  e.  om  /\  ( n F x )  e.  ( ~P A  \  { (/) } ) )  ->  ( { suc  n }  X.  ( n F x ) )  C_  ( om  X.  A ) )
14 snex 4605 . . . . . . . . . . 11  |-  { suc  n }  e.  _V
15 ovex 6277 . . . . . . . . . . 11  |-  ( n F x )  e. 
_V
1614, 15xpex 6553 . . . . . . . . . 10  |-  ( { suc  n }  X.  ( n F x ) )  e.  _V
1716elpw 3930 . . . . . . . . 9  |-  ( ( { suc  n }  X.  ( n F x ) )  e.  ~P ( om  X.  A )  <-> 
( { suc  n }  X.  ( n F x ) )  C_  ( om  X.  A ) )
1813, 17sylibr 215 . . . . . . . 8  |-  ( ( n  e.  om  /\  ( n F x )  e.  ( ~P A  \  { (/) } ) )  ->  ( { suc  n }  X.  ( n F x ) )  e.  ~P ( om  X.  A ) )
194, 5, 18syl2anc 665 . . . . . . 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 3531 . . . . . . . 8  |-  ( ( n F x )  e.  ( ~P A  \  { (/) } )  ->  -.  ( n F x )  e.  { (/) } )
2115elsnc 3965 . . . . . . . . . . 11  |-  ( ( n F x )  e.  { (/) }  <->  ( n F x )  =  (/) )
2221necon3bbii 2648 . . . . . . . . . 10  |-  ( -.  ( n F x )  e.  { (/) }  <-> 
( n F x )  =/=  (/) )
23 vex 3025 . . . . . . . . . . . . 13  |-  n  e. 
_V
2423sucex 6596 . . . . . . . . . . . 12  |-  suc  n  e.  _V
2524snnz 4061 . . . . . . . . . . 11  |-  { suc  n }  =/=  (/)
26 xpnz 5218 . . . . . . . . . . . 12  |-  ( ( { suc  n }  =/=  (/)  /\  ( n F x )  =/=  (/) )  <->  ( { suc  n }  X.  (
n F x ) )  =/=  (/) )
2726biimpi 197 . . . . . . . . . . 11  |-  ( ( { suc  n }  =/=  (/)  /\  ( n F x )  =/=  (/) )  ->  ( { suc  n }  X.  ( n F x ) )  =/=  (/) )
2825, 27mpan 674 . . . . . . . . . 10  |-  ( ( n F x )  =/=  (/)  ->  ( { suc  n }  X.  (
n F x ) )  =/=  (/) )
2922, 28sylbi 198 . . . . . . . . 9  |-  ( -.  ( n F x )  e.  { (/) }  ->  ( { suc  n }  X.  (
n F x ) )  =/=  (/) )
3016elsnc 3965 . . . . . . . . . 10  |-  ( ( { suc  n }  X.  ( n F x ) )  e.  { (/)
}  <->  ( { suc  n }  X.  (
n F x ) )  =  (/) )
3130necon3bbii 2648 . . . . . . . . 9  |-  ( -.  ( { suc  n }  X.  ( n F x ) )  e. 
{ (/) }  <->  ( { suc  n }  X.  (
n F x ) )  =/=  (/) )
3229, 31sylibr 215 . . . . . . . 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.  { (/)
} )
3419, 33eldifd 3390 . . . . . 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 1208 . . . . 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 2785 . . . 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 6818 . . . 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 199 . . 3  |-  ( F : ( om  X.  A ) --> ( ~P A  \  { (/) } )  ->  G :
( om  X.  A
) --> ( ~P ( om  X.  A )  \  { (/) } ) )
40 dcomex 8828 . . . . 5  |-  om  e.  _V
4140, 9xpex 6553 . . . 4  |-  ( om 
X.  A )  e. 
_V
4241axdc3 8835 . . 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 479 . 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 6780 . . . . . . . . 9  |-  ( h : om --> ( om 
X.  A )  -> 
( 2nd  o.  h
) : om --> A )
45443ad2ant1 1026 . . . . . . . 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 467 . . . . . . 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 6706 . . . . . . . 8  |-  ( ( ( 2nd  o.  h
) : om --> A  /\  om  e.  _V  /\  A  e.  _V )  ->  ( 2nd  o.  h )  e. 
_V )
4840, 9, 47mp3an23 1352 . . . . . . 7  |-  ( ( 2nd  o.  h ) : om --> A  -> 
( 2nd  o.  h
)  e.  _V )
4946, 48syl 17 . . . . . 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 5902 . . . . . . . . . . 11  |-  ( ( h : om --> ( om 
X.  A )  /\  (/) 
e.  om )  ->  (
( 2nd  o.  h
) `  (/) )  =  ( 2nd `  (
h `  (/) ) ) )
511, 50mpan2 675 . . . . . . . . . 10  |-  ( h : om --> ( om 
X.  A )  -> 
( ( 2nd  o.  h ) `  (/) )  =  ( 2nd `  (
h `  (/) ) ) )
52513ad2ant1 1026 . . . . . . . . 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 5825 . . . . . . . . . 10  |-  ( ( h `  (/) )  = 
<. (/) ,  C >.  -> 
( 2nd `  (
h `  (/) ) )  =  ( 2nd `  <. (/)
,  C >. )
)
54533ad2ant2 1027 . . . . . . . . 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 2462 . . . . . . . 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 6764 . . . . . . . . 9  |-  ( (
(/)  e.  om  /\  C  e.  A )  ->  ( 2nd `  <. (/) ,  C >. )  =  C )
571, 56mpan 674 . . . . . . . 8  |-  ( C  e.  A  ->  ( 2nd `  <. (/) ,  C >. )  =  C )
5855, 57sylan9eqr 2484 . . . . . . 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 1755 . . . . . . . . 9  |-  F/ k  C  e.  A
60 nfv 1755 . . . . . . . . . 10  |-  F/ k  h : om --> ( om 
X.  A )
61 nfv 1755 . . . . . . . . . 10  |-  F/ k ( h `  (/) )  = 
<. (/) ,  C >.
62 nfra1 2746 . . . . . . . . . 10  |-  F/ k A. k  e.  om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) )
6360, 61, 62nf3an 1990 . . . . . . . . 9  |-  F/ k ( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )
6459, 63nfan 1988 . . . . . . . 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 5825 . . . . . . . . . . . . . . . . 17  |-  ( m  =  (/)  ->  ( h `
 m )  =  ( h `  (/) ) )
66 opeq1 4130 . . . . . . . . . . . . . . . . 17  |-  ( m  =  (/)  ->  <. m ,  z >.  =  <. (/)
,  z >. )
6765, 66eqeq12d 2443 . . . . . . . . . . . . . . . 16  |-  ( m  =  (/)  ->  ( ( h `  m )  =  <. m ,  z
>. 
<->  ( h `  (/) )  = 
<. (/) ,  z >.
) )
6867exbidv 1762 . . . . . . . . . . . . . . 15  |-  ( m  =  (/)  ->  ( E. z ( h `  m )  =  <. m ,  z >.  <->  E. z
( h `  (/) )  = 
<. (/) ,  z >.
) )
69 fveq2 5825 . . . . . . . . . . . . . . . . 17  |-  ( m  =  i  ->  (
h `  m )  =  ( h `  i ) )
70 opeq1 4130 . . . . . . . . . . . . . . . . 17  |-  ( m  =  i  ->  <. m ,  z >.  =  <. i ,  z >. )
7169, 70eqeq12d 2443 . . . . . . . . . . . . . . . 16  |-  ( m  =  i  ->  (
( h `  m
)  =  <. m ,  z >.  <->  ( h `  i )  =  <. i ,  z >. )
)
7271exbidv 1762 . . . . . . . . . . . . . . 15  |-  ( m  =  i  ->  ( E. z ( h `  m )  =  <. m ,  z >.  <->  E. z
( h `  i
)  =  <. i ,  z >. )
)
73 fveq2 5825 . . . . . . . . . . . . . . . . 17  |-  ( m  =  suc  i  -> 
( h `  m
)  =  ( h `
 suc  i )
)
74 opeq1 4130 . . . . . . . . . . . . . . . . 17  |-  ( m  =  suc  i  ->  <. m ,  z >.  =  <. suc  i , 
z >. )
7573, 74eqeq12d 2443 . . . . . . . . . . . . . . . 16  |-  ( m  =  suc  i  -> 
( ( h `  m )  =  <. m ,  z >.  <->  ( h `  suc  i )  = 
<. suc  i ,  z
>. ) )
7675exbidv 1762 . . . . . . . . . . . . . . 15  |-  ( m  =  suc  i  -> 
( E. z ( h `  m )  =  <. m ,  z
>. 
<->  E. z ( h `
 suc  i )  =  <. suc  i , 
z >. ) )
77 opeq2 4131 . . . . . . . . . . . . . . . . . . 19  |-  ( z  =  C  ->  <. (/) ,  z
>.  =  <. (/) ,  C >. )
7877eqeq2d 2438 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  C  ->  (
( h `  (/) )  = 
<. (/) ,  z >.  <->  ( h `  (/) )  = 
<. (/) ,  C >. ) )
7978spcegv 3110 . . . . . . . . . . . . . . . . 17  |-  ( C  e.  A  ->  (
( h `  (/) )  = 
<. (/) ,  C >.  ->  E. z ( h `  (/) )  =  <. (/) ,  z
>. ) )
8079imp 430 . . . . . . . . . . . . . . . 16  |-  ( ( C  e.  A  /\  ( h `  (/) )  = 
<. (/) ,  C >. )  ->  E. z ( h `
 (/) )  =  <. (/)
,  z >. )
81803ad2antr2 1171 . . . . . . . . . . . . . . 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 5825 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( h `  i )  =  <. i ,  z
>.  ->  ( G `  ( h `  i
) )  =  ( G `  <. i ,  z >. )
)
83 df-ov 6252 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( i G z )  =  ( G `  <. i ,  z >. )
8482, 83syl6eqr 2480 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( h `  i )  =  <. i ,  z
>.  ->  ( G `  ( h `  i
) )  =  ( i G z ) )
8584adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( h : om --> ( om  X.  A )  /\  i  e.  om )  /\  ( h `  i )  =  <. i ,  z >. )  ->  ( G `  (
h `  i )
)  =  ( i G z ) )
86 simplr 760 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( h : om --> ( om  X.  A )  /\  i  e.  om )  /\  ( h `  i )  =  <. i ,  z >. )  ->  i  e.  om )
87 ffvelrn 5979 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( h : om --> ( om 
X.  A )  /\  i  e.  om )  ->  ( h `  i
)  e.  ( om 
X.  A ) )
88 eleq1 2494 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( h `  i )  =  <. i ,  z
>.  ->  ( ( h `
 i )  e.  ( om  X.  A
)  <->  <. i ,  z
>.  e.  ( om  X.  A ) ) )
89 opelxp2 4830 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( <.
i ,  z >.  e.  ( om  X.  A
)  ->  z  e.  A )
9088, 89syl6bi 231 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( h `  i )  =  <. i ,  z
>.  ->  ( ( h `
 i )  e.  ( om  X.  A
)  ->  z  e.  A ) )
9187, 90mpan9 471 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( h : om --> ( om  X.  A )  /\  i  e.  om )  /\  ( h `  i )  =  <. i ,  z >. )  ->  z  e.  A )
92 suceq 5450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( n  =  i  ->  suc  n  =  suc  i )
9392sneqd 3953 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( n  =  i  ->  { suc  n }  =  { suc  i } )
94 oveq1 6256 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( n  =  i  ->  (
n F x )  =  ( i F x ) )
9593, 94xpeq12d 4821 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( n  =  i  ->  ( { suc  n }  X.  ( n F x ) )  =  ( { suc  i }  X.  ( i F x ) ) )
96 oveq2 6257 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  =  z  ->  (
i F x )  =  ( i F z ) )
9796xpeq2d 4820 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  =  z  ->  ( { suc  i }  X.  ( i F x ) )  =  ( { suc  i }  X.  ( i F z ) ) )
98 snex 4605 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  { suc  i }  e.  _V
99 ovex 6277 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( i F z )  e. 
_V
10098, 99xpex 6553 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( { suc  i }  X.  ( i F z ) )  e.  _V
10195, 97, 37, 100ovmpt2 6390 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( i  e.  om  /\  z  e.  A )  ->  ( i G z )  =  ( { suc  i }  X.  ( i F z ) ) )
10286, 91, 101syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( h : om --> ( om  X.  A )  /\  i  e.  om )  /\  ( h `  i )  =  <. i ,  z >. )  ->  ( i G z )  =  ( { suc  i }  X.  ( i F z ) ) )
10385, 102eqtrd 2462 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( h : om --> ( om  X.  A )  /\  i  e.  om )  /\  ( h `  i )  =  <. i ,  z >. )  ->  ( G `  (
h `  i )
)  =  ( { suc  i }  X.  ( i F z ) ) )
104 suceq 5450 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( k  =  i  ->  suc  k  =  suc  i )
105104fveq2d 5829 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  =  i  ->  (
h `  suc  k )  =  ( h `  suc  i ) )
106 fveq2 5825 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( k  =  i  ->  (
h `  k )  =  ( h `  i ) )
107106fveq2d 5829 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  =  i  ->  ( G `  ( h `  k ) )  =  ( G `  (
h `  i )
) )
108105, 107eleq12d 2500 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( k  =  i  ->  (
( h `  suc  k )  e.  ( G `  ( h `
 k ) )  <-> 
( h `  suc  i )  e.  ( G `  ( h `
 i ) ) ) )
109108rspcv 3121 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( i  e.  om  ->  ( A. k  e.  om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) )  ->  ( h `  suc  i )  e.  ( G `  ( h `
 i ) ) ) )
110109ad2antlr 731 . . . . . . . . . . . . . . . . . . . . . . . 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 2495 . . . . . . . . . . . . . . . . . . . . . . . . 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 4813 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3955 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( s  e.  { suc  i } 
<->  s  =  suc  i
)
114 opeq1 4130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( s  =  suc  i  ->  <. s ,  t >.  =  <. suc  i , 
t >. )
115113, 114sylbi 198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( s  e.  { suc  i }  ->  <. s ,  t
>.  =  <. suc  i ,  t >. )
116115eqeq2d 2438 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( s  e.  { suc  i }  ->  ( ( h `
 suc  i )  =  <. s ,  t
>. 
<->  ( h `  suc  i )  =  <. suc  i ,  t >.
) )
117116biimpac 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( h `  suc  i )  =  <. s ,  t >.  /\  s  e.  { suc  i } )  ->  ( h `  suc  i )  = 
<. suc  i ,  t
>. )
118117adantrr 721 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( h `  suc  i )  =  <. s ,  t >.  /\  (
s  e.  { suc  i }  /\  t  e.  ( i F z ) ) )  -> 
( h `  suc  i )  =  <. suc  i ,  t >.
)
119118eximi 1701 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1770 . . . . . . . . . . . . . . . . . . . . . . . . . 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 198 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( h `  suc  i
)  e.  ( { suc  i }  X.  ( i F z ) )  ->  E. t
( h `  suc  i )  =  <. suc  i ,  t >.
)
122111, 121syl6bi 231 . . . . . . . . . . . . . . . . . . . . . . . 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 58 . . . . . . . . . . . . . . . . . . . . . . 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 436 . . . . . . . . . . . . . . . . . . . . . 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 1770 . . . . . . . . . . . . . . . . . . . . 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 84 . . . . . . . . . . . . . . . . . . . 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 4131 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( t  =  z  ->  <. suc  i ,  t >.  =  <. suc  i ,  z >.
)
128127eqeq2d 2438 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  =  z  ->  (
( h `  suc  i )  =  <. suc  i ,  t >.  <->  ( h `  suc  i
)  =  <. suc  i ,  z >. )
)
129128cbvexv 2089 . . . . . . . . . . . . . . . . . . . 20  |-  ( E. t ( h `  suc  i )  =  <. suc  i ,  t >.  <->  E. z ( h `  suc  i )  =  <. suc  i ,  z >.
)
130126, 129syl8ib 234 . . . . . . . . . . . . . . . . . . 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 441 . . . . . . . . . . . . . . . . . 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 1024 . . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . 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 32 . . . . . . . . . . . . . . 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 6679 . . . . . . . . . . . . . 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 32 . . . . . . . . . . . . 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 2777 . . . . . . . . . . . 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 5825 . . . . . . . . . . . . . . 15  |-  ( m  =  k  ->  (
h `  m )  =  ( h `  k ) )
139 opeq1 4130 . . . . . . . . . . . . . . 15  |-  ( m  =  k  ->  <. m ,  z >.  =  <. k ,  z >. )
140138, 139eqeq12d 2443 . . . . . . . . . . . . . 14  |-  ( m  =  k  ->  (
( h `  m
)  =  <. m ,  z >.  <->  ( h `  k )  =  <. k ,  z >. )
)
141140exbidv 1762 . . . . . . . . . . . . 13  |-  ( m  =  k  ->  ( E. z ( h `  m )  =  <. m ,  z >.  <->  E. z
( h `  k
)  =  <. k ,  z >. )
)
142141rspccv 3122 . . . . . . . . . . . 12  |-  ( A. m  e.  om  E. z
( h `  m
)  =  <. m ,  z >.  ->  (
k  e.  om  ->  E. z ( h `  k )  =  <. k ,  z >. )
)
143137, 142syl 17 . . . . . . . . . . 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 1202 . . . . . . . . . 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 1038 . . . . . . . . . 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 1007 . . . . . . . . . 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 rspa 2732 . . . . . . . . . . . 12  |-  ( ( A. k  e.  om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) )  /\  k  e.  om )  ->  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )
1481473ad2antl3 1169 . . . . . . . . . . 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
) ) )
1491483adant1 1023 . . . . . . . . . 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
) ) )
150 simpl 458 . . . . . . . . . . . . . . . . 17  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( h `  k )  =  <. k ,  z >. )
151150fveq2d 5829 . . . . . . . . . . . . . . . 16  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( G `  ( h `  k
) )  =  ( G `  <. k ,  z >. )
)
152 simprr 764 . . . . . . . . . . . . . . . . 17  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  k  e.  om )
153 ffvelrn 5979 . . . . . . . . . . . . . . . . . . 19  |-  ( ( h : om --> ( om 
X.  A )  /\  k  e.  om )  ->  ( h `  k
)  e.  ( om 
X.  A ) )
154 eleq1 2494 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( h `  k )  =  <. k ,  z
>.  ->  ( ( h `
 k )  e.  ( om  X.  A
)  <->  <. k ,  z
>.  e.  ( om  X.  A ) ) )
155 opelxp2 4830 . . . . . . . . . . . . . . . . . . . 20  |-  ( <.
k ,  z >.  e.  ( om  X.  A
)  ->  z  e.  A )
156154, 155syl6bi 231 . . . . . . . . . . . . . . . . . . 19  |-  ( ( h `  k )  =  <. k ,  z
>.  ->  ( ( h `
 k )  e.  ( om  X.  A
)  ->  z  e.  A ) )
157153, 156syl5 33 . . . . . . . . . . . . . . . . . 18  |-  ( ( h `  k )  =  <. k ,  z
>.  ->  ( ( h : om --> ( om 
X.  A )  /\  k  e.  om )  ->  z  e.  A ) )
158157imp 430 . . . . . . . . . . . . . . . . 17  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  z  e.  A )
159 df-ov 6252 . . . . . . . . . . . . . . . . . 18  |-  ( k G z )  =  ( G `  <. k ,  z >. )
160 suceq 5450 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  k  ->  suc  n  =  suc  k )
161160sneqd 3953 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  k  ->  { suc  n }  =  { suc  k } )
162 oveq1 6256 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  k  ->  (
n F x )  =  ( k F x ) )
163161, 162xpeq12d 4821 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  k  ->  ( { suc  n }  X.  ( n F x ) )  =  ( { suc  k }  X.  ( k F x ) ) )
164 oveq2 6257 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  z  ->  (
k F x )  =  ( k F z ) )
165164xpeq2d 4820 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  z  ->  ( { suc  k }  X.  ( k F x ) )  =  ( { suc  k }  X.  ( k F z ) ) )
166 snex 4605 . . . . . . . . . . . . . . . . . . . 20  |-  { suc  k }  e.  _V
167 ovex 6277 . . . . . . . . . . . . . . . . . . . 20  |-  ( k F z )  e. 
_V
168166, 167xpex 6553 . . . . . . . . . . . . . . . . . . 19  |-  ( { suc  k }  X.  ( k F z ) )  e.  _V
169163, 165, 37, 168ovmpt2 6390 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  om  /\  z  e.  A )  ->  ( k G z )  =  ( { suc  k }  X.  ( k F z ) ) )
170159, 169syl5eqr 2476 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  om  /\  z  e.  A )  ->  ( G `  <. k ,  z >. )  =  ( { suc  k }  X.  (
k F z ) ) )
171152, 158, 170syl2anc 665 . . . . . . . . . . . . . . . 16  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( G `  <. k ,  z
>. )  =  ( { suc  k }  X.  ( k F z ) ) )
172151, 171eqtrd 2462 . . . . . . . . . . . . . . 15  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( G `  ( h `  k
) )  =  ( { suc  k }  X.  ( k F z ) ) )
173172eleq2d 2491 . . . . . . . . . . . . . 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 ) ) ) )
174 elxp 4813 . . . . . . . . . . . . . . . . 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 ) ) ) )
175 peano2 6671 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  e.  om  ->  suc  k  e.  om )
176 fvco3 5902 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( h : om --> ( om 
X.  A )  /\  suc  k  e.  om )  ->  ( ( 2nd 
o.  h ) `  suc  k )  =  ( 2nd `  ( h `
 suc  k )
) )
177175, 176sylan2 476 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( h : om --> ( om 
X.  A )  /\  k  e.  om )  ->  ( ( 2nd  o.  h ) `  suc  k )  =  ( 2nd `  ( h `
 suc  k )
) )
178177adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
179 simpll 758 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( h `  suc  k )  = 
<. s ,  t >.
)
180179fveq2d 5829 . . . . . . . . . . . . . . . . . . . . . . . . 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 >. )
)
181178, 180eqtrd 2462 . . . . . . . . . . . . . . . . . . . . . . . 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 >. )
)
182 vex 3025 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  s  e. 
_V
183 vex 3025 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  t  e. 
_V
184182, 183op2nd 6760 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 2nd `  <. s ,  t
>. )  =  t
185181, 184syl6eq 2478 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( ( 2nd  o.  h ) `  suc  k )  =  t )
186 fvco3 5902 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( h : om --> ( om 
X.  A )  /\  k  e.  om )  ->  ( ( 2nd  o.  h ) `  k
)  =  ( 2nd `  ( h `  k
) ) )
187186adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
188 simplr 760 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( h `  k )  =  <. k ,  z >. )
189188fveq2d 5829 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( 2nd `  ( h `  k
) )  =  ( 2nd `  <. k ,  z >. )
)
190187, 189eqtrd 2462 . . . . . . . . . . . . . . . . . . . . . . . . 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 >. )
)
191 vex 3025 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  k  e. 
_V
192 vex 3025 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  z  e. 
_V
193191, 192op2nd 6760 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 2nd `  <. k ,  z
>. )  =  z
194190, 193syl6eq 2478 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( ( 2nd  o.  h ) `  k )  =  z )
195194oveq2d 6265 . . . . . . . . . . . . . . . . . . . . . . 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 ) )
196185, 195eleq12d 2500 . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
197196biimprcd 228 . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
198197exp4c 611 . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
199198adantl 467 . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
200199impcom 431 . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
201200exlimivv 1771 . . . . . . . . . . . . . . . . 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 ) ) ) ) )
202174, 201sylbi 198 . . . . . . . . . . . . . . . 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 ) ) ) ) )
203202com3l 84 . . . . . . . . . . . . . . 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 ) ) ) ) )
204203imp 430 . . . . . . . . . . . . . 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 ) ) ) )
205173, 204sylbid 218 . . . . . . . . . . . . 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
) ) ) )
206205ex 435 . . . . . . . . . . . 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 ) ) ) ) )
207206exlimiv 1770 . . . . . . . . . . 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 ) ) ) ) )
2082073imp 1199 . . . . . . . . . 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 ) ) )
209144, 145, 146, 149, 208syl121anc 1269 . . . . . . . . 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
) ) )
2102093expia 1207 . . . . . . . 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
) ) ) )
21164, 210ralrimi 2765 . . . . . . 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 ) ) )
21246, 58, 2113jca 1185 . . . . . 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 ) ) ) )
213 feq1 5671 . . . . . . . 8  |-  ( g  =  ( 2nd  o.  h )  ->  (
g : om --> A  <->  ( 2nd  o.  h ) : om --> A ) )
214 fveq1 5824 . . . . . . . . 9  |-  ( g  =  ( 2nd  o.  h )  ->  (
g `  (/) )  =  ( ( 2nd  o.  h ) `  (/) ) )
215214eqeq1d 2430 . . . . . . . 8  |-  ( g  =  ( 2nd  o.  h )  ->  (
( g `  (/) )  =  C  <->  ( ( 2nd 
o.  h ) `  (/) )  =  C ) )
216 fveq1 5824 . . . . . . . . . 10  |-  ( g  =  ( 2nd  o.  h )  ->  (
g `  suc  k )  =  ( ( 2nd 
o.  h ) `  suc  k ) )
217 fveq1 5824 . . . . . . . . . . 11  |-  ( g  =  ( 2nd  o.  h )  ->  (
g `  k )  =  ( ( 2nd 
o.  h ) `  k ) )
218217oveq2d 6265 . . . . . . . . . 10  |-  ( g  =  ( 2nd  o.  h )  ->  (
k F ( g `
 k ) )  =  ( k F ( ( 2nd  o.  h ) `  k
) ) )
219216, 218eleq12d 2500 . . . . . . . . 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 ) ) ) )
220219ralbidv 2804 . . . . . . . 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 ) ) ) )
221213, 215, 2203anbi123d 1335 . . . . . . 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 ) ) ) ) )
222221spcegv 3110 . . . . . 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 ) ) ) ) )
22349, 212, 222sylc 62 . . . . 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
) ) ) )
224223ex 435 . . . 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
) ) ) ) )
225224exlimdv 1772 . . 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
) ) ) ) )
226225adantr 466 . 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
) ) ) ) )
22743, 226mpd 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 setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 370    /\ w3a 982    = wceq 1437   E.wex 1657    e. wcel 1872    =/= wne 2599   A.wral 2714   _Vcvv 3022    \ cdif 3376    C_ wss 3379   (/)c0 3704   ~Pcpw 3924   {csn 3941   <.cop 3947    X. cxp 4794    o. ccom 4800   suc csuc 5387   -->wf 5540   ` cfv 5544  (class class class)co 6249    |-> cmpt2 6251   omcom 6650   2ndc2nd 6750
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-sep 4489  ax-nul 4498  ax-pow 4545  ax-pr 4603  ax-un 6541  ax-dc 8827
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-reu 2721  df-rab 2723  df-v 3024  df-sbc 3243  df-csb 3339  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-pss 3395  df-nul 3705  df-if 3855  df-pw 3926  df-sn 3942  df-pr 3944  df-tp 3946  df-op 3948  df-uni 4163  df-iun 4244  df-br 4367  df-opab 4426  df-mpt 4427  df-tr 4462  df-eprel 4707  df-id 4711  df-po 4717  df-so 4718  df-fr 4755  df-we 4757  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-ord 5388  df-on 5389  df-lim 5390  df-suc 5391  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-f1 5549  df-fo 5550  df-f1o 5551  df-fv 5552  df-ov 6252  df-oprab 6253  df-mpt2 6254  df-om 6651  df-1st 6751  df-2nd 6752  df-1o 7137
This theorem is referenced by:  axdc4  8837
  Copyright terms: Public domain W3C validator