Metamath Proof Explorer

Theorem axdc4lem

Description: Lemma for axdc4 . (Contributed by Mario Carneiro, 31-Jan-2013) (Revised by Mario Carneiro, 16-Nov-2013)

Ref Expression
Hypotheses axdc4lem.1 
|- A e. _V
axdc4lem.2 
|- G = ( n e. _om , x e. A |-> ( { suc n } X. ( n F x ) ) )
Assertion 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 ) ) ) )

Proof

Step Hyp Ref Expression
1 axdc4lem.1 
 |-  A e. _V
2 axdc4lem.2 
 |-  G = ( n e. _om , x e. A |-> ( { suc n } X. ( n F x ) ) )
3 peano1 
 |-  (/) e. _om
4 opelxpi 
 |-  ( ( (/) e. _om /\ C e. A ) -> <. (/) , C >. e. ( _om X. A ) )
5 3 4 mpan 
 |-  ( C e. A -> <. (/) , C >. e. ( _om X. A ) )
6 simp2 
 |-  ( ( F : ( _om X. A ) --> ( ~P A \ { (/) } ) /\ n e. _om /\ x e. A ) -> n e. _om )
7 fovcdm 
 |-  ( ( F : ( _om X. A ) --> ( ~P A \ { (/) } ) /\ n e. _om /\ x e. A ) -> ( n F x ) e. ( ~P A \ { (/) } ) )
8 peano2 
 |-  ( n e. _om -> suc n e. _om )
9 8 snssd 
 |-  ( n e. _om -> { suc n } C_ _om )
10 eldifi 
 |-  ( ( n F x ) e. ( ~P A \ { (/) } ) -> ( n F x ) e. ~P A )
11 1 elpw2 
 |-  ( ( n F x ) e. ~P A <-> ( n F x ) C_ A )
12 xpss12 
 |-  ( ( { suc n } C_ _om /\ ( n F x ) C_ A ) -> ( { suc n } X. ( n F x ) ) C_ ( _om X. A ) )
13 11 12 sylan2b 
 |-  ( ( { suc n } C_ _om /\ ( n F x ) e. ~P A ) -> ( { suc n } X. ( n F x ) ) C_ ( _om X. A ) )
14 9 10 13 syl2an 
 |-  ( ( n e. _om /\ ( n F x ) e. ( ~P A \ { (/) } ) ) -> ( { suc n } X. ( n F x ) ) C_ ( _om X. A ) )
15 snex 
 |-  { suc n } e. _V
16 ovex 
 |-  ( n F x ) e. _V
17 15 16 xpex 
 |-  ( { suc n } X. ( n F x ) ) e. _V
18 17 elpw 
 |-  ( ( { suc n } X. ( n F x ) ) e. ~P ( _om X. A ) <-> ( { suc n } X. ( n F x ) ) C_ ( _om X. A ) )
19 14 18 sylibr 
 |-  ( ( n e. _om /\ ( n F x ) e. ( ~P A \ { (/) } ) ) -> ( { suc n } X. ( n F x ) ) e. ~P ( _om X. A ) )
20 6 7 19 syl2anc 
 |-  ( ( F : ( _om X. A ) --> ( ~P A \ { (/) } ) /\ n e. _om /\ x e. A ) -> ( { suc n } X. ( n F x ) ) e. ~P ( _om X. A ) )
21 eldifn 
 |-  ( ( n F x ) e. ( ~P A \ { (/) } ) -> -. ( n F x ) e. { (/) } )
22 16 elsn 
 |-  ( ( n F x ) e. { (/) } <-> ( n F x ) = (/) )
23 22 necon3bbii 
 |-  ( -. ( n F x ) e. { (/) } <-> ( n F x ) =/= (/) )
24 vex 
 |-  n e. _V
25 24 sucex 
 |-  suc n e. _V
26 25 snnz 
 |-  { suc n } =/= (/)
27 xpnz 
 |-  ( ( { suc n } =/= (/) /\ ( n F x ) =/= (/) ) <-> ( { suc n } X. ( n F x ) ) =/= (/) )
28 27 biimpi 
 |-  ( ( { suc n } =/= (/) /\ ( n F x ) =/= (/) ) -> ( { suc n } X. ( n F x ) ) =/= (/) )
