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

Theorem axdc4lem 8327
Description: Lemma for axdc4 8328. (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 4856 . . . 4  |-  (/)  e.  om
2 opelxpi 4902 . . . 4  |-  ( (
(/)  e.  om  /\  C  e.  A )  ->  <. (/) ,  C >.  e.  ( om  X.  A ) )
31, 2mpan 652 . . 3  |-  ( C  e.  A  ->  <. (/) ,  C >.  e.  ( om  X.  A ) )
4 simp2 958 . . . . . . . 8  |-  ( ( F : ( om 
X.  A ) --> ( ~P A  \  { (/)
} )  /\  n  e.  om  /\  x  e.  A )  ->  n  e.  om )
5 fovrn 6208 . . . . . . . 8  |-  ( ( F : ( om 
X.  A ) --> ( ~P A  \  { (/)
} )  /\  n  e.  om  /\  x  e.  A )  ->  (
n F x )  e.  ( ~P A  \  { (/) } ) )
6 peano2 4857 . . . . . . . . . . 11  |-  ( n  e.  om  ->  suc  n  e.  om )
76snssd 3935 . . . . . . . . . 10  |-  ( n  e.  om  ->  { suc  n }  C_  om )
8 eldifi 3461 . . . . . . . . . 10  |-  ( ( n F x )  e.  ( ~P A  \  { (/) } )  -> 
( n F x )  e.  ~P A
)
9 axdc4lem.1 . . . . . . . . . . . 12  |-  A  e. 
_V
109elpw2 4356 . . . . . . . . . . 11  |-  ( ( n F x )  e.  ~P A  <->  ( n F x )  C_  A )
11 xpss12 4973 . . . . . . . . . . 11  |-  ( ( { suc  n }  C_ 
om  /\  ( n F x )  C_  A )  ->  ( { suc  n }  X.  ( n F x ) )  C_  ( om  X.  A ) )
1210, 11sylan2b 462 . . . . . . . . . 10  |-  ( ( { suc  n }  C_ 
om  /\  ( n F x )  e. 
~P A )  -> 
( { suc  n }  X.  ( n F x ) )  C_  ( om  X.  A ) )
137, 8, 12syl2an 464 . . . . . . . . 9  |-  ( ( n  e.  om  /\  ( n F x )  e.  ( ~P A  \  { (/) } ) )  ->  ( { suc  n }  X.  ( n F x ) )  C_  ( om  X.  A ) )
14 snex 4397 . . . . . . . . . . 11  |-  { suc  n }  e.  _V
15 ovex 6098 . . . . . . . . . . 11  |-  ( n F x )  e. 
_V
1614, 15xpex 4982 . . . . . . . . . 10  |-  ( { suc  n }  X.  ( n F x ) )  e.  _V
1716elpw 3797 . . . . . . . . 9  |-  ( ( { suc  n }  X.  ( n F x ) )  e.  ~P ( om  X.  A )  <-> 
( { suc  n }  X.  ( n F x ) )  C_  ( om  X.  A ) )
1813, 17sylibr 204 . . . . . . . 8  |-  ( ( n  e.  om  /\  ( n F x )  e.  ( ~P A  \  { (/) } ) )  ->  ( { suc  n }  X.  ( n F x ) )  e.  ~P ( om  X.  A ) )
194, 5, 18syl2anc 643 . . . . . . 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 3462 . . . . . . . 8  |-  ( ( n F x )  e.  ( ~P A  \  { (/) } )  ->  -.  ( n F x )  e.  { (/) } )
2115elsnc 3829 . . . . . . . . . . 11  |-  ( ( n F x )  e.  { (/) }  <->  ( n F x )  =  (/) )
2221necon3bbii 2629 . . . . . . . . . 10  |-  ( -.  ( n F x )  e.  { (/) }  <-> 
( n F x )  =/=  (/) )
23 vex 2951 . . . . . . . . . . . . 13  |-  n  e. 
_V
2423sucex 4783 . . . . . . . . . . . 12  |-  suc  n  e.  _V
2524snnz 3914 . . . . . . . . . . 11  |-  { suc  n }  =/=  (/)
26 xpnz 5284 . . . . . . . . . . . 12  |-  ( ( { suc  n }  =/=  (/)  /\  ( n F x )  =/=  (/) )  <->  ( { suc  n }  X.  (
n F x ) )  =/=  (/) )
2726biimpi 187 . . . . . . . . . . 11  |-  ( ( { suc  n }  =/=  (/)  /\  ( n F x )  =/=  (/) )  ->  ( { suc  n }  X.  ( n F x ) )  =/=  (/) )
2825, 27mpan 652 . . . . . . . . . 10  |-  ( ( n F x )  =/=  (/)  ->  ( { suc  n }  X.  (
n F x ) )  =/=  (/) )
2922, 28sylbi 188 . . . . . . . . 9  |-  ( -.  ( n F x )  e.  { (/) }  ->  ( { suc  n }  X.  (
n F x ) )  =/=  (/) )
3016elsnc 3829 . . . . . . . . . 10  |-  ( ( { suc  n }  X.  ( n F x ) )  e.  { (/)
}  <->  ( { suc  n }  X.  (
n F x ) )  =  (/) )
3130necon3bbii 2629 . . . . . . . . 9  |-  ( -.  ( { suc  n }  X.  ( n F x ) )  e. 
{ (/) }  <->  ( { suc  n }  X.  (
n F x ) )  =/=  (/) )
3229, 31sylibr 204 . . . . . . . 8  |-  ( -.  ( n F x )  e.  { (/) }  ->  -.  ( { suc  n }  X.  (
n F x ) )  e.  { (/) } )
335, 20, 323syl 19 . . . . . . 7  |-  ( ( F : ( om 
X.  A ) --> ( ~P A  \  { (/)
} )  /\  n  e.  om  /\  x  e.  A )  ->  -.  ( { suc  n }  X.  ( n F x ) )  e.  { (/)
} )
3419, 33eldifd 3323 . . . . . 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 1156 . . . . 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 2789 . . . 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 6410 . . . 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 189 . . 3  |-  ( F : ( om  X.  A ) --> ( ~P A  \  { (/) } )  ->  G :
( om  X.  A
) --> ( ~P ( om  X.  A )  \  { (/) } ) )
40 dcomex 8319 . . . . 5  |-  om  e.  _V
4140, 9xpex 4982 . . . 4  |-  ( om 
X.  A )  e. 
_V
4241axdc3 8326 . . 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 464 . 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 6367 . . . . . . . . 9  |-  ( h : om --> ( om 
X.  A )  -> 
( 2nd  o.  h
) : om --> A )
45443ad2ant1 978 . . . . . . . 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 453 . . . . . . 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 5595 . . . . . . . 8  |-  ( ( ( 2nd  o.  h
) : om --> A  /\  om  e.  _V  /\  A  e.  _V )  ->  ( 2nd  o.  h )  e. 
_V )
4840, 9, 47mp3an23 1271 . . . . . . 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 5792 . . . . . . . . . . 11  |-  ( ( h : om --> ( om 
X.  A )  /\  (/) 
e.  om )  ->  (
( 2nd  o.  h
) `  (/) )  =  ( 2nd `  (
h `  (/) ) ) )
511, 50mpan2 653 . . . . . . . . . 10  |-  ( h : om --> ( om 
X.  A )  -> 
( ( 2nd  o.  h ) `  (/) )  =  ( 2nd `  (
h `  (/) ) ) )
52513ad2ant1 978 . . . . . . . . 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 5720 . . . . . . . . . 10  |-  ( ( h `  (/) )  = 
<. (/) ,  C >.  -> 
( 2nd `  (
h `  (/) ) )  =  ( 2nd `  <. (/)
,  C >. )
)
54533ad2ant2 979 . . . . . . . . 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 2467 . . . . . . . 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 6352 . . . . . . . . 9  |-  ( (
(/)  e.  om  /\  C  e.  A )  ->  ( 2nd `  <. (/) ,  C >. )  =  C )
571, 56mpan 652 . . . . . . . 8  |-  ( C  e.  A  ->  ( 2nd `  <. (/) ,  C >. )  =  C )
5855, 57sylan9eqr 2489 . . . . . . 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 1629 . . . . . . . . 9  |-  F/ k  C  e.  A
60 nfv 1629 . . . . . . . . . 10  |-  F/ k  h : om --> ( om 
X.  A )
61 nfv 1629 . . . . . . . . . 10  |-  F/ k ( h `  (/) )  = 
<. (/) ,  C >.
62 nfra1 2748 . . . . . . . . . 10  |-  F/ k A. k  e.  om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) )
6360, 61, 62nf3an 1849 . . . . . . . . 9  |-  F/ k ( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )
6459, 63nfan 1846 . . . . . . . 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 5720 . . . . . . . . . . . . . . . . 17  |-  ( m  =  (/)  ->  ( h `
 m )  =  ( h `  (/) ) )
66 opeq1 3976 . . . . . . . . . . . . . . . . 17  |-  ( m  =  (/)  ->  <. m ,  z >.  =  <. (/)
,  z >. )
6765, 66eqeq12d 2449 . . . . . . . . . . . . . . . 16  |-  ( m  =  (/)  ->  ( ( h `  m )  =  <. m ,  z
>. 
<->  ( h `  (/) )  = 
<. (/) ,  z >.
) )
6867exbidv 1636 . . . . . . . . . . . . . . 15  |-  ( m  =  (/)  ->  ( E. z ( h `  m )  =  <. m ,  z >.  <->  E. z
( h `  (/) )  = 
<. (/) ,  z >.
) )
69 fveq2 5720 . . . . . . . . . . . . . . . . 17  |-  ( m  =  i  ->  (
h `  m )  =  ( h `  i ) )
70 opeq1 3976 . . . . . . . . . . . . . . . . 17  |-  ( m  =  i  ->  <. m ,  z >.  =  <. i ,  z >. )
7169, 70eqeq12d 2449 . . . . . . . . . . . . . . . 16  |-  ( m  =  i  ->  (
( h `  m
)  =  <. m ,  z >.  <->  ( h `  i )  =  <. i ,  z >. )
)
7271exbidv 1636 . . . . . . . . . . . . . . 15  |-  ( m  =  i  ->  ( E. z ( h `  m )  =  <. m ,  z >.  <->  E. z
( h `  i
)  =  <. i ,  z >. )
)
73 fveq2 5720 . . . . . . . . . . . . . . . . 17  |-  ( m  =  suc  i  -> 
( h `  m
)  =  ( h `
 suc  i )
)
74 opeq1 3976 . . . . . . . . . . . . . . . . 17  |-  ( m  =  suc  i  ->  <. m ,  z >.  =  <. suc  i , 
z >. )
7573, 74eqeq12d 2449 . . . . . . . . . . . . . . . 16  |-  ( m  =  suc  i  -> 
( ( h `  m )  =  <. m ,  z >.  <->  ( h `  suc  i )  = 
<. suc  i ,  z
>. ) )
7675exbidv 1636 . . . . . . . . . . . . . . 15  |-  ( m  =  suc  i  -> 
( E. z ( h `  m )  =  <. m ,  z
>. 
<->  E. z ( h `
 suc  i )  =  <. suc  i , 
z >. ) )
77 opeq2 3977 . . . . . . . . . . . . . . . . . . 19  |-  ( z  =  C  ->  <. (/) ,  z
>.  =  <. (/) ,  C >. )
7877eqeq2d 2446 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  C  ->  (
( h `  (/) )  = 
<. (/) ,  z >.  <->  ( h `  (/) )  = 
<. (/) ,  C >. ) )
7978spcegv 3029 . . . . . . . . . . . . . . . . 17  |-  ( C  e.  A  ->  (
( h `  (/) )  = 
<. (/) ,  C >.  ->  E. z ( h `  (/) )  =  <. (/) ,  z
>. ) )
8079imp 419 . . . . . . . . . . . . . . . 16  |-  ( ( C  e.  A  /\  ( h `  (/) )  = 
<. (/) ,  C >. )  ->  E. z ( h `
 (/) )  =  <. (/)
,  z >. )
81803ad2antr2 1123 . . . . . . . . . . . . . . 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 5720 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( h `  i )  =  <. i ,  z
>.  ->  ( G `  ( h `  i
) )  =  ( G `  <. i ,  z >. )
)
83 df-ov 6076 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( i G z )  =  ( G `  <. i ,  z >. )
8482, 83syl6eqr 2485 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( h `  i )  =  <. i ,  z
>.  ->  ( G `  ( h `  i
) )  =  ( i G z ) )
8584adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( h : om --> ( om  X.  A )  /\  i  e.  om )  /\  ( h `  i )  =  <. i ,  z >. )  ->  ( G `  (
h `  i )
)  =  ( i G z ) )
86 simplr 732 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( h : om --> ( om  X.  A )  /\  i  e.  om )  /\  ( h `  i )  =  <. i ,  z >. )  ->  i  e.  om )
87 ffvelrn 5860 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( h : om --> ( om 
X.  A )  /\  i  e.  om )  ->  ( h `  i
)  e.  ( om 
X.  A ) )
88 eleq1 2495 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( h `  i )  =  <. i ,  z
>.  ->  ( ( h `
 i )  e.  ( om  X.  A
)  <->  <. i ,  z
>.  e.  ( om  X.  A ) ) )
89 opelxp2 4904 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( <.
i ,  z >.  e.  ( om  X.  A
)  ->  z  e.  A )
9088, 89syl6bi 220 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( h `  i )  =  <. i ,  z
>.  ->  ( ( h `
 i )  e.  ( om  X.  A
)  ->  z  e.  A ) )
9187, 90mpan9 456 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( h : om --> ( om  X.  A )  /\  i  e.  om )  /\  ( h `  i )  =  <. i ,  z >. )  ->  z  e.  A )
92 suceq 4638 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( n  =  i  ->  suc  n  =  suc  i )
9392sneqd 3819 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( n  =  i  ->  { suc  n }  =  { suc  i } )
94 oveq1 6080 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( n  =  i  ->  (
n F x )  =  ( i F x ) )
9593, 94xpeq12d 4895 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( n  =  i  ->  ( { suc  n }  X.  ( n F x ) )  =  ( { suc  i }  X.  ( i F x ) ) )
96 oveq2 6081 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  =  z  ->  (
i F x )  =  ( i F z ) )
9796xpeq2d 4894 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  =  z  ->  ( { suc  i }  X.  ( i F x ) )  =  ( { suc  i }  X.  ( i F z ) ) )
98 snex 4397 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  { suc  i }  e.  _V
99 ovex 6098 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( i F z )  e. 
_V
10098, 99xpex 4982 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( { suc  i }  X.  ( i F z ) )  e.  _V
10195, 97, 37, 100ovmpt2 6201 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( i  e.  om  /\  z  e.  A )  ->  ( i G z )  =  ( { suc  i }  X.  ( i F z ) ) )
10286, 91, 101syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( h : om --> ( om  X.  A )  /\  i  e.  om )  /\  ( h `  i )  =  <. i ,  z >. )  ->  ( i G z )  =  ( { suc  i }  X.  ( i F z ) ) )
10385, 102eqtrd 2467 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( h : om --> ( om  X.  A )  /\  i  e.  om )  /\  ( h `  i )  =  <. i ,  z >. )  ->  ( G `  (
h `  i )
)  =  ( { suc  i }  X.  ( i F z ) ) )
104 suceq 4638 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( k  =  i  ->  suc  k  =  suc  i )
105104fveq2d 5724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  =  i  ->  (
h `  suc  k )  =  ( h `  suc  i ) )
106 fveq2 5720 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( k  =  i  ->  (
h `  k )  =  ( h `  i ) )
107106fveq2d 5724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  =  i  ->  ( G `  ( h `  k ) )  =  ( G `  (
h `  i )
) )
108105, 107eleq12d 2503 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( k  =  i  ->  (
( h `  suc  k )  e.  ( G `  ( h `
 k ) )  <-> 
( h `  suc  i )  e.  ( G `  ( h `
 i ) ) ) )
109108rspcv 3040 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( i  e.  om  ->  ( A. k  e.  om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) )  ->  ( h `  suc  i )  e.  ( G `  ( h `
 i ) ) ) )
