Metamath Proof Explorer

Theorem axcclem

Description: Lemma for axcc . (Contributed by Mario Carneiro, 2-Feb-2013) (Revised by Mario Carneiro, 16-Nov-2013)

Ref Expression
Hypotheses axcclem.1 
|- A = ( x \ { (/) } )
axcclem.2 
|- F = ( n e. _om , y e. U. A |-> ( f ` n ) )
axcclem.3 
|- G = ( w e. A |-> ( h ` suc ( `' f ` w ) ) )
Assertion axcclem 
|- ( x ~~ _om -> E. g A. z e. x ( z =/= (/) -> ( g ` z ) e. z ) )

Proof

Step Hyp Ref Expression
1 axcclem.1 
 |-  A = ( x \ { (/) } )
2 axcclem.2 
 |-  F = ( n e. _om , y e. U. A |-> ( f ` n ) )
3 axcclem.3 
 |-  G = ( w e. A |-> ( h ` suc ( `' f ` w ) ) )
4 isfinite2 
 |-  ( A ~< _om -> A e. Fin )
5 1 eleq1i 
 |-  ( A e. Fin <-> ( x \ { (/) } ) e. Fin )
6 undif1 
 |-  ( ( x \ { (/) } ) u. { (/) } ) = ( x u. { (/) } )
7 snfi 
 |-  { (/) } e. Fin
8 unfi 
 |-  ( ( ( x \ { (/) } ) e. Fin /\ { (/) } e. Fin ) -> ( ( x \ { (/) } ) u. { (/) } ) e. Fin )
9 7 8 mpan2 
 |-  ( ( x \ { (/) } ) e. Fin -> ( ( x \ { (/) } ) u. { (/) } ) e. Fin )
10 6 9 eqeltrrid 
 |-  ( ( x \ { (/) } ) e. Fin -> ( x u. { (/) } ) e. Fin )
11 ssun1 
 |-  x C_ ( x u. { (/) } )
12 ssfi 
 |-  ( ( ( x u. { (/) } ) e. Fin /\ x C_ ( x u. { (/) } ) ) -> x e. Fin )
13 10 11 12 sylancl 
 |-  ( ( x \ { (/) } ) e. Fin -> x e. Fin )
14 5 13 sylbi 
 |-  ( A e. Fin -> x e. Fin )
15 dcomex 
 |-  _om e. _V
16 isfiniteg 
 |-  ( _om e. _V -> ( x e. Fin <-> x ~< _om ) )
17 15 16 ax-mp 
 |-  ( x e. Fin <-> x ~< _om )
18 sdomnen 
 |-  ( x ~< _om -> -. x ~~ _om )
19 17 18 sylbi 
 |-  ( x e. Fin -> -. x ~~ _om )
20 4 14 19 3syl 
 |-  ( A ~< _om -> -. x ~~ _om )
21 20 con2i 
 |-  ( x ~~ _om -> -. A ~< _om )
22 sdomentr 
 |-  ( ( A ~< x /\ x ~~ _om ) -> A ~< _om )
23 22 expcom 
 |-  ( x ~~ _om -> ( A ~< x -> A ~< _om ) )
24 21 23 mtod 
 |-  ( x ~~ _om -> -. A ~< x )
25 vex 
 |-  x e. _V
26 difss 
 |-  ( x \ { (/) } ) C_ x
27 1 26 eqsstri 
 |-  A C_ x
28 ssdomg 
 |-  ( x e. _V -> ( A C_ x -> A ~<_ x ) )
29 25 27 28 mp2 
 |-  A ~<_ x
30 24 29 jctil 
 |-  ( x ~~ _om -> ( A ~<_ x /\ -. A ~< x ) )
31 bren2 
 |-  ( A ~~ x <-> ( A ~<_ x /\ -. A ~< x ) )
32 30 31 sylibr 
 |-  ( x ~~ _om -> A ~~ x )
33 entr 
 |-  ( ( A ~~ x /\ x ~~ _om ) -> A ~~ _om )
34 32 33 mpancom 
 |-  ( x ~~ _om -> A ~~ _om )
35 ensym 
 |-  ( A ~~ _om -> _om ~~ A )
36 bren 
 |-  ( _om ~~ A <-> E. f f : _om -1-1-onto-> A )
37 f1of 
 |-  ( f : _om -1-1-onto-> A -> f : _om --> A )
38 peano1 
 |-  (/) e. _om
39 ffvelcdm 
 |-  ( ( f : _om --> A /\ (/) e. _om ) -> ( f ` (/) ) e. A )
40 37 38 39 sylancl 
 |-  ( f : _om -1-1-onto-> A -> ( f ` (/) ) e. A )
41 eldifn 
 |-  ( ( f ` (/) ) e. ( x \ { (/) } ) -> -. ( f ` (/) ) e. { (/) } )
42 41 1 eleq2s 
 |-  ( ( f ` (/) ) e. A -> -. ( f ` (/) ) e. { (/) } )
43 fvex 
 |-  ( f ` (/) ) e. _V
44 43 elsn 
 |-  ( ( f ` (/) ) e. { (/) } <-> ( f ` (/) ) = (/) )
45 44 notbii 
 |-  ( -. ( f ` (/) ) e. { (/) } <-> -. ( f ` (/) ) = (/) )
46 neq0 
 |-  ( -. ( f ` (/) ) = (/) <-> E. c c e. ( f ` (/) ) )
47 45 46 bitr2i 
 |-  ( E. c c e. ( f ` (/) ) <-> -. ( f ` (/) ) e. { (/) } )
48 42 47 sylibr 
 |-  ( ( f ` (/) ) e. A -> E. c c e. ( f ` (/) ) )
49 40 48 syl 
 |-  ( f : _om -1-1-onto-> A -> E. c c e. ( f ` (/) ) )
50 elunii 
 |-  ( ( c e. ( f ` (/) ) /\ ( f ` (/) ) e. A ) -> c e. U. A )
51 40 50 sylan2 
 |-  ( ( c e. ( f ` (/) ) /\ f : _om -1-1-onto-> A ) -> c e. U. A )
52 37 ffvelcdmda 
 |-  ( ( f : _om -1-1-onto-> A /\ n e. _om ) -> ( f ` n ) e. A )
53 difabs 
 |-  ( ( x \ { (/) } ) \ { (/) } ) = ( x \ { (/) } )
54 1 difeq1i 
 |-  ( A \ { (/) } ) = ( ( x \ { (/) } ) \ { (/) } )
55 53 54 1 3eqtr4i 
 |-  ( A \ { (/) } ) = A
56 pwuni 
 |-  A C_ ~P U. A
57 ssdif 
 |-  ( A C_ ~P U. A -> ( A \ { (/) } ) C_ ( ~P U. A \ { (/) } ) )
58 56 57 ax-mp 
 |-  ( A \ { (/) } ) C_ ( ~P U. A \ { (/) } )
59 55 58 eqsstrri 
 |-  A C_ ( ~P U. A \ { (/) } )
60 59 sseli 
 |-  ( ( f ` n ) e. A -> ( f ` n ) e. ( ~P U. A \ { (/) } ) )
61 60 ralrimivw 
 |-  ( ( f ` n ) e. A -> A. y e. U. A ( f ` n ) e. ( ~P U. A \ { (/) } ) )
62 52 61 syl 
 |-  ( ( f : _om -1-1-onto-> A /\ n e. _om ) -> A. y e. U. A ( f ` n ) e. ( ~P U. A \ { (/) } ) )
63 62 ralrimiva 
 |-  ( f : _om -1-1-onto-> A -> A. n e. _om A. y e. U. A ( f ` n ) e. ( ~P U. A \ { (/) } ) )
64 2 fmpo 
 |-  ( A. n e. _om A. y e. U. A ( f ` n ) e. ( ~P U. A \ { (/) } ) <-> F : ( _om X. U. A ) --> ( ~P U. A \ { (/) } ) )
65 63 64 sylib 
 |-  ( f : _om -1-1-onto-> A -> F : ( _om X. U. A ) --> ( ~P U. A \ { (/) } ) )
66 65 adantl 
 |-  ( ( c e. ( f ` (/) ) /\ f : _om -1-1-onto-> A ) -> F : ( _om X. U. A ) --> ( ~P U. A \ { (/) } ) )
67 25 difexi 
 |-  ( x \ { (/) } ) e. _V
68 1 67 eqeltri 
 |-  A e. _V
69 68 uniex 
 |-  U. A e. _V
70 69 axdc4 
 |-  ( ( c e. U. A /\ F : ( _om X. U. A ) --> ( ~P U. A \ { (/) } ) ) -> E. h ( h : _om --> U. A /\ ( h ` (/) ) = c /\ A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) ) )
71 51 66 70 syl2anc 
 |-  ( ( c e. ( f ` (/) ) /\ f : _om -1-1-onto-> A ) -> E. h ( h : _om --> U. A /\ ( h ` (/) ) = c /\ A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) ) )
72 3simpb 
 |-  ( ( h : _om --> U. A /\ ( h ` (/) ) = c /\ A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) ) -> ( h : _om --> U. A /\ A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) ) )