29 26 28 mpan 
 |-  ( ( n F x ) =/= (/) -> ( { suc n } X. ( n F x ) ) =/= (/) )
30 23 29 sylbi 
 |-  ( -. ( n F x ) e. { (/) } -> ( { suc n } X. ( n F x ) ) =/= (/) )
31 17 elsn 
 |-  ( ( { suc n } X. ( n F x ) ) e. { (/) } <-> ( { suc n } X. ( n F x ) ) = (/) )
32 31 necon3bbii 
 |-  ( -. ( { suc n } X. ( n F x ) ) e. { (/) } <-> ( { suc n } X. ( n F x ) ) =/= (/) )
33 30 32 sylibr 
 |-  ( -. ( n F x ) e. { (/) } -> -. ( { suc n } X. ( n F x ) ) e. { (/) } )
34 7 21 33 3syl 
 |-  ( ( F : ( _om X. A ) --> ( ~P A \ { (/) } ) /\ n e. _om /\ x e. A ) -> -. ( { suc n } X. ( n F x ) ) e. { (/) } )
35 20 34 eldifd 
 |-  ( ( F : ( _om X. A ) --> ( ~P A \ { (/) } ) /\ n e. _om /\ x e. A ) -> ( { suc n } X. ( n F x ) ) e. ( ~P ( _om X. A ) \ { (/) } ) )
36 35 3expib 
 |-  ( F : ( _om X. A ) --> ( ~P A \ { (/) } ) -> ( ( n e. _om /\ x e. A ) -> ( { suc n } X. ( n F x ) ) e. ( ~P ( _om X. A ) \ { (/) } ) ) )
37 36 ralrimivv 
 |-  ( F : ( _om X. A ) --> ( ~P A \ { (/) } ) -> A. n e. _om A. x e. A ( { suc n } X. ( n F x ) ) e. ( ~P ( _om X. A ) \ { (/) } ) )
38 2 fmpo 
 |-  ( 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 ) \ { (/) } ) )
39 37 38 sylib 
 |-  ( F : ( _om X. A ) --> ( ~P A \ { (/) } ) -> G : ( _om X. A ) --> ( ~P ( _om X. A ) \ { (/) } ) )
40 dcomex 
 |-  _om e. _V
41 40 1 xpex 
 |-  ( _om X. A ) e. _V
42 41 axdc3 
 |-  ( ( <. (/) , 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 ) ) ) )
43 5 39 42 syl2an 
 |-  ( ( 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 
 |-  ( h : _om --> ( _om X. A ) -> ( 2nd o. h ) : _om --> A )
45 44 3ad2ant1 
 |-  ( ( h : _om --> ( _om X. A ) /\ ( h ` (/) ) = <. (/) , C >. /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( 2nd o. h ) : _om --> A )
46 45 adantl 
 |-  ( ( 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 
 |-  ( ( ( 2nd o. h ) : _om --> A /\ _om e. _V /\ A e. _V ) -> ( 2nd o. h ) e. _V )
48 40 1 47 mp3an23 
 |-  ( ( 2nd o. h ) : _om --> A -> ( 2nd o. h ) e. _V )
49 46 48 syl 
 |-  ( ( 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 
 |-  ( ( h : _om --> ( _om X. A ) /\ (/) e. _om ) -> ( ( 2nd o. h ) ` (/) ) = ( 2nd ` ( h ` (/) ) ) )
51 3 50 mpan2 
 |-  ( h : _om --> ( _om X. A ) -> ( ( 2nd o. h ) ` (/) ) = ( 2nd ` ( h ` (/) ) ) )
52 51 3ad2ant1 
 |-  ( ( 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 
 |-  ( ( h ` (/) ) = <. (/) , C >. -> ( 2nd ` ( h ` (/) ) ) = ( 2nd ` <. (/) , C >. ) )
54 53 3ad2ant2 
 |-  ( ( h : _om --> ( _om X. A ) /\ ( h ` (/) ) = <. (/) , C >. /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( 2nd ` ( h ` (/) ) ) = ( 2nd ` <. (/) , C >. ) )
55 52 54 eqtrd 
 |-  ( ( 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 
 |-  ( ( (/) e. _om /\ C e. A ) -> ( 2nd ` <. (/) , C >. ) = C )
57 3 56 mpan 
 |-  ( C e. A -> ( 2nd ` <. (/) , C >. ) = C )
58 55 57 sylan9eqr 
 |-  ( ( 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 
 |-  F/ k C e. A
60 nfv 
 |-  F/ k h : _om --> ( _om X. A )
61 nfv 
 |-  F/ k ( h ` (/) ) = <. (/) , C >.
62 nfra1 
 |-  F/ k A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) )