110109ad2antlr 708 . . . . . . . . . . . . . . . . . . . . . . . 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 2496 . . . . . . . . . . . . . . . . . . . . . . . . 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 4887 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( s  e.  { suc  i } 
<->  s  =  suc  i
)
114 opeq1 3976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( s  =  suc  i  ->  <. s ,  t >.  =  <. suc  i , 
t >. )
115113, 114sylbi 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( s  e.  { suc  i }  ->  <. s ,  t
>.  =  <. suc  i ,  t >. )
116115eqeq2d 2446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( s  e.  { suc  i }  ->  ( ( h `
 suc  i )  =  <. s ,  t
>. 
<->  ( h `  suc  i )  =  <. suc  i ,  t >.
) )
117116biimpac 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( h `  suc  i )  =  <. s ,  t >.  /\  s  e.  { suc  i } )  ->  ( h `  suc  i )  = 
<. suc  i ,  t
>. )
118117adantrr 698 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( h `  suc  i )  =  <. s ,  t >.  /\  (
s  e.  { suc  i }  /\  t  e.  ( i F z ) ) )  -> 
( h `  suc  i )  =  <. suc  i ,  t >.
)
119118eximi 1585 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1644 . . . . . . . . . . . . . . . . . . . . . . . . . 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 188 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( h `  suc  i
)  e.  ( { suc  i }  X.  ( i F z ) )  ->  E. t
( h `  suc  i )  =  <. suc  i ,  t >.
)
122111, 121syl6bi 220 . . . . . . . . . . . . . . . . . . . . . . . 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 54 . . . . . . . . . . . . . . . . . . . . . . 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 425 . . . . . . . . . . . . . . . . . . . . . 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 1644 . . . . . . . . . . . . . . . . . . . . 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 77 . . . . . . . . . . . . . . . . . . . 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 3977 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( t  =  z  ->  <. suc  i ,  t >.  =  <. suc  i ,  z >.
)
128127eqeq2d 2446 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  =  z  ->  (
( h `  suc  i )  =  <. suc  i ,  t >.  <->  ( h `  suc  i
)  =  <. suc  i ,  z >. )
)
129128cbvexv 1985 . . . . . . . . . . . . . . . . . . . 20  |-  ( E. t ( h `  suc  i )  =  <. suc  i ,  t >.  <->  E. z ( h `  suc  i )  =  <. suc  i ,  z >.
)
130126, 129syl8ib 223 . . . . . . . . . . . . . . . . . . 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 428 . . . . . . . . . . . . . . . . . 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 976 . . . . . . . . . . . . . . . . 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 453 . . . . . . . . . . . . . . . 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 29 . . . . . . . . . . . . . . 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 4865 . . . . . . . . . . . . . 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 29 . . . . . . . . . . . . 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 2780 . . . . . . . . . . . 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 5720 . . . . . . . . . . . . . . 15  |-  ( m  =  k  ->  (
h `  m )  =  ( h `  k ) )
139 opeq1 3976 . . . . . . . . . . . . . . 15  |-  ( m  =  k  ->  <. m ,  z >.  =  <. k ,  z >. )
140138, 139eqeq12d 2449 . . . . . . . . . . . . . 14  |-  ( m  =  k  ->  (
( h `  m
)  =  <. m ,  z >.  <->  ( h `  k )  =  <. k ,  z >. )
)
141140exbidv 1636 . . . . . . . . . . . . 13  |-  ( m  =  k  ->  ( E. z ( h `  m )  =  <. m ,  z >.  <->  E. z
( h `  k
)  =  <. k ,  z >. )
)
142141rspccv 3041 . . . . . . . . . . . 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 1150 . . . . . . . . . 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 990 . . . . . . . . . 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 959 . . . . . . . . . 10  |-  ( ( C  e.  A  /\  ( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  /\  k  e. 
om )  ->  k  e.  om )
147 rsp 2758 . . . . . . . . . . . . 13  |-  ( A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) )  ->  (
k  e.  om  ->  ( h `  suc  k
)  e.  ( G `
 ( h `  k ) ) ) )
148147imp 419 . . . . . . . . . . . 12  |-  ( ( A. k  e.  om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) )  /\  k  e.  om )  ->  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )
1491483ad2antl3 1121 . . . . . . . . . . 11  |-  ( ( ( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  /\  k  e. 
om )  ->  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )
1501493adant1 975 . . . . . . . . . 10  |-  ( ( C  e.  A  /\  ( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  /\  k  e. 
om )  ->  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )
151 simpl 444 . . . . . . . . . . . . . . . . 17  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( h `  k )  =  <. k ,  z >. )
152151fveq2d 5724 . . . . . . . . . . . . . . . 16  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( G `  ( h `  k
) )  =  ( G `  <. k ,  z >. )
)
153 simprr 734 . . . . . . . . . . . . . . . . 17  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  k  e.  om )
154 ffvelrn 5860 . . . . . . . . . . . . . . . . . . 19  |-  ( ( h : om --> ( om 
X.  A )  /\  k  e.  om )  ->  ( h `  k
)  e.  ( om 
X.  A ) )
155 eleq1 2495 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( h `  k )  =  <. k ,  z
>.  ->  ( ( h `
 k )  e.  ( om  X.  A
)  <->  <. k ,  z
>.  e.  ( om  X.  A ) ) )
156 opelxp2 4904 . . . . . . . . . . . . . . . . . . . 20  |-  ( <.
k ,  z >.  e.  ( om  X.  A
)  ->  z  e.  A )
157155, 156syl6bi 220 . . . . . . . . . . . . . . . . . . 19  |-  ( ( h `  k )  =  <. k ,  z
>.  ->  ( ( h `
 k )  e.  ( om  X.  A
)  ->  z  e.  A ) )
158154, 157syl5 30 . . . . . . . . . . . . . . . . . 18  |-  ( ( h `  k )  =  <. k ,  z
>.  ->  ( ( h : om --> ( om 
X.  A )  /\  k  e.  om )  ->  z  e.  A ) )
159158imp 419 . . . . . . . . . . . . . . . . 17  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  z  e.  A )
160 df-ov 6076 . . . . . . . . . . . . . . . . . 18  |-  ( k G z )  =  ( G `  <. k ,  z >. )
161 suceq 4638 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  k  ->  suc  n  =  suc  k )
162161sneqd 3819 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  k  ->  { suc  n }  =  { suc  k } )
163 oveq1 6080 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  k  ->  (
n F x )  =  ( k F x ) )
164162, 163xpeq12d 4895 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  k  ->  ( { suc  n }  X.  ( n F x ) )  =  ( { suc  k }  X.  ( k F x ) ) )
165 oveq2 6081 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  z  ->  (
k F x )  =  ( k F z ) )
166165xpeq2d 4894 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  z  ->  ( { suc  k }  X.  ( k F x ) )  =  ( { suc  k }  X.  ( k F z ) ) )
167 snex 4397 . . . . . . . . . . . . . . . . . . . 20  |-  { suc  k }  e.  _V
168 ovex 6098 . . . . . . . . . . . . . . . . . . . 20  |-  ( k F z )  e. 
_V
169167, 168xpex 4982 . . . . . . . . . . . . . . . . . . 19  |-  ( { suc  k }  X.  ( k F z ) )  e.  _V
170164, 166, 37, 169ovmpt2 6201 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  om  /\  z  e.  A )  ->  ( k G z )  =  ( { suc  k }  X.  ( k F z ) ) )
171160, 170syl5eqr 2481 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  om  /\  z  e.  A )  ->  ( G `  <. k ,  z >. )  =  ( { suc  k }  X.  (
k F z ) ) )
172153, 159, 171syl2anc 643 . . . . . . . . . . . . . . . 16  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( G `  <. k ,  z
>. )  =  ( { suc  k }  X.  ( k F z ) ) )
173152, 172eqtrd 2467 . . . . . . . . . . . . . . 15  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( G `  ( h `  k
) )  =  ( { suc  k }  X.  ( k F z ) ) )
174173eleq2d 2502 . . . . . . . . . . . . . 14  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( (
h `  suc  k )  e.  ( G `  ( h `  k
) )  <->  ( h `  suc  k )  e.  ( { suc  k }  X.  ( k F z ) ) ) )
175 elxp 4887 . . . . . . . . . . . . . . . . 17  |-  ( ( h `  suc  k
)  e.  ( { suc  k }  X.  ( k F z ) )  <->  E. s E. t ( ( h `
 suc  k )  =  <. s ,  t
>.  /\  ( s  e. 
{ suc  k }  /\  t  e.  (
k F z ) ) ) )
176 peano2 4857 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  e.  om  ->  suc  k  e.  om )
177 fvco3 5792 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( h : om --> ( om 
X.  A )  /\  suc  k  e.  om )  ->  ( ( 2nd 
o.  h ) `  suc  k )  =  ( 2nd `  ( h `
 suc  k )
) )
178176, 177sylan2 461 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( h : om --> ( om 
X.  A )  /\  k  e.  om )  ->  ( ( 2nd  o.  h ) `  suc  k )  =  ( 2nd `  ( h `
 suc  k )
) )
179178adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( ( 2nd  o.  h ) `  suc  k )  =  ( 2nd `  ( h `
 suc  k )
) )
180 simpll 731 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( h `  suc  k )  = 
<. s ,  t >.
)
181180fveq2d 5724 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( 2nd `  ( h `  suc  k ) )  =  ( 2nd `  <. s ,  t >. )
)
182179, 181eqtrd 2467 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( ( 2nd  o.  h ) `  suc  k )  =  ( 2nd `  <. s ,  t >. )
)
183 vex 2951 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  s  e. 
_V
184 vex 2951 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  t  e. 
_V
185183, 184op2nd 6348 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 2nd `  <. s ,  t
>. )  =  t
186182, 185syl6eq 2483 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( ( 2nd  o.  h ) `  suc  k )  =  t )
187 fvco3 5792 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( h : om --> ( om 
X.  A )  /\  k  e.  om )  ->  ( ( 2nd  o.  h ) `  k
)  =  ( 2nd `  ( h `  k
) ) )
188187adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( ( 2nd  o.  h ) `  k )  =  ( 2nd `  ( h `
 k ) ) )
189 simplr 732 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( h `  k )  =  <. k ,  z >. )
190189fveq2d 5724 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( 2nd `  ( h `  k
) )  =  ( 2nd `  <. k ,  z >. )
)
191188, 190eqtrd 2467 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( ( 2nd  o.  h ) `  k )  =  ( 2nd `  <. k ,  z >. )
)
192 vex 2951 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  k  e. 
_V
193 vex 2951 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  z  e. 
_V
194192, 193op2nd 6348 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 2nd `  <. k ,  z
>. )  =  z
195191, 194syl6eq 2483 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( ( 2nd  o.  h ) `  k )  =  z )
196195oveq2d 6089 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( k F ( ( 2nd 
o.  h ) `  k ) )  =  ( k F z ) )
197186, 196eleq12d 2503 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
h `  k )  =  <. k ,  z
>. )  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( (
( 2nd  o.  h
) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `  k
) )  <->  t  e.  ( k F z ) ) )
198197biimprcd 217 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  e.  ( k F z )  ->  (
( ( ( h `
 suc  k )  =  <. s ,  t
>.  /\  ( h `  k )  =  <. k ,  z >. )  /\  ( h : om --> ( om  X.  A )  /\  k  e.  om ) )  ->  (
( 2nd  o.  h
) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `  k
) ) ) )
199198exp4c 592 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  e.  ( k F z )  ->  (
( h `  suc  k )  =  <. s ,  t >.  ->  (
( h `  k
)  =  <. k ,  z >.  ->  (
( h : om --> ( om  X.  A )  /\  k  e.  om )  ->  ( ( 2nd 
o.  h ) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `
 k ) ) ) ) ) )