73 72 eximi 
 |-  ( E. h ( h : _om --> U. A /\ ( h ` (/) ) = c /\ A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) ) -> E. h ( h : _om --> U. A /\ A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) ) )
74 71 73 syl 
 |-  ( ( c e. ( f ` (/) ) /\ f : _om -1-1-onto-> A ) -> E. h ( h : _om --> U. A /\ A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) ) )
75 74 ex 
 |-  ( c e. ( f ` (/) ) -> ( f : _om -1-1-onto-> A -> E. h ( h : _om --> U. A /\ A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) ) ) )
76 75 exlimiv 
 |-  ( E. c c e. ( f ` (/) ) -> ( f : _om -1-1-onto-> A -> E. h ( h : _om --> U. A /\ A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) ) ) )
77 49 76 mpcom 
 |-  ( f : _om -1-1-onto-> A -> E. h ( h : _om --> U. A /\ A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) ) )
78 velsn 
 |-  ( z e. { (/) } <-> z = (/) )
79 78 necon3bbii 
 |-  ( -. z e. { (/) } <-> z =/= (/) )
80 1 eleq2i 
 |-  ( z e. A <-> z e. ( x \ { (/) } ) )
81 eldif 
 |-  ( z e. ( x \ { (/) } ) <-> ( z e. x /\ -. z e. { (/) } ) )