63 60 61 62 nf3an 
 |-  F/ k ( h : _om --> ( _om X. A ) /\ ( h ` (/) ) = <. (/) , C >. /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) )
64 59 63 nfan 
 |-  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 
 |-  ( m = (/) -> ( h ` m ) = ( h ` (/) ) )
66 opeq1 
 |-  ( m = (/) -> <. m , z >. = <. (/) , z >. )
67 65 66 eqeq12d 
 |-  ( m = (/) -> ( ( h ` m ) = <. m , z >. <-> ( h ` (/) ) = <. (/) , z >. ) )
68 67 exbidv 
 |-  ( m = (/) -> ( E. z ( h ` m ) = <. m , z >. <-> E. z ( h ` (/) ) = <. (/) , z >. ) )
69 fveq2 
 |-  ( m = i -> ( h ` m ) = ( h ` i ) )
70 opeq1 
 |-  ( m = i -> <. m , z >. = <. i , z >. )
71 69 70 eqeq12d 
 |-  ( m = i -> ( ( h ` m ) = <. m , z >. <-> ( h ` i ) = <. i , z >. ) )
72 71 exbidv 
 |-  ( m = i -> ( E. z ( h ` m ) = <. m , z >. <-> E. z ( h ` i ) = <. i , z >. ) )
73 fveq2 
 |-  ( m = suc i -> ( h ` m ) = ( h ` suc i ) )
74 opeq1 
 |-  ( m = suc i -> <. m , z >. = <. suc i , z >. )
75 73 74 eqeq12d 
 |-  ( m = suc i -> ( ( h ` m ) = <. m , z >. <-> ( h ` suc i ) = <. suc i , z >. ) )
76 75 exbidv 
 |-  ( m = suc i -> ( E. z ( h ` m ) = <. m , z >. <-> E. z ( h ` suc i ) = <. suc i , z >. ) )
77 opeq2 
 |-  ( z = C -> <. (/) , z >. = <. (/) , C >. )
78 77 eqeq2d 
 |-  ( z = C -> ( ( h ` (/) ) = <. (/) , z >. <-> ( h ` (/) ) = <. (/) , C >. ) )
79 78 spcegv 
 |-  ( C e. A -> ( ( h ` (/) ) = <. (/) , C >. -> E. z ( h ` (/) ) = <. (/) , z >. ) )
80 79 imp 
 |-  ( ( C e. A /\ ( h ` (/) ) = <. (/) , C >. ) -> E. z ( h ` (/) ) = <. (/) , z >. )
81 80 3ad2antr2 
 |-  ( ( 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 
 |-  ( ( h ` i ) = <. i , z >. -> ( G ` ( h ` i ) ) = ( G ` <. i , z >. ) )
83 df-ov 
 |-  ( i G z ) = ( G ` <. i , z >. )
84 82 83 eqtr4di 
 |-  ( ( h ` i ) = <. i , z >. -> ( G ` ( h ` i ) ) = ( i G z ) )
85 84 adantl 
 |-  ( ( ( h : _om --> ( _om X. A ) /\ i e. _om ) /\ ( h ` i ) = <. i , z >. ) -> ( G ` ( h ` i ) ) = ( i G z ) )
86 simplr 
 |-  ( ( ( h : _om --> ( _om X. A ) /\ i e. _om ) /\ ( h ` i ) = <. i , z >. ) -> i e. _om )
87 ffvelcdm 
 |-  ( ( h : _om --> ( _om X. A ) /\ i e. _om ) -> ( h ` i ) e. ( _om X. A ) )
88 eleq1 
 |-  ( ( h ` i ) = <. i , z >. -> ( ( h ` i ) e. ( _om X. A ) <-> <. i , z >. e. ( _om X. A ) ) )
89 opelxp2 
 |-  ( <. i , z >. e. ( _om X. A ) -> z e. A )
90 88 89 biimtrdi 
 |-  ( ( h ` i ) = <. i , z >. -> ( ( h ` i ) e. ( _om X. A ) -> z e. A ) )