200199adantl 453 . . . . . . . . . . . . . . . . . . 19  |-  ( ( s  e.  { suc  k }  /\  t  e.  ( k F z ) )  ->  (
( h `  suc  k )  =  <. s ,  t >.  ->  (
( h `  k
)  =  <. k ,  z >.  ->  (
( h : om --> ( om  X.  A )  /\  k  e.  om )  ->  ( ( 2nd 
o.  h ) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `
 k ) ) ) ) ) )
201200impcom 420 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
s  e.  { suc  k }  /\  t  e.  ( k F z ) ) )  -> 
( ( h `  k )  =  <. k ,  z >.  ->  (
( h : om --> ( om  X.  A )  /\  k  e.  om )  ->  ( ( 2nd 
o.  h ) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `
 k ) ) ) ) )
202201exlimivv 1645 . . . . . . . . . . . . . . . . 17  |-  ( E. s E. t ( ( h `  suc  k )  =  <. s ,  t >.  /\  (
s  e.  { suc  k }  /\  t  e.  ( k F z ) ) )  -> 
( ( h `  k )  =  <. k ,  z >.  ->  (
( h : om --> ( om  X.  A )  /\  k  e.  om )  ->  ( ( 2nd 
o.  h ) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `
 k ) ) ) ) )
203175, 202sylbi 188 . . . . . . . . . . . . . . . 16  |-  ( ( h `  suc  k
)  e.  ( { suc  k }  X.  ( k F z ) )  ->  (
( h `  k
)  =  <. k ,  z >.  ->  (
( h : om --> ( om  X.  A )  /\  k  e.  om )  ->  ( ( 2nd 
o.  h ) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `
 k ) ) ) ) )
204203com3l 77 . . . . . . . . . . . . . . 15  |-  ( ( h `  k )  =  <. k ,  z
>.  ->  ( ( h : om --> ( om 
X.  A )  /\  k  e.  om )  ->  ( ( h `  suc  k )  e.  ( { suc  k }  X.  ( k F z ) )  -> 
( ( 2nd  o.  h ) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `
 k ) ) ) ) )
