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

Theorem axdc4lem 8833
Description: Lemma for axdc4 8834. (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 6700 . . . 4  |-  (/)  e.  om
2 opelxpi 5017 . . . 4  |-  ( (
(/)  e.  om  /\  C  e.  A )  ->  <. (/) ,  C >.  e.  ( om  X.  A ) )
31, 2mpan 670 . . 3  |-  ( C  e.  A  ->  <. (/) ,  C >.  e.  ( om  X.  A ) )
4 simp2 996 . . . . . . . 8  |-  ( ( F : ( om 
X.  A ) --> ( ~P A  \  { (/)
} )  /\  n  e.  om  /\  x  e.  A )  ->  n  e.  om )
5 fovrn 6426 . . . . . . . 8  |-  ( ( F : ( om 
X.  A ) --> ( ~P A  \  { (/)
} )  /\  n  e.  om  /\  x  e.  A )  ->  (
n F x )  e.  ( ~P A  \  { (/) } ) )
6 peano2 6701 . . . . . . . . . . 11  |-  ( n  e.  om  ->  suc  n  e.  om )
76snssd 4156 . . . . . . . . . 10  |-  ( n  e.  om  ->  { suc  n }  C_  om )
8 eldifi 3608 . . . . . . . . . 10  |-  ( ( n F x )  e.  ( ~P A  \  { (/) } )  -> 
( n F x )  e.  ~P A
)
9 axdc4lem.1 . . . . . . . . . . . 12  |-  A  e. 
_V
109elpw2 4597 . . . . . . . . . . 11  |-  ( ( n F x )  e.  ~P A  <->  ( n F x )  C_  A )
11 xpss12 5094 . . . . . . . . . . 11  |-  ( ( { suc  n }  C_ 
om  /\  ( n F x )  C_  A )  ->  ( { suc  n }  X.  ( n F x ) )  C_  ( om  X.  A ) )
1210, 11sylan2b 475 . . . . . . . . . 10  |-  ( ( { suc  n }  C_ 
om  /\  ( n F x )  e. 
~P A )  -> 
( { suc  n }  X.  ( n F x ) )  C_  ( om  X.  A ) )
137, 8, 12syl2an 477 . . . . . . . . 9  |-  ( ( n  e.  om  /\  ( n F x )  e.  ( ~P A  \  { (/) } ) )  ->  ( { suc  n }  X.  ( n F x ) )  C_  ( om  X.  A ) )
14 snex 4674 . . . . . . . . . . 11  |-  { suc  n }  e.  _V
15 ovex 6305 . . . . . . . . . . 11  |-  ( n F x )  e. 
_V
1614, 15xpex 6585 . . . . . . . . . 10  |-  ( { suc  n }  X.  ( n F x ) )  e.  _V
1716elpw 3999 . . . . . . . . 9  |-  ( ( { suc  n }  X.  ( n F x ) )  e.  ~P ( om  X.  A )  <-> 
( { suc  n }  X.  ( n F x ) )  C_  ( om  X.  A ) )
1813, 17sylibr 212 . . . . . . . 8  |-  ( ( n  e.  om  /\  ( n F x )  e.  ( ~P A  \  { (/) } ) )  ->  ( { suc  n }  X.  ( n F x ) )  e.  ~P ( om  X.  A ) )
194, 5, 18syl2anc 661 . . . . . . 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 3609 . . . . . . . 8  |-  ( ( n F x )  e.  ( ~P A  \  { (/) } )  ->  -.  ( n F x )  e.  { (/) } )
2115elsnc 4034 . . . . . . . . . . 11  |-  ( ( n F x )  e.  { (/) }  <->  ( n F x )  =  (/) )
2221necon3bbii 2702 . . . . . . . . . 10  |-  ( -.  ( n F x )  e.  { (/) }  <-> 
( n F x )  =/=  (/) )
23 vex 3096 . . . . . . . . . . . . 13  |-  n  e. 
_V
2423sucex 6627 . . . . . . . . . . . 12  |-  suc  n  e.  _V
2524snnz 4129 . . . . . . . . . . 11  |-  { suc  n }  =/=  (/)
26 xpnz 5412 . . . . . . . . . . . 12  |-  ( ( { suc  n }  =/=  (/)  /\  ( n F x )  =/=  (/) )  <->  ( { suc  n }  X.  (
n F x ) )  =/=  (/) )
2726biimpi 194 . . . . . . . . . . 11  |-  ( ( { suc  n }  =/=  (/)  /\  ( n F x )  =/=  (/) )  ->  ( { suc  n }  X.  ( n F x ) )  =/=  (/) )
2825, 27mpan 670 . . . . . . . . . 10  |-  ( ( n F x )  =/=  (/)  ->  ( { suc  n }  X.  (
n F x ) )  =/=  (/) )
2922, 28sylbi 195 . . . . . . . . 9  |-  ( -.  ( n F x )  e.  { (/) }  ->  ( { suc  n }  X.  (
n F x ) )  =/=  (/) )
3016elsnc 4034 . . . . . . . . . 10  |-  ( ( { suc  n }  X.  ( n F x ) )  e.  { (/)
}  <->  ( { suc  n }  X.  (
n F x ) )  =  (/) )
3130necon3bbii 2702 . . . . . . . . 9  |-  ( -.  ( { suc  n }  X.  ( n F x ) )  e. 
{ (/) }  <->  ( { suc  n }  X.  (
n F x ) )  =/=  (/) )
3229, 31sylibr 212 . . . . . . . 8  |-  ( -.  ( n F x )  e.  { (/) }  ->  -.  ( { suc  n }  X.  (
n F x ) )  e.  { (/) } )
335, 20, 323syl 20 . . . . . . 7  |-  ( ( F : ( om 
X.  A ) --> ( ~P A  \  { (/)
} )  /\  n  e.  om  /\  x  e.  A )  ->  -.  ( { suc  n }  X.  ( n F x ) )  e.  { (/)
} )
3419, 33eldifd 3469 . . . . . 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 1198 . . . . 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 2861 . . . 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 6848 . . . 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 196 . . 3  |-  ( F : ( om  X.  A ) --> ( ~P A  \  { (/) } )  ->  G :
( om  X.  A
) --> ( ~P ( om  X.  A )  \  { (/) } ) )
40 dcomex 8825 . . . . 5  |-  om  e.  _V
4140, 9xpex 6585 . . . 4  |-  ( om 
X.  A )  e. 
_V
4241axdc3 8832 . . 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 477 . 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 6810 . . . . . . . . 9  |-  ( h : om --> ( om 
X.  A )  -> 
( 2nd  o.  h
) : om --> A )
45443ad2ant1 1016 . . . . . . . 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 466 . . . . . . 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 6736 . . . . . . . 8  |-  ( ( ( 2nd  o.  h
) : om --> A  /\  om  e.  _V  /\  A  e.  _V )  ->  ( 2nd  o.  h )  e. 
_V )
4840, 9, 47mp3an23 1315 . . . . . . 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 5931 . . . . . . . . . . 11  |-  ( ( h : om --> ( om 
X.  A )  /\  (/) 
e.  om )  ->  (
( 2nd  o.  h
) `  (/) )  =  ( 2nd `  (
h `  (/) ) ) )
511, 50mpan2 671 . . . . . . . . . 10  |-  ( h : om --> ( om 
X.  A )  -> 
( ( 2nd  o.  h ) `  (/) )  =  ( 2nd `  (
h `  (/) ) ) )
52513ad2ant1 1016 . . . . . . . . 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 5852 . . . . . . . . . 10  |-  ( ( h `  (/) )  = 
<. (/) ,  C >.  -> 
( 2nd `  (
h `  (/) ) )  =  ( 2nd `  <. (/)
,  C >. )
)
54533ad2ant2 1017 . . . . . . . . 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 2482 . . . . . . . 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 6794 . . . . . . . . 9  |-  ( (
(/)  e.  om  /\  C  e.  A )  ->  ( 2nd `  <. (/) ,  C >. )  =  C )
571, 56mpan 670 . . . . . . . 8  |-  ( C  e.  A  ->  ( 2nd `  <. (/) ,  C >. )  =  C )
5855, 57sylan9eqr 2504 . . . . . . 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 1692 . . . . . . . . 9  |-  F/ k  C  e.  A
60 nfv 1692 . . . . . . . . . 10  |-  F/ k  h : om --> ( om 
X.  A )
61 nfv 1692 . . . . . . . . . 10  |-  F/ k ( h `  (/) )  = 
<. (/) ,  C >.
62 nfra1 2822 . . . . . . . . . 10  |-  F/ k A. k  e.  om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) )
6360, 61, 62nf3an 1914 . . . . . . . . 9  |-  F/ k ( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )
6459, 63nfan 1912 . . . . . . . 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 5852 . . . . . . . . . . . . . . . . 17  |-  ( m  =  (/)  ->  ( h `
 m )  =  ( h `  (/) ) )
66 opeq1 4198 . . . . . . . . . . . . . . . . 17  |-  ( m  =  (/)  ->  <. m ,  z >.  =  <. (/)
,  z >. )
6765, 66eqeq12d 2463 . . . . . . . . . . . . . . . 16  |-  ( m  =  (/)  ->  ( ( h `  m )  =  <. m ,  z
>. 
<->  ( h `  (/) )  = 
<. (/) ,  z >.
) )
6867exbidv 1699 . . . . . . . . . . . . . . 15  |-  ( m  =  (/)  ->  ( E. z ( h `  m )  =  <. m ,  z >.  <->  E. z
( h `  (/) )  = 
<. (/) ,  z >.
) )
69 fveq2 5852 . . . . . . . . . . . . . . . . 17  |-  ( m  =  i  ->  (
h `  m )  =  ( h `  i ) )
70 opeq1 4198 . . . . . . . . . . . . . . . . 17  |-  ( m  =  i  ->  <. m ,  z >.  =  <. i ,  z >. )
7169, 70eqeq12d 2463 . . . . . . . . . . . . . . . 16  |-  ( m  =  i  ->  (
( h `  m
)  =  <. m ,  z >.  <->  ( h `  i )  =  <. i ,  z >. )
)
7271exbidv 1699 . . . . . . . . . . . . . . 15  |-  ( m  =  i  ->  ( E. z ( h `  m )  =  <. m ,  z >.  <->  E. z
( h `  i
)  =  <. i ,  z >. )
)
73 fveq2 5852 . . . . . . . . . . . . . . . . 17  |-  ( m  =  suc  i  -> 
( h `  m
)  =  ( h `
 suc  i )
)
74 opeq1 4198 . . . . . . . . . . . . . . . . 17  |-  ( m  =  suc  i  ->  <. m ,  z >.  =  <. suc  i , 
z >. )
7573, 74eqeq12d 2463 . . . . . . . . . . . . . . . 16  |-  ( m  =  suc  i  -> 
( ( h `  m )  =  <. m ,  z >.  <->  ( h `  suc  i )  = 
<. suc  i ,  z
>. ) )
7675exbidv 1699 . . . . . . . . . . . . . . 15  |-  ( m  =  suc  i  -> 
( E. z ( h `  m )  =  <. m ,  z
>. 
<->  E. z ( h `
 suc  i )  =  <. suc  i , 
z >. ) )
77 opeq2 4199 . . . . . . . . . . . . . . . . . . 19  |-  ( z  =  C  ->  <. (/) ,  z
>.  =  <. (/) ,  C >. )
7877eqeq2d 2455 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  C  ->  (
( h `  (/) )  = 
<. (/) ,  z >.  <->  ( h `  (/) )  = 
<. (/) ,  C >. ) )
7978spcegv 3179 . . . . . . . . . . . . . . . . 17  |-  ( C  e.  A  ->  (
( h `  (/) )  = 
<. (/) ,  C >.  ->  E. z ( h `  (/) )  =  <. (/) ,  z
>. ) )
8079imp 429 . . . . . . . . . . . . . . . 16  |-  ( ( C  e.  A  /\  ( h `  (/) )  = 
<. (/) ,  C >. )  ->  E. z ( h `
 (/) )  =  <. (/)
,  z >. )
81803ad2antr2 1161 . . . . . . . . . . . . . . 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 5852 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( h `  i )  =  <. i ,  z
>.  ->  ( G `  ( h `  i
) )  =  ( G `  <. i ,  z >. )
)
83 df-ov 6280 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( i G z )  =  ( G `  <. i ,  z >. )
8482, 83syl6eqr 2500 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( h `  i )  =  <. i ,  z
>.  ->  ( G `  ( h `  i
) )  =  ( i G z ) )
8584adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( h : om --> ( om  X.  A )  /\  i  e.  om )  /\  ( h `  i )  =  <. i ,  z >. )  ->  ( G `  (
h `  i )
)  =  ( i G z ) )
86 simplr 754 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( h : om --> ( om  X.  A )  /\  i  e.  om )  /\  ( h `  i )  =  <. i ,  z >. )  ->  i  e.  om )
87 ffvelrn 6010 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( h : om --> ( om 
X.  A )  /\  i  e.  om )  ->  ( h `  i
)  e.  ( om 
X.  A ) )
88 eleq1 2513 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( h `  i )  =  <. i ,  z
>.  ->  ( ( h `
 i )  e.  ( om  X.  A
)  <->  <. i ,  z
>.  e.  ( om  X.  A ) ) )
89 opelxp2 5019 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( <.
i ,  z >.  e.  ( om  X.  A
)  ->  z  e.  A )
9088, 89syl6bi 228 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( h `  i )  =  <. i ,  z
>.  ->  ( ( h `
 i )  e.  ( om  X.  A
)  ->  z  e.  A ) )
9187, 90mpan9 469 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( h : om --> ( om  X.  A )  /\  i  e.  om )  /\  ( h `  i )  =  <. i ,  z >. )  ->  z  e.  A )
92 suceq 4929 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( n  =  i  ->  suc  n  =  suc  i )
9392sneqd 4022 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( n  =  i  ->  { suc  n }  =  { suc  i } )
94 oveq1 6284 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( n  =  i  ->  (
n F x )  =  ( i F x ) )
9593, 94xpeq12d 5010 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( n  =  i  ->  ( { suc  n }  X.  ( n F x ) )  =  ( { suc  i }  X.  ( i F x ) ) )
96 oveq2 6285 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  =  z  ->  (
i F x )  =  ( i F z ) )
9796xpeq2d 5009 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  =  z  ->  ( { suc  i }  X.  ( i F x ) )  =  ( { suc  i }  X.  ( i F z ) ) )
98 snex 4674 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  { suc  i }  e.  _V
99 ovex 6305 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( i F z )  e. 
_V
10098, 99xpex 6585 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( { suc  i }  X.  ( i F z ) )  e.  _V
10195, 97, 37, 100ovmpt2 6419 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( i  e.  om  /\  z  e.  A )  ->  ( i G z )  =  ( { suc  i }  X.  ( i F z ) ) )
10286, 91, 101syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( h : om --> ( om  X.  A )  /\  i  e.  om )  /\  ( h `  i )  =  <. i ,  z >. )  ->  ( i G z )  =  ( { suc  i }  X.  ( i F z ) ) )
10385, 102eqtrd 2482 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( h : om --> ( om  X.  A )  /\  i  e.  om )  /\  ( h `  i )  =  <. i ,  z >. )  ->  ( G `  (
h `  i )
)  =  ( { suc  i }  X.  ( i F z ) ) )
104 suceq 4929 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( k  =  i  ->  suc  k  =  suc  i )
105104fveq2d 5856 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  =  i  ->  (
h `  suc  k )  =  ( h `  suc  i ) )
106 fveq2 5852 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( k  =  i  ->  (
h `  k )  =  ( h `  i ) )
107106fveq2d 5856 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  =  i  ->  ( G `  ( h `  k ) )  =  ( G `  (
h `  i )
) )
108105, 107eleq12d 2523 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( k  =  i  ->  (
( h `  suc  k )  e.  ( G `  ( h `
 k ) )  <-> 
( h `  suc  i )  e.  ( G `  ( h `
 i ) ) ) )
109108rspcv 3190 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( i  e.  om  ->  ( A. k  e.  om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) )  ->  ( h `  suc  i )  e.  ( G `  ( h `
 i ) ) ) )