82 80 81 sylbbr 
 |-  ( ( z e. x /\ -. z e. { (/) } ) -> z e. A )
83 79 82 sylan2br 
 |-  ( ( z e. x /\ z =/= (/) ) -> z e. A )
84 simpl 
 |-  ( ( f : _om -1-1-onto-> A /\ z e. A ) -> f : _om -1-1-onto-> A )
85 f1ofo 
 |-  ( f : _om -1-1-onto-> A -> f : _om -onto-> A )
86 foelrn 
 |-  ( ( f : _om -onto-> A /\ z e. A ) -> E. i e. _om z = ( f ` i ) )
87 85 86 sylan 
 |-  ( ( f : _om -1-1-onto-> A /\ z e. A ) -> E. i e. _om z = ( f ` i ) )
88 suceq 
 |-  ( k = i -> suc k = suc i )
89 88 fveq2d 
 |-  ( k = i -> ( h ` suc k ) = ( h ` suc i ) )
90 id 
 |-  ( k = i -> k = i )
91 fveq2 
 |-  ( k = i -> ( h ` k ) = ( h ` i ) )
92 90 91 oveq12d 
 |-  ( k = i -> ( k F ( h ` k ) ) = ( i F ( h ` i ) ) )
93 89 92 eleq12d 
 |-  ( k = i -> ( ( h ` suc k ) e. ( k F ( h ` k ) ) <-> ( h ` suc i ) e. ( i F ( h ` i ) ) ) )
94 93 rspcv 
 |-  ( i e. _om -> ( A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) -> ( h ` suc i ) e. ( i F ( h ` i ) ) ) )
95 94 3ad2ant3 
 |-  ( ( h : _om --> U. A /\ f : _om -1-1-onto-> A /\ i e. _om ) -> ( A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) -> ( h ` suc i ) e. ( i F ( h ` i ) ) ) )
96 95 imp 
 |-  ( ( ( h : _om --> U. A /\ f : _om -1-1-onto-> A /\ i e. _om ) /\ A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) ) -> ( h ` suc i ) e. ( i F ( h ` i ) ) )