91 87 90 mpan9 
 |-  ( ( ( h : _om --> ( _om X. A ) /\ i e. _om ) /\ ( h ` i ) = <. i , z >. ) -> z e. A )
92 suceq 
 |-  ( n = i -> suc n = suc i )
93 92 sneqd 
 |-  ( n = i -> { suc n } = { suc i } )
94 oveq1 
 |-  ( n = i -> ( n F x ) = ( i F x ) )
95 93 94 xpeq12d 
 |-  ( n = i -> ( { suc n } X. ( n F x ) ) = ( { suc i } X. ( i F x ) ) )
96 oveq2 
 |-  ( x = z -> ( i F x ) = ( i F z ) )
97 96 xpeq2d 
 |-  ( x = z -> ( { suc i } X. ( i F x ) ) = ( { suc i } X. ( i F z ) ) )
98 snex 
 |-  { suc i } e. _V
99 ovex 
 |-  ( i F z ) e. _V
100 98 99 xpex 
 |-  ( { suc i } X. ( i F z ) ) e. _V
101 95 97 2 100 ovmpo 
 |-  ( ( i e. _om /\ z e. A ) -> ( i G z ) = ( { suc i } X. ( i F z ) ) )
102 86 91 101 syl2anc 
 |-  ( ( ( h : _om --> ( _om X. A ) /\ i e. _om ) /\ ( h ` i ) = <. i , z >. ) -> ( i G z ) = ( { suc i } X. ( i F z ) ) )
103 85 102 eqtrd 
 |-  ( ( ( h : _om --> ( _om X. A ) /\ i e. _om ) /\ ( h ` i ) = <. i , z >. ) -> ( G ` ( h ` i ) ) = ( { suc i } X. ( i F z ) ) )
104 suceq 
 |-  ( k = i -> suc k = suc i )
105 104 fveq2d 
 |-  ( k = i -> ( h ` suc k ) = ( h ` suc i ) )
106 2fveq3 
 |-  ( k = i -> ( G ` ( h ` k ) ) = ( G ` ( h ` i ) ) )
107 105 106 eleq12d 
 |-  ( k = i -> ( ( h ` suc k ) e. ( G ` ( h ` k ) ) <-> ( h ` suc i ) e. ( G ` ( h ` i ) ) ) )
108 107 rspcv 
 |-  ( i e. _om -> ( A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) -> ( h ` suc i ) e. ( G ` ( h ` i ) ) ) )
109 108 ad2antlr 
 |-  ( ( ( 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 ) ) ) )
110 eleq2 
 |-  ( ( 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 ) ) ) )
111 elxp 
 |-  ( ( 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 ) ) ) )
112 velsn 
 |-  ( s e. { suc i } <-> s = suc i )
113 opeq1 
 |-  ( s = suc i -> <. s , t >. = <. suc i , t >. )
114 112 113 sylbi 
 |-  ( s e. { suc i } -> <. s , t >. = <. suc i , t >. )
115 114 eqeq2d 
 |-  ( s e. { suc i } -> ( ( h ` suc i ) = <. s , t >. <-> ( h ` suc i ) = <. suc i , t >. ) )
116 115 biimpac 
 |-  ( ( ( h ` suc i ) = <. s , t >. /\ s e. { suc i } ) -> ( h ` suc i ) = <. suc i , t >. )
117 116 adantrr 
 |-  ( ( ( h ` suc i ) = <. s , t >. /\ ( s e. { suc i } /\ t e. ( i F z ) ) ) -> ( h ` suc i ) = <. suc i , t >. )
118 117 eximi 
 |-  ( E. t ( ( h ` suc i ) = <. s , t >. /\ ( s e. { suc i } /\ t e. ( i F z ) ) ) -> E. t ( h ` suc i ) = <. suc i , t >. )
119 118 exlimiv 
 |-  ( 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 >. )
120 111 119 sylbi 
 |-  ( ( h ` suc i ) e. ( { suc i } X. ( i F z ) ) -> E. t ( h ` suc i ) = <. suc i , t >. )
121 110 120 biimtrdi 
 |-  ( ( G ` ( h ` i ) ) = ( { suc i } X. ( i F z ) ) -> ( ( h ` suc i ) e. ( G ` ( h ` i ) ) -> E. t ( h ` suc i ) = <. suc i , t >. ) )
122 103 109 121 sylsyld 
 |-  ( ( ( 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 >. ) )
123 122 expcom 
 |-  ( ( 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 >. ) ) )
124 123 exlimiv 
 |-  ( 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 >. ) ) )
125 124 com3l 
 |-  ( ( 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 >. ) ) )