110109ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . 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 2514 . . . . . . . . . . . . . . . . . . . . . . . . 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 5002 . . . . . . . . . . . . . . . . . . . . . . . . . 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 4024 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( s  e.  { suc  i } 
<->  s  =  suc  i
)
114 opeq1 4198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( s  =  suc  i  ->  <. s ,  t >.  =  <. suc  i , 
t >. )
115113, 114sylbi 195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( s  e.  { suc  i }  ->  <. s ,  t
>.  =  <. suc  i ,  t >. )
116115eqeq2d 2455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( s  e.  { suc  i }  ->  ( ( h `
 suc  i )  =  <. s ,  t
>. 
<->  ( h `  suc  i )  =  <. suc  i ,  t >.
) )
117116biimpac 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( h `  suc  i )  =  <. s ,  t >.  /\  s  e.  { suc  i } )  ->  ( h `  suc  i )  = 
<. suc  i ,  t
>. )
118117adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( h `  suc  i )  =  <. s ,  t >.  /\  (
s  e.  { suc  i }  /\  t  e.  ( i F z ) ) )  -> 
( h `  suc  i )  =  <. suc  i ,  t >.
)
119118eximi 1641 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1707 . . . . . . . . . . . . . . . . . . . . . . . . . 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 195 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( h `  suc  i
)  e.  ( { suc  i }  X.  ( i F z ) )  ->  E. t
( h `  suc  i )  =  <. suc  i ,  t >.
)
122111, 121syl6bi 228 . . . . . . . . . . . . . . . . . . . . . . . 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 56 . . . . . . . . . . . . . . . . . . . . . . 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 435 . . . . . . . . . . . . . . . . . . . . . 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 1707 . . . . . . . . . . . . . . . . . . . . 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 81 . . . . . . . . . . . . . . . . . . . 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 4199 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( t  =  z  ->  <. suc  i ,  t >.  =  <. suc  i ,  z >.
)
128127eqeq2d 2455 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  =  z  ->  (
( h `  suc  i )  =  <. suc  i ,  t >.  <->  ( h `  suc  i
)  =  <. suc  i ,  z >. )
)
129128cbvexv 2008 . . . . . . . . . . . . . . . . . . . 20  |-  ( E. t ( h `  suc  i )  =  <. suc  i ,  t >.  <->  E. z ( h `  suc  i )  =  <. suc  i ,  z >.
)
130126, 129syl8ib 231 . . . . . . . . . . . . . . . . . . 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 440 . . . . . . . . . . . . . . . . . 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 1014 . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . 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 31 . . . . . . . . . . . . . . 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 6709 . . . . . . . . . . . . . 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 31 . . . . . . . . . . . . 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 2853 . . . . . . . . . . . 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 5852 . . . . . . . . . . . . . . 15  |-  ( m  =  k  ->  (
h `  m )  =  ( h `  k ) )
139 opeq1 4198 . . . . . . . . . . . . . . 15  |-  ( m  =  k  ->  <. m ,  z >.  =  <. k ,  z >. )
140138, 139eqeq12d 2463 . . . . . . . . . . . . . 14  |-  ( m  =  k  ->  (
( h `  m
)  =  <. m ,  z >.  <->  ( h `  k )  =  <. k ,  z >. )
)
141140exbidv 1699 . . . . . . . . . . . . 13  |-  ( m  =  k  ->  ( E. z ( h `  m )  =  <. m ,  z >.  <->  E. z
( h `  k
)  =  <. k ,  z >. )
)
142141rspccv 3191 . . . . . . . . . . . 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 1192 . . . . . . . . . 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 1028 . . . . . . . . . 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 997 . . . . . . . . . 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 2808 . . . . . . . . . . . 12  |-  ( ( A. k  e.  om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) )  /\  k  e.  om )  ->  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )
1481473ad2antl3 1159 . . . . . . . . . . 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 1013 . . . . . . . . . 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 457 . . . . . . . . . . . . . . . . 17  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( h `  k )  =  <. k ,  z >. )
151150fveq2d 5856 . . . . . . . . . . . . . . . 16  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( G `  ( h `  k
) )  =  ( G `  <. k ,  z >. )
)
152 simprr 756 . . . . . . . . . . . . . . . . 17  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  k  e.  om )
153 ffvelrn 6010 . . . . . . . . . . . . . . . . . . 19  |-  ( ( h : om --> ( om 
X.  A )  /\  k  e.  om )  ->  ( h `  k
)  e.  ( om 
X.  A ) )
154 eleq1 2513 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( h `  k )  =  <. k ,  z
>.  ->  ( ( h `
 k )  e.  ( om  X.  A
)  <->  <. k ,  z
>.  e.  ( om  X.  A ) ) )
155 opelxp2 5019 . . . . . . . . . . . . . . . . . . . 20  |-  ( <.
k ,  z >.  e.  ( om  X.  A
)  ->  z  e.  A )
156154, 155syl6bi 228 . . . . . . . . . . . . . . . . . . 19  |-  ( ( h `  k )  =  <. k ,  z
>.  ->  ( ( h `
 k )  e.  ( om  X.  A
)  ->  z  e.  A ) )
157153, 156syl5 32 . . . . . . . . . . . . . . . . . 18  |-  ( ( h `  k )  =  <. k ,  z
>.  ->  ( ( h : om --> ( om 
X.  A )  /\  k  e.  om )  ->  z  e.  A ) )
158157imp 429 . . . . . . . . . . . . . . . . 17  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  z  e.  A )
159 df-ov 6280 . . . . . . . . . . . . . . . . . 18  |-  ( k G z )  =  ( G `  <. k ,  z >. )
160 suceq 4929 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  k  ->  suc  n  =  suc  k )
161160sneqd 4022 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  k  ->  { suc  n }  =  { suc  k } )
162 oveq1 6284 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  k  ->  (
n F x )  =  ( k F x ) )
163161, 162xpeq12d 5010 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  k  ->  ( { suc  n }  X.  ( n F x ) )  =  ( { suc  k }  X.  ( k F x ) ) )
164 oveq2 6285 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  z  ->  (
k F x )  =  ( k F z ) )
165164xpeq2d 5009 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  z  ->  ( { suc  k }  X.  ( k F x ) )  =  ( { suc  k }  X.  ( k F z ) ) )
166 snex 4674 . . . . . . . . . . . . . . . . . . . 20  |-  { suc  k }  e.  _V
167 ovex 6305 . . . . . . . . . . . . . . . . . . . 20  |-  ( k F z )  e. 
_V
168166, 167xpex 6585 . . . . . . . . . . . . . . . . . . 19  |-  ( { suc  k }  X.  ( k F z ) )  e.  _V
169163, 165, 37, 168ovmpt2 6419 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  om  /\  z  e.  A )  ->  ( k G z )  =  ( { suc  k }  X.  ( k F z ) ) )
170159, 169syl5eqr 2496 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  om  /\  z  e.  A )  ->  ( G `  <. k ,  z >. )  =  ( { suc  k }  X.  (
k F z ) ) )
171152, 158, 170syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( G `  <. k ,  z
>. )  =  ( { suc  k }  X.  ( k F z ) ) )
172151, 171eqtrd 2482 . . . . . . . . . . . . . . 15  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( G `  ( h `  k
) )  =  ( { suc  k }  X.  ( k F z ) ) )
173172eleq2d 2511 . . . . . . . . . . . . . 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 5002 . . . . . . . . . . . . . . . . 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 6701 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  e.  om  ->  suc  k  e.  om )
176 fvco3 5931 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( h : om --> ( om 
X.  A )  /\  suc  k  e.  om )  ->  ( ( 2nd 
o.  h ) `  suc  k )  =  ( 2nd `  ( h `
 suc  k )
) )
177175, 176sylan2 474 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( h : om --> ( om 
X.  A )  /\  k  e.  om )  ->  ( ( 2nd  o.  h ) `  suc  k )  =  ( 2nd `  ( h `
 suc  k )
) )
178177adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . 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 753 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( h `  suc  k )  = 
<. s ,  t >.
)
180179fveq2d 5856 . . . . . . . . . . . . . . . . . . . . . . . . 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 2482 . . . . . . . . . . . . . . . . . . . . . . . 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 3096 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  s  e. 
_V
183 vex 3096 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  t  e. 
_V
184182, 183op2nd 6790 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 2nd `  <. s ,  t
>. )  =  t
185181, 184syl6eq 2498 . . . . . . . . . . . . . . . . . . . . . . 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 5931 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( h : om --> ( om 
X.  A )  /\  k  e.  om )  ->  ( ( 2nd  o.  h ) `  k
)  =  ( 2nd `  ( h `  k
) ) )
187186adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . 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 754 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( h `  k )  =  <. k ,  z >. )
189188fveq2d 5856 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2482 . . . . . . . . . . . . . . . . . . . . . . . . 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 3096 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  k  e. 
_V
192 vex 3096 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  z  e. 
_V
193191, 192op2nd 6790 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 2nd `  <. k ,  z
>. )  =  z
194190, 193syl6eq 2498 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( ( 2nd  o.  h ) `  k )  =  z )
195194oveq2d 6293 . . . . . . . . . . . . . . . . . . . . . . 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 2523 . . . . . . . . . . . . . . . . . . . . . 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 225 . . . . . . . . . . . . . . . . . . . . 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 608 . . . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . . 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 430 . . . . . . . . . . . . . . . . . 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 1708 . . . . . . . . . . . . . . . . 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 195 . . . . . . . . . . . . . . . 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 81 . . . . . . . . . . . . . . 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 429 . . . . . . . . . . . . . 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 215 . . . . . . . . . . . . 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 434 . . . . . . . . . . . 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 1707 . . . . . . . . . . 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 1189 . . . . . . . . . 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 1232 . . . . . . . . 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 1197 . . . . . . . 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 2841 . . . . . . 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 1175 . . . . . 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 5699 . . . . . . . 8  |-  ( g  =  ( 2nd  o.  h )  ->  (
g : om --> A  <->  ( 2nd  o.  h ) : om --> A ) )
214 fveq1 5851 . . . . . . . . 9  |-  ( g  =  ( 2nd  o.  h )  ->  (
g `  (/) )  =  ( ( 2nd  o.  h ) `  (/) ) )
215214eqeq1d 2443 . . . . . . . 8  |-  ( g  =  ( 2nd  o.  h )  ->  (
( g `  (/) )  =  C  <->  ( ( 2nd 
o.  h ) `  (/) )  =  C ) )
216 fveq1 5851 . . . . . . . . . 10  |-  ( g  =  ( 2nd  o.  h )  ->  (
g `  suc  k )  =  ( ( 2nd 
o.  h ) `  suc  k ) )
217 fveq1 5851 . . . . . . . . . . 11  |-  ( g  =  ( 2nd  o.  h )  ->  (
g `  k )  =  ( ( 2nd 
o.  h ) `  k ) )
218217oveq2d 6293 . . . . . . . . . 10  |-  ( g  =  ( 2nd  o.  h )  ->  (
k F ( g `
 k ) )  =  ( k F ( ( 2nd  o.  h ) `  k
) ) )
219216, 218eleq12d 2523 . . . . . . . . 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 2880 . . . . . . . 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 1298 . . . . . . 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 3179 . . . . . 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 60 . . . . 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 434 . . . 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 1709 . . 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 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 ) ) )  ->  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 369    /\ w3a 972    = wceq 1381   E.wex 1597    e. wcel 1802    =/= wne 2636   A.wral 2791   _Vcvv 3093    \ cdif 3455    C_ wss 3458   (/)c0 3767   ~Pcpw 3993   {csn 4010   <.cop 4016   suc csuc 4866    X. cxp 4983    o. ccom 4989   -->wf 5570   ` cfv 5574  (class class class)co 6277    |-> cmpt2 6279   omcom 6681   2ndc2nd 6780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pow 4611  ax-pr 4672  ax-un 6573  ax-dc 8824
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-reu 2798  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3418  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-pss 3474  df-nul 3768  df-if 3923  df-pw 3995  df-sn 4011  df-pr 4013  df-tp 4015  df-op 4017  df-uni 4231  df-iun 4313  df-br 4434  df-opab 4492  df-mpt 4493  df-tr 4527  df-eprel 4777  df-id 4781  df-po 4786  df-so 4787  df-fr 4824  df-we 4826  df-ord 4867  df-on 4868  df-lim 4869  df-suc 4870  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-iota 5537  df-fun 5576  df-fn 5577  df-f 5578  df-f1 5579  df-fo 5580  df-f1o 5581  df-fv 5582  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-om 6682  df-1st 6781  df-2nd 6782  df-1o 7128
This theorem is referenced by:  axdc4  8834
  Copyright terms: Public domain W3C validator