205204imp 419 . . . . . . . . . . . . . 14  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( (
h `  suc  k )  e.  ( { suc  k }  X.  (
k F z ) )  ->  ( ( 2nd  o.  h ) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `
 k ) ) ) )
206174, 205sylbid 207 . . . . . . . . . . . . 13  |-  ( ( ( h `  k
)  =  <. k ,  z >.  /\  (
h : om --> ( om 
X.  A )  /\  k  e.  om )
)  ->  ( (
h `  suc  k )  e.  ( G `  ( h `  k
) )  ->  (
( 2nd  o.  h
) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `  k
) ) ) )
207206ex 424 . . . . . . . . . . . 12  |-  ( ( h `  k )  =  <. k ,  z
>.  ->  ( ( h : om --> ( om 
X.  A )  /\  k  e.  om )  ->  ( ( h `  suc  k )  e.  ( G `  ( h `
 k ) )  ->  ( ( 2nd 
o.  h ) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `
 k ) ) ) ) )
208207exlimiv 1644 . . . . . . . . . . 11  |-  ( E. z ( h `  k )  =  <. k ,  z >.  ->  (
( h : om --> ( om  X.  A )  /\  k  e.  om )  ->  ( ( h `
 suc  k )  e.  ( G `  (
h `  k )
)  ->  ( ( 2nd  o.  h ) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `
 k ) ) ) ) )
2092083imp 1147 . . . . . . . . . 10  |-  ( ( E. z ( h `
 k )  = 