126 opeq2 
 |-  ( t = z -> <. suc i , t >. = <. suc i , z >. )
127 126 eqeq2d 
 |-  ( t = z -> ( ( h ` suc i ) = <. suc i , t >. <-> ( h ` suc i ) = <. suc i , z >. ) )
128 127 cbvexvw 
 |-  ( E. t ( h ` suc i ) = <. suc i , t >. <-> E. z ( h ` suc i ) = <. suc i , z >. )
129 125 128 syl8ib 
 |-  ( ( 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 >. ) ) )
130 129 impancom 
 |-  ( ( 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 >. ) ) )
131 130 3adant2 
 |-  ( ( 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 >. ) ) )
132 131 adantl 
 |-  ( ( 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 >. ) ) )
133 132 com12 
 |-  ( 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 >. ) ) )
134 68 72 76 81 133 finds2 
 |-  ( 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 >. ) )
135 134 com12 
 |-  ( ( 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 >. ) )
136 135 ralrimiv 
 |-  ( ( 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 >. )
137 fveq2 
 |-  ( m = k -> ( h ` m ) = ( h ` k ) )
138 opeq1 
 |-  ( m = k -> <. m , z >. = <. k , z >. )
139 137 138 eqeq12d 
 |-  ( m = k -> ( ( h ` m ) = <. m , z >. <-> ( h ` k ) = <. k , z >. ) )
140 139 exbidv 
 |-  ( m = k -> ( E. z ( h ` m ) = <. m , z >. <-> E. z ( h ` k ) = <. k , z >. ) )
141 140 rspccv 
 |-  ( A. m e. _om E. z ( h ` m ) = <. m , z >. -> ( k e. _om -> E. z ( h ` k ) = <. k , z >. ) )
142 136 141 syl 
 |-  ( ( 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 >. ) )
143 142 3impia 
 |-  ( ( 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 >. )
144 simp21 
 |-  ( ( 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 ) )
145 simp3 
 |-  ( ( 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 )
146 rspa 
 |-  ( ( A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) /\ k e. _om ) -> ( h ` suc k ) e. ( G ` ( h ` k ) ) )
147 146 3ad2antl3 
 |-  ( ( ( 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 ) ) )
148 147 3adant1 
 |-  ( ( 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 ) ) )
149 simpl 
 |-  ( ( ( h ` k ) = <. k , z >. /\ ( h : _om --> ( _om X. A ) /\ k e. _om ) ) -> ( h ` k ) = <. k , z >. )
150 149 fveq2d 
 |-  ( ( ( h ` k ) = <. k , z >. /\ ( h : _om --> ( _om X. A ) /\ k e. _om ) ) -> ( G ` ( h ` k ) ) = ( G ` <. k , z >. ) )
151 simprr 
 |-  ( ( ( h ` k ) = <. k , z >. /\ ( h : _om --> ( _om X. A ) /\ k e. _om ) ) -> k e. _om )
152 eleq1 
 |-  ( ( h ` k ) = <. k , z >. -> ( ( h ` k ) e. ( _om X. A ) <-> <. k , z >. e. ( _om X. A ) ) )
153 opelxp2 
 |-  ( <. k , z >. e. ( _om X. A ) -> z e. A )
154 152 153 biimtrdi 
 |-  ( ( h ` k ) = <. k , z >. -> ( ( h ` k ) e. ( _om X. A ) -> z e. A ) )
155 ffvelcdm 
 |-  ( ( h : _om --> ( _om X. A ) /\ k e. _om ) -> ( h ` k ) e. ( _om X. A ) )
156 154 155 impel 
 |-  ( ( ( h ` k ) = <. k , z >. /\ ( h : _om --> ( _om X. A ) /\ k e. _om ) ) -> z e. A )