97 96 3adant3 
 |-  ( ( ( h : _om --> U. A /\ f : _om -1-1-onto-> A /\ i e. _om ) /\ A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) /\ z = ( f ` i ) ) -> ( h ` suc i ) e. ( i F ( h ` i ) ) )
98 eqcom 
 |-  ( z = ( f ` i ) <-> ( f ` i ) = z )
99 f1ocnvfv 
 |-  ( ( f : _om -1-1-onto-> A /\ i e. _om ) -> ( ( f ` i ) = z -> ( `' f ` z ) = i ) )
100 98 99 biimtrid 
 |-  ( ( f : _om -1-1-onto-> A /\ i e. _om ) -> ( z = ( f ` i ) -> ( `' f ` z ) = i ) )
101 100 3adant1 
 |-  ( ( h : _om --> U. A /\ f : _om -1-1-onto-> A /\ i e. _om ) -> ( z = ( f ` i ) -> ( `' f ` z ) = i ) )
102 101 imp 
 |-  ( ( ( h : _om --> U. A /\ f : _om -1-1-onto-> A /\ i e. _om ) /\ z = ( f ` i ) ) -> ( `' f ` z ) = i )
103 102 eqcomd 
 |-  ( ( ( h : _om --> U. A /\ f : _om -1-1-onto-> A /\ i e. _om ) /\ z = ( f ` i ) ) -> i = ( `' f ` z ) )
104 103 3adant2 
 |-  ( ( ( h : _om --> U. A /\ f : _om -1-1-onto-> A /\ i e. _om ) /\ A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) /\ z = ( f ` i ) ) -> i = ( `' f ` z ) )
105 suceq 
 |-  ( i = ( `' f ` z ) -> suc i = suc ( `' f ` z ) )
106 104 105 syl 
 |-  ( ( ( h : _om --> U. A /\ f : _om -1-1-onto-> A /\ i e. _om ) /\ A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) /\ z = ( f ` i ) ) -> suc i = suc ( `' f ` z ) )
107 106 fveq2d 
 |-  ( ( ( h : _om --> U. A /\ f : _om -1-1-onto-> A /\ i e. _om ) /\ A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) /\ z = ( f ` i ) ) -> ( h ` suc i ) = ( h ` suc ( `' f ` z ) ) )
108 simpr 
 |-  ( ( h : _om --> U. A /\ i e. _om ) -> i e. _om )
109 ffvelcdm 
 |-  ( ( h : _om --> U. A /\ i e. _om ) -> ( h ` i ) e. U. A )
110 fveq2 
 |-  ( n = i -> ( f ` n ) = ( f ` i ) )
111 eqidd 
 |-  ( y = ( h ` i ) -> ( f ` i ) = ( f ` i ) )
112 fvex 
 |-  ( f ` i ) e. _V
113 110 111 2 112 ovmpo 
 |-  ( ( i e. _om /\ ( h ` i ) e. U. A ) -> ( i F ( h ` i ) ) = ( f ` i ) )
114 108 109 113 syl2anc 
 |-  ( ( h : _om --> U. A /\ i e. _om ) -> ( i F ( h ` i ) ) = ( f ` i ) )
115 114 3adant2 
 |-  ( ( h : _om --> U. A /\ f : _om -1-1-onto-> A /\ i e. _om ) -> ( i F ( h ` i ) ) = ( f ` i ) )
116 115 3ad2ant1 
 |-  ( ( ( h : _om --> U. A /\ f : _om -1-1-onto-> A /\ i e. _om ) /\ A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) /\ z = ( f ` i ) ) -> ( i F ( h ` i ) ) = ( f ` i ) )
117 97 107 116 3eltr3d 
 |-  ( ( ( h : _om --> U. A /\ f : _om -1-1-onto-> A /\ i e. _om ) /\ A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) /\ z = ( f ` i ) ) -> ( h ` suc ( `' f ` z ) ) e. ( f ` i ) )
118 37 ffvelcdmda 
 |-  ( ( f : _om -1-1-onto-> A /\ i e. _om ) -> ( f ` i ) e. A )
119 118 3adant1 
 |-  ( ( h : _om --> U. A /\ f : _om -1-1-onto-> A /\ i e. _om ) -> ( f ` i ) e. A )
120 119 3ad2ant1 
 |-  ( ( ( h : _om --> U. A /\ f : _om -1-1-onto-> A /\ i e. _om ) /\ A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) /\ z = ( f ` i ) ) -> ( f ` i ) e. A )
121 eleq1 
 |-  ( z = ( f ` i ) -> ( z e. A <-> ( f ` i ) e. A ) )
122 121 3ad2ant3 
 |-  ( ( ( h : _om --> U. A /\ f : _om -1-1-onto-> A /\ i e. _om ) /\ A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) /\ z = ( f ` i ) ) -> ( z e. A <-> ( f ` i ) e. A ) )
123 120 122 mpbird 
 |-  ( ( ( h : _om --> U. A /\ f : _om -1-1-onto-> A /\ i e. _om ) /\ A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) /\ z = ( f ` i ) ) -> z e. A )
124 fveq2 
 |-  ( w = z -> ( `' f ` w ) = ( `' f ` z ) )
125 suceq 
 |-  ( ( `' f ` w ) = ( `' f ` z ) -> suc ( `' f ` w ) = suc ( `' f ` z ) )
126 124 125 syl 
 |-  ( w = z -> suc ( `' f ` w ) = suc ( `' f ` z ) )
127 126 fveq2d 
 |-  ( w = z -> ( h ` suc ( `' f ` w ) ) = ( h ` suc ( `' f ` z ) ) )
128 fvex 
 |-  ( h ` suc ( `' f ` z ) ) e. _V
129 127 3 128 fvmpt 
 |-  ( z e. A -> ( G ` z ) = ( h ` suc ( `' f ` z ) ) )
130 123 129 syl 
 |-  ( ( ( h : _om --> U. A /\ f : _om -1-1-onto-> A /\ i e. _om ) /\ A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) /\ z = ( f ` i ) ) -> ( G ` z ) = ( h ` suc ( `' f ` z ) ) )
131 simp3 
 |-  ( ( ( h : _om --> U. A /\ f : _om -1-1-onto-> A /\ i e. _om ) /\ A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) /\ z = ( f ` i ) ) -> z = ( f ` i ) )
132 117 130 131 3eltr4d 
 |-  ( ( ( h : _om --> U. A /\ f : _om -1-1-onto-> A /\ i e. _om ) /\ A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) /\ z = ( f ` i ) ) -> ( G ` z ) e. z )
133 132 3exp 
 |-  ( ( h : _om --> U. A /\ f : _om -1-1-onto-> A /\ i e. _om ) -> ( A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) -> ( z = ( f ` i ) -> ( G ` z ) e. z ) ) )
134 133 com3r 
 |-  ( z = ( f ` i ) -> ( ( h : _om --> U. A /\ f : _om -1-1-onto-> A /\ i e. _om ) -> ( A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) -> ( G ` z ) e. z ) ) )
135 134 3expd 
 |-  ( z = ( f ` i ) -> ( h : _om --> U. A -> ( f : _om -1-1-onto-> A -> ( i e. _om -> ( A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) -> ( G ` z ) e. z ) ) ) ) )
136 135 com4r 
 |-  ( i e. _om -> ( z = ( f ` i ) -> ( h : _om --> U. A -> ( f : _om -1-1-onto-> A -> ( A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) -> ( G ` z ) e. z ) ) ) ) )
137 136 rexlimiv 
 |-  ( E. i e. _om z = ( f ` i ) -> ( h : _om --> U. A -> ( f : _om -1-1-onto-> A -> ( A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) -> ( G ` z ) e. z ) ) ) )
138 87 137 syl 
 |-  ( ( f : _om -1-1-onto-> A /\ z e. A ) -> ( h : _om --> U. A -> ( f : _om -1-1-onto-> A -> ( A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) -> ( G ` z ) e. z ) ) ) )
139 84 138 mpid 
 |-  ( ( f : _om -1-1-onto-> A /\ z e. A ) -> ( h : _om --> U. A -> ( A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) -> ( G ` z ) e. z ) ) )
140 139 impd 
 |-  ( ( f : _om -1-1-onto-> A /\ z e. A ) -> ( ( h : _om --> U. A /\ A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) ) -> ( G ` z ) e. z ) )
141 140 impancom 
 |-  ( ( f : _om -1-1-onto-> A /\ ( h : _om --> U. A /\ A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) ) ) -> ( z e. A -> ( G ` z ) e. z ) )
142 83 141 syl5 
 |-  ( ( f : _om -1-1-onto-> A /\ ( h : _om --> U. A /\ A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) ) ) -> ( ( z e. x /\ z =/= (/) ) -> ( G ` z ) e. z ) )
143 142 expd 
 |-  ( ( f : _om -1-1-onto-> A /\ ( h : _om --> U. A /\ A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) ) ) -> ( z e. x -> ( z =/= (/) -> ( G ` z ) e. z ) ) )
144 143 ralrimiv 
 |-  ( ( f : _om -1-1-onto-> A /\ ( h : _om --> U. A /\ A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) ) ) -> A. z e. x ( z =/= (/) -> ( G ` z ) e. z ) )
145 fvrn0 
 |-  ( h ` suc ( `' f ` w ) ) e. ( ran h u. { (/) } )
146 145 rgenw 
 |-  A. w e. A ( h ` suc ( `' f ` w ) ) e. ( ran h u. { (/) } )
147 eqid 
 |-  ( w e. A |-> ( h ` suc ( `' f ` w ) ) ) = ( w e. A |-> ( h ` suc ( `' f ` w ) ) )
148 147 fmpt 
 |-  ( A. w e. A ( h ` suc ( `' f ` w ) ) e. ( ran h u. { (/) } ) <-> ( w e. A |-> ( h ` suc ( `' f ` w ) ) ) : A --> ( ran h u. { (/) } ) )
149 146 148 mpbi 
 |-  ( w e. A |-> ( h ` suc ( `' f ` w ) ) ) : A --> ( ran h u. { (/) } )
150 vex 
 |-  h e. _V
151 150 rnex 
 |-  ran h e. _V
152 p0ex 
 |-  { (/) } e. _V
153 151 152 unex 
 |-  ( ran h u. { (/) } ) e. _V
154 fex2 
 |-  ( ( ( w e. A |-> ( h ` suc ( `' f ` w ) ) ) : A --> ( ran h u. { (/) } ) /\ A e. _V /\ ( ran h u. { (/) } ) e. _V ) -> ( w e. A |-> ( h ` suc ( `' f ` w ) ) ) e. _V )
155 149 68 153 154 mp3an 
 |-  ( w e. A |-> ( h ` suc ( `' f ` w ) ) ) e. _V
156 3 155 eqeltri 
 |-  G e. _V
157 fveq1 
 |-  ( g = G -> ( g ` z ) = ( G ` z ) )
158 157 eleq1d 
 |-  ( g = G -> ( ( g ` z ) e. z <-> ( G ` z ) e. z ) )
159 158 imbi2d 
 |-  ( g = G -> ( ( z =/= (/) -> ( g ` z ) e. z ) <-> ( z =/= (/) -> ( G ` z ) e. z ) ) )
160 159 ralbidv 
 |-  ( g = G -> ( A. z e. x ( z =/= (/) -> ( g ` z ) e. z ) <-> A. z e. x ( z =/= (/) -> ( G ` z ) e. z ) ) )
161 156 160 spcev 
 |-  ( A. z e. x ( z =/= (/) -> ( G ` z ) e. z ) -> E. g A. z e. x ( z =/= (/) -> ( g ` z ) e. z ) )
162 144 161 syl 
 |-  ( ( f : _om -1-1-onto-> A /\ ( h : _om --> U. A /\ A. k e. _om ( h ` suc k ) e. ( k F ( h ` k ) ) ) ) -> E. g A. z e. x ( z =/= (/) -> ( g ` z ) e. z ) )
163 77 162 exlimddv 
 |-  ( f : _om -1-1-onto-> A -> E. g A. z e. x ( z =/= (/) -> ( g ` z ) e. z ) )
164 163 exlimiv 
 |-  ( E. f f : _om -1-1-onto-> A -> E. g A. z e. x ( z =/= (/) -> ( g ` z ) e. z ) )
165 36 164 sylbi 
 |-  ( _om ~~ A -> E. g A. z e. x ( z =/= (/) -> ( g ` z ) e. z ) )
166 34 35 165 3syl 
 |-  ( x ~~ _om -> E. g A. z e. x ( z =/= (/) -> ( g ` z ) e. z ) )