<. k ,  z >.  /\  ( h : om --> ( om  X.  A )  /\  k  e.  om )  /\  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  ->  ( ( 2nd  o.  h ) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `
 k ) ) )
210144, 145, 146, 150, 209syl121anc 1189 . . . . . . . . 9  |-  ( ( C  e.  A  /\  ( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  /\  k  e. 
om )  ->  (
( 2nd  o.  h
) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `  k
) ) )
2112103expia 1155 . . . . . . . 8  |-  ( ( C  e.  A  /\  ( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )  ->  (
k  e.  om  ->  ( ( 2nd  o.  h
) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `  k
) ) ) )
21264, 211ralrimi 2779 . . . . . . 7  |-  ( ( C  e.  A  /\  ( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )  ->  A. k  e.  om  ( ( 2nd 
o.  h ) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `
 k ) ) )
21346, 58, 2123jca 1134 . . . . . 6  |-  ( ( C  e.  A  /\  ( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )  ->  (
( 2nd  o.  h
) : om --> A  /\  ( ( 2nd  o.  h ) `  (/) )  =  C  /\  A. k  e.  om  ( ( 2nd 
o.  h ) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `
 k ) ) ) )
214 feq1 5568 . . . . . . . 8  |-  ( g  =  ( 2nd  o.  h )  ->  (
g : om --> A  <->  ( 2nd  o.  h ) : om --> A ) )
215 fveq1 5719 . . . . . . . . 9  |-  ( g  =  ( 2nd  o.  h )  ->  (
g `  (/) )  =  ( ( 2nd  o.  h ) `  (/) ) )
216215eqeq1d 2443 . . . . . . . 8  |-  ( g  =  ( 2nd  o.  h )  ->  (
( g `  (/) )  =  C  <->  ( ( 2nd 
o.  h ) `  (/) )  =  C ) )
217 fveq1 5719 . . . . . . . . . 10  |-  ( g  =  ( 2nd  o.  h )  ->  (
g `  suc  k )  =  ( ( 2nd 
o.  h ) `  suc  k ) )
218 fveq1 5719 . . . . . . . . . . 11  |-  ( g  =  ( 2nd  o.  h )  ->  (
g `  k )  =  ( ( 2nd 
o.  h ) `  k ) )
219218oveq2d 6089 . . . . . . . . . 10  |-  ( g  =  ( 2nd  o.  h )  ->  (
k F ( g `
 k ) )  =  ( k F ( ( 2nd  o.  h ) `  k
) ) )
220217, 219eleq12d 2503 . . . . . . . . 9  |-  ( g  =  ( 2nd  o.  h )  ->  (
( g `  suc  k )  e.  ( k F ( g `
 k ) )  <-> 
( ( 2nd  o.  h ) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `
 k ) ) ) )
221220ralbidv 2717 . . . . . . . 8  |-  ( g  =  ( 2nd  o.  h )  ->  ( A. k  e.  om  ( g `  suc  k )  e.  ( k F ( g `
 k ) )  <->  A. k  e.  om  ( ( 2nd  o.  h ) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `
 k ) ) ) )