157 df-ov 
 |-  ( k G z ) = ( G ` <. k , z >. )
158 suceq 
 |-  ( n = k -> suc n = suc k )
159 158 sneqd 
 |-  ( n = k -> { suc n } = { suc k } )
160 oveq1 
 |-  ( n = k -> ( n F x ) = ( k F x ) )
161 159 160 xpeq12d 
 |-  ( n = k -> ( { suc n } X. ( n F x ) ) = ( { suc k } X. ( k F x ) ) )
162 oveq2 
 |-  ( x = z -> ( k F x ) = ( k F z ) )
163 162 xpeq2d 
 |-  ( x = z -> ( { suc k } X. ( k F x ) ) = ( { suc k } X. ( k F z ) ) )
164 snex 
 |-  { suc k } e. _V
165 ovex 
 |-  ( k F z ) e. _V
166 164 165 xpex 
 |-  ( { suc k } X. ( k F z ) ) e. _V
167 161 163 2 166 ovmpo 
 |-  ( ( k e. _om /\ z e. A ) -> ( k G z ) = ( { suc k } X. ( k F z ) ) )
168 157 167 eqtr3id 
 |-  ( ( k e. _om /\ z e. A ) -> ( G ` <. k , z >. ) = ( { suc k } X. ( k F z ) ) )
169 151 156 168 syl2anc 
 |-  ( ( ( h ` k ) = <. k , z >. /\ ( h : _om --> ( _om X. A ) /\ k e. _om ) ) -> ( G ` <. k , z >. ) = ( { suc k } X. ( k F z ) ) )
170 150 169 eqtrd 
 |-  ( ( ( h ` k ) = <. k , z >. /\ ( h : _om --> ( _om X. A ) /\ k e. _om ) ) -> ( G ` ( h ` k ) ) = ( { suc k } X. ( k F z ) ) )
171 170 eleq2d 
 |-  ( ( ( 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 ) ) ) )
172 elxp 
 |-  ( ( 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 ) ) ) )
173 peano2 
 |-  ( k e. _om -> suc k e. _om )
174 fvco3 
 |-  ( ( h : _om --> ( _om X. A ) /\ suc k e. _om ) -> ( ( 2nd o. h ) ` suc k ) = ( 2nd ` ( h ` suc k ) ) )
175 173 174 sylan2 
 |-  ( ( h : _om --> ( _om X. A ) /\ k e. _om ) -> ( ( 2nd o. h ) ` suc k ) = ( 2nd ` ( h ` suc k ) ) )
176 175 adantl 
 |-  ( ( ( ( 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 ) ) )
177 simpll 
 |-  ( ( ( ( h ` suc k ) = <. s , t >. /\ ( h ` k ) = <. k , z >. ) /\ ( h : _om --> ( _om X. A ) /\ k e. _om ) ) -> ( h ` suc k ) = <. s , t >. )
178 177 fveq2d 
 |-  ( ( ( ( h ` suc k ) = <. s , t >. /\ ( h ` k ) = <. k , z >. ) /\ ( h : _om --> ( _om X. A ) /\ k e. _om ) ) -> ( 2nd ` ( h ` suc k ) ) = ( 2nd ` <. s , t >. ) )
179 176 178 eqtrd 
 |-  ( ( ( ( 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 >. ) )
180 vex 
 |-  s e. _V
181 vex 
 |-  t e. _V
182 180 181 op2nd 
 |-  ( 2nd ` <. s , t >. ) = t
183 179 182 eqtrdi 
 |-  ( ( ( ( h ` suc k ) = <. s , t >. /\ ( h ` k ) = <. k , z >. ) /\ ( h : _om --> ( _om X. A ) /\ k e. _om ) ) -> ( ( 2nd o. h ) ` suc k ) = t )
184 fvco3 
 |-  ( ( h : _om --> ( _om X. A ) /\ k e. _om ) -> ( ( 2nd o. h ) ` k ) = ( 2nd ` ( h ` k ) ) )
185 184 adantl 
 |-  ( ( ( ( h ` suc k ) = <. s , t >. /\ ( h ` k ) = <. k , z >. ) /\ ( h : _om --> ( _om X. A ) /\ k e. _om ) ) -> ( ( 2nd o. h ) ` k ) = ( 2nd ` ( h ` k ) ) )
186 simplr 
 |-  ( ( ( ( h ` suc k ) = <. s , t >. /\ ( h ` k ) = <. k , z >. ) /\ ( h : _om --> ( _om X. A ) /\ k e. _om ) ) -> ( h ` k ) = <. k , z >. )
187 186 fveq2d 
 |-  ( ( ( ( h ` suc k ) = <. s , t >. /\ ( h ` k ) = <. k , z >. ) /\ ( h : _om --> ( _om X. A ) /\ k e. _om ) ) -> ( 2nd ` ( h ` k ) ) = ( 2nd ` <. k , z >. ) )
188 185 187 eqtrd 
 |-  ( ( ( ( h ` suc k ) = <. s , t >. /\ ( h ` k ) = <. k , z >. ) /\ ( h : _om --> ( _om X. A ) /\ k e. _om ) ) -> ( ( 2nd o. h ) ` k ) = ( 2nd ` <. k , z >. ) )
189 vex 
 |-  k e. _V
190 vex 
 |-  z e. _V
191 189 190 op2nd 
 |-  ( 2nd ` <. k , z >. ) = z
192 188 191 eqtrdi 
 |-  ( ( ( ( h ` suc k ) = <. s , t >. /\ ( h ` k ) = <. k , z >. ) /\ ( h : _om --> ( _om X. A ) /\ k e. _om ) ) -> ( ( 2nd o. h ) ` k ) = z )
193 192 oveq2d 
 |-  ( ( ( ( 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 ) )
194 183 193 eleq12d 
 |-  ( ( ( ( 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 ) ) )
195 194 biimprcd 
 |-  ( 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 ) ) ) )
196 195 exp4c 
 |-  ( 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 ) ) ) ) ) )
197 196 adantl 
 |-  ( ( 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 ) ) ) ) ) )
198 197 impcom 
 |-  ( ( ( 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 ) ) ) ) )
199 198 exlimivv 
 |-  ( 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 ) ) ) ) )
200 172 199 sylbi 
 |-  ( ( 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 ) ) ) ) )
201 200 com3l 
 |-  ( ( 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 ) ) ) ) )
202 201 imp 
 |-  ( ( ( 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 ) ) ) )
203 171 202 sylbid 
 |-  ( ( ( 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 ) ) ) )
204 203 ex 
 |-  ( ( 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 ) ) ) ) )
205 204 exlimiv 
 |-  ( 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 ) ) ) ) )
206 205 3imp 
 |-  ( ( 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 ) ) )
207 143 144 145 148 206 syl121anc 
 |-  ( ( 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 ) ) )
208 207 3expia 
 |-  ( ( 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 ) ) ) )
209 64 208 ralrimi 
 |-  ( ( 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 ) ) )
210 46 58 209 3jca 
 |-  ( ( 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 ) ) ) )
211 feq1 
 |-  ( g = ( 2nd o. h ) -> ( g : _om --> A <-> ( 2nd o. h ) : _om --> A ) )
212 fveq1 
 |-  ( g = ( 2nd o. h ) -> ( g ` (/) ) = ( ( 2nd o. h ) ` (/) ) )
213 212 eqeq1d 
 |-  ( g = ( 2nd o. h ) -> ( ( g ` (/) ) = C <-> ( ( 2nd o. h ) ` (/) ) = C ) )
214 fveq1 
 |-  ( g = ( 2nd o. h ) -> ( g ` suc k ) = ( ( 2nd o. h ) ` suc k ) )
215 fveq1 
 |-  ( g = ( 2nd o. h ) -> ( g ` k ) = ( ( 2nd o. h ) ` k ) )
216 215 oveq2d 
 |-  ( g = ( 2nd o. h ) -> ( k F ( g ` k ) ) = ( k F ( ( 2nd o. h ) ` k ) ) )
217 214 216 eleq12d 
 |-  ( g = ( 2nd o. h ) -> ( ( g ` suc k ) e. ( k F ( g ` k ) ) <-> ( ( 2nd o. h ) ` suc k ) e. ( k F ( ( 2nd o. h ) ` k ) ) ) )
218 217 ralbidv 
 |-  ( 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 ) ) ) )
219 211 213 218 3anbi123d 
 |-  ( 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 ) ) ) ) )
220 49 210 219 spcedv 
 |-  ( ( 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 ) ) ) )
221 220 ex 
 |-  ( 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 ) ) ) ) )
222 221 exlimdv 
 |-  ( 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 ) ) ) ) )
223 222 adantr 
 |-  ( ( 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 ) ) ) ) )
224 43 223 mpd 
 |-  ( ( 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 ) ) ) )