222214, 216, 2213anbi123d 1254 . . . . . . 7  |-  ( g  =  ( 2nd  o.  h )  ->  (
( g : om --> A  /\  ( g `  (/) )  =  C  /\  A. k  e.  om  (
g `  suc  k )  e.  ( k F ( g `  k
) ) )  <->  ( ( 2nd  o.  h ) : om --> A  /\  (
( 2nd  o.  h
) `  (/) )  =  C  /\  A. k  e.  om  ( ( 2nd 
o.  h ) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `
 k ) ) ) ) )
223222spcegv 3029 . . . . . 6  |-  ( ( 2nd  o.  h )  e.  _V  ->  (
( ( 2nd  o.  h ) : om --> A  /\  ( ( 2nd 
o.  h ) `  (/) )  =  C  /\  A. k  e.  om  (
( 2nd  o.  h
) `  suc  k )  e.  ( k F ( ( 2nd  o.  h ) `  k
) ) )  ->  E. g ( g : om --> A  /\  (
g `  (/) )  =  C  /\  A. k  e.  om  ( g `  suc  k )  e.  ( k F ( g `
 k ) ) ) ) )
22449, 213, 223sylc 58 . . . . 5  |-  ( ( C  e.  A  /\  ( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )  ->  E. g
( g : om --> A  /\  ( g `  (/) )  =  C  /\  A. k  e.  om  (
g `  suc  k )  e.  ( k F ( g `  k
) ) ) )
225224ex 424 . . . 4  |-  ( C  e.  A  ->  (
( h : om --> ( om  X.  A )  /\  ( h `  (/) )  =  <. (/) ,  C >.  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  ->  E. g
( g : om --> A  /\  ( g `  (/) )  =  C  /\  A. k  e.  om  (
g `  suc  k )  e.  ( k F ( g `  k
) ) ) ) )
226225exlimdv 1646 . . 3  |-  ( C  e.  A  ->  ( E. h ( h : om --> ( om  X.  A )  /\  (
h `  (/) )  = 
<. (/) ,  C >.  /\ 
A. k  e.  om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  ->  E. g
( g : om --> A  /\  ( g `  (/) )  =  C  /\  A. k  e.  om  (
g `  suc  k )  e.  ( k F ( g `  k
) ) ) ) )
227226adantr 452 . 2  |-  ( ( C  e.  A  /\  F : ( om  X.  A ) --> ( ~P A  \  { (/) } ) )  ->  ( E. h ( h : om --> ( om  X.  A )  /\  (
h `  (/) )  = 
<. (/) ,  C >.  /\ 
A. k  e.  om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  ->  E. g
( g : om --> A  /\  ( g `  (/) )  =  C  /\  A. k  e.  om  (
g `  suc  k )  e.  ( k F ( g `  k
) ) ) ) )
22843, 227mpd 15 1  |-  ( ( C  e.  A  /\  F : ( om  X.  A ) --> ( ~P A  \  { (/) } ) )  ->  E. g
( g : om --> A  /\  ( g `  (/) )  =  C  /\  A. k  e.  om  (
g `  suc  k )  e.  ( k F ( g `  k
) ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 359    /\ w3a 936   E.wex 1550    = wceq 1652    e. wcel 1725    =/= wne 2598   A.wral 2697   _Vcvv 2948    \ cdif 3309    C_ wss 3312   (/)c0 3620   ~Pcpw 3791   {csn 3806   <.cop 3809   suc csuc 4575   omcom 4837    X. cxp 4868    o. ccom 4874   -->wf 5442   ` cfv 5446  (class class class)co 6073    e. cmpt2 6075   2ndc2nd 6340
This theorem is referenced by:  axdc4  8328
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693  ax-dc 8318
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-reu 2704  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-iun 4087  df-br 4205  df-opab 4259  df-mpt 4260  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-om 4838  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454  df-ov 6076  df-oprab 6077  df-mpt2 6078  df-1st 6341  df-2nd 6342  df-1o 6716
  Copyright terms: Public domain W3C validator