Metamath Proof Explorer

Theorem axdc3lem2

Description: Lemma for axdc3 . We have constructed a "candidate set" S , which consists of all finite sequences s that satisfy our property of interest, namely s ( x + 1 ) e. F ( s ( x ) ) on its domain, but with the added constraint that s ( 0 ) = C . These sets are possible "initial segments" of theinfinite sequence satisfying these constraints, but we can leverage the standard ax-dc (with no initial condition) to select a sequence of ever-lengthening finite sequences, namely ( hn ) : m --> A (for some integer m ). We let our "choice" function select a sequence whose domain is one more than the last one, and agrees with the previous one on its domain. Thus, the application of vanilla ax-dc yields a sequence of sequences whose domains increase without bound, and whose union is a function which has all the properties we want. In this lemma, we show that given the sequence h , we can construct the sequence g that we are after. (Contributed by Mario Carneiro, 30-Jan-2013)

Ref Expression
Hypotheses axdc3lem2.1 
|- A e. _V
axdc3lem2.2 
|- S = { s | E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) }
axdc3lem2.3 
|- G = ( x e. S |-> { y e. S | ( dom y = suc dom x /\ ( y |` dom x ) = x ) } )
Assertion axdc3lem2 
|- ( E. h ( h : _om --> S /\ 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. ( F ` ( g ` k ) ) ) )

Proof

Step Hyp Ref Expression
1 axdc3lem2.1 
 |-  A e. _V
2 axdc3lem2.2 
 |-  S = { s | E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) }
3 axdc3lem2.3 
 |-  G = ( x e. S |-> { y e. S | ( dom y = suc dom x /\ ( y |` dom x ) = x ) } )
4 id 
 |-  ( m = (/) -> m = (/) )
5 fveq2 
 |-  ( m = (/) -> ( h ` m ) = ( h ` (/) ) )
6 5 dmeqd 
 |-  ( m = (/) -> dom ( h ` m ) = dom ( h ` (/) ) )
7 4 6 eleq12d 
 |-  ( m = (/) -> ( m e. dom ( h ` m ) <-> (/) e. dom ( h ` (/) ) ) )
8 eleq2 
 |-  ( m = (/) -> ( j e. m <-> j e. (/) ) )
9 5 sseq2d 
 |-  ( m = (/) -> ( ( h ` j ) C_ ( h ` m ) <-> ( h ` j ) C_ ( h ` (/) ) ) )
10 8 9 imbi12d 
 |-  ( m = (/) -> ( ( j e. m -> ( h ` j ) C_ ( h ` m ) ) <-> ( j e. (/) -> ( h ` j ) C_ ( h ` (/) ) ) ) )
11 7 10 anbi12d 
 |-  ( m = (/) -> ( ( m e. dom ( h ` m ) /\ ( j e. m -> ( h ` j ) C_ ( h ` m ) ) ) <-> ( (/) e. dom ( h ` (/) ) /\ ( j e. (/) -> ( h ` j ) C_ ( h ` (/) ) ) ) ) )
12 id 
 |-  ( m = i -> m = i )
13 fveq2 
 |-  ( m = i -> ( h ` m ) = ( h ` i ) )
14 13 dmeqd 
 |-  ( m = i -> dom ( h ` m ) = dom ( h ` i ) )
15 12 14 eleq12d 
 |-  ( m = i -> ( m e. dom ( h ` m ) <-> i e. dom ( h ` i ) ) )
16 elequ2 
 |-  ( m = i -> ( j e. m <-> j e. i ) )
17 13 sseq2d 
 |-  ( m = i -> ( ( h ` j ) C_ ( h ` m ) <-> ( h ` j ) C_ ( h ` i ) ) )
18 16 17 imbi12d 
 |-  ( m = i -> ( ( j e. m -> ( h ` j ) C_ ( h ` m ) ) <-> ( j e. i -> ( h ` j ) C_ ( h ` i ) ) ) )
19 15 18 anbi12d 
 |-  ( m = i -> ( ( m e. dom ( h ` m ) /\ ( j e. m -> ( h ` j ) C_ ( h ` m ) ) ) <-> ( i e. dom ( h ` i ) /\ ( j e. i -> ( h ` j ) C_ ( h ` i ) ) ) ) )
20 id 
 |-  ( m = suc i -> m = suc i )
21 fveq2 
 |-  ( m = suc i -> ( h ` m ) = ( h ` suc i ) )
22 21 dmeqd 
 |-  ( m = suc i -> dom ( h ` m ) = dom ( h ` suc i ) )
23 20 22 eleq12d 
 |-  ( m = suc i -> ( m e. dom ( h ` m ) <-> suc i e. dom ( h ` suc i ) ) )
24 eleq2 
 |-  ( m = suc i -> ( j e. m <-> j e. suc i ) )
25 21 sseq2d 
 |-  ( m = suc i -> ( ( h ` j ) C_ ( h ` m ) <-> ( h ` j ) C_ ( h ` suc i ) ) )
26 24 25 imbi12d 
 |-  ( m = suc i -> ( ( j e. m -> ( h ` j ) C_ ( h ` m ) ) <-> ( j e. suc i -> ( h ` j ) C_ ( h ` suc i ) ) ) )
27 23 26 anbi12d 
 |-  ( m = suc i -> ( ( m e. dom ( h ` m ) /\ ( j e. m -> ( h ` j ) C_ ( h ` m ) ) ) <-> ( suc i e. dom ( h ` suc i ) /\ ( j e. suc i -> ( h ` j ) C_ ( h ` suc i ) ) ) ) )
28 peano1 
 |-  (/) e. _om
29 ffvelcdm 
 |-  ( ( h : _om --> S /\ (/) e. _om ) -> ( h ` (/) ) e. S )
30 28 29 mpan2 
 |-  ( h : _om --> S -> ( h ` (/) ) e. S )
31 fdm 
 |-  ( s : suc n --> A -> dom s = suc n )
32 nnord 
 |-  ( n e. _om -> Ord n )
33 0elsuc 
 |-  ( Ord n -> (/) e. suc n )
34 32 33 syl 
 |-  ( n e. _om -> (/) e. suc n )
35 peano2 
 |-  ( n e. _om -> suc n e. _om )
36 eleq2 
 |-  ( dom s = suc n -> ( (/) e. dom s <-> (/) e. suc n ) )
37 eleq1 
 |-  ( dom s = suc n -> ( dom s e. _om <-> suc n e. _om ) )
38 36 37 anbi12d 
 |-  ( dom s = suc n -> ( ( (/) e. dom s /\ dom s e. _om ) <-> ( (/) e. suc n /\ suc n e. _om ) ) )
39 38 biimprcd 
 |-  ( ( (/) e. suc n /\ suc n e. _om ) -> ( dom s = suc n -> ( (/) e. dom s /\ dom s e. _om ) ) )
40 34 35 39 syl2anc 
 |-  ( n e. _om -> ( dom s = suc n -> ( (/) e. dom s /\ dom s e. _om ) ) )
41 31 40 syl5com 
 |-  ( s : suc n --> A -> ( n e. _om -> ( (/) e. dom s /\ dom s e. _om ) ) )
42 41 3ad2ant1 
 |-  ( ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) -> ( n e. _om -> ( (/) e. dom s /\ dom s e. _om ) ) )
43 42 impcom 
 |-  ( ( n e. _om /\ ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) ) -> ( (/) e. dom s /\ dom s e. _om ) )
44 43 rexlimiva 
 |-  ( E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) -> ( (/) e. dom s /\ dom s e. _om ) )
45 44 ss2abi 
 |-  { s | E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) } C_ { s | ( (/) e. dom s /\ dom s e. _om ) }
46 2 45 eqsstri 
 |-  S C_ { s | ( (/) e. dom s /\ dom s e. _om ) }
47 46 sseli 
 |-  ( ( h ` (/) ) e. S -> ( h ` (/) ) e. { s | ( (/) e. dom s /\ dom s e. _om ) } )
48 fvex 
 |-  ( h ` (/) ) e. _V
49 dmeq 
 |-  ( s = ( h ` (/) ) -> dom s = dom ( h ` (/) ) )
50 49 eleq2d 
 |-  ( s = ( h ` (/) ) -> ( (/) e. dom s <-> (/) e. dom ( h ` (/) ) ) )
51 49 eleq1d 
 |-  ( s = ( h ` (/) ) -> ( dom s e. _om <-> dom ( h ` (/) ) e. _om ) )
52 50 51 anbi12d 
 |-  ( s = ( h ` (/) ) -> ( ( (/) e. dom s /\ dom s e. _om ) <-> ( (/) e. dom ( h ` (/) ) /\ dom ( h ` (/) ) e. _om ) ) )
53 48 52 elab 
 |-  ( ( h ` (/) ) e. { s | ( (/) e. dom s /\ dom s e. _om ) } <-> ( (/) e. dom ( h ` (/) ) /\ dom ( h ` (/) ) e. _om ) )
54 47 53 sylib 
 |-  ( ( h ` (/) ) e. S -> ( (/) e. dom ( h ` (/) ) /\ dom ( h ` (/) ) e. _om ) )
55 54 simpld 
 |-  ( ( h ` (/) ) e. S -> (/) e. dom ( h ` (/) ) )
56 30 55 syl 
 |-  ( h : _om --> S -> (/) e. dom ( h ` (/) ) )
57 noel 
 |-  -. j e. (/)
58 57 pm2.21i 
 |-  ( j e. (/) -> ( h ` j ) C_ ( h ` (/) ) )
59 56 58 jctir 
 |-  ( h : _om --> S -> ( (/) e. dom ( h ` (/) ) /\ ( j e. (/) -> ( h ` j ) C_ ( h ` (/) ) ) ) )
60 59 adantr 
 |-  ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( (/) e. dom ( h ` (/) ) /\ ( j e. (/) -> ( h ` j ) C_ ( h ` (/) ) ) ) )
61 ffvelcdm 
 |-  ( ( h : _om --> S /\ i e. _om ) -> ( h ` i ) e. S )
62 61 ancoms 
 |-  ( ( i e. _om /\ h : _om --> S ) -> ( h ` i ) e. S )
63 62 adantrr 
 |-  ( ( i e. _om /\ ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) ) -> ( h ` i ) e. S )
64 suceq 
 |-  ( k = i -> suc k = suc i )
65 64 fveq2d 
 |-  ( k = i -> ( h ` suc k ) = ( h ` suc i ) )
66 2fveq3 
 |-  ( k = i -> ( G ` ( h ` k ) ) = ( G ` ( h ` i ) ) )
67 65 66 eleq12d 
 |-  ( k = i -> ( ( h ` suc k ) e. ( G ` ( h ` k ) ) <-> ( h ` suc i ) e. ( G ` ( h ` i ) ) ) )
68 67 rspcva 
 |-  ( ( i e. _om /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( h ` suc i ) e. ( G ` ( h ` i ) ) )
69 68 adantrl 
 |-  ( ( i e. _om /\ ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) ) -> ( h ` suc i ) e. ( G ` ( h ` i ) ) )
70 46 sseli 
 |-  ( ( h ` i ) e. S -> ( h ` i ) e. { s | ( (/) e. dom s /\ dom s e. _om ) } )
71 fvex 
 |-  ( h ` i ) e. _V
72 dmeq 
 |-  ( s = ( h ` i ) -> dom s = dom ( h ` i ) )
73 72 eleq2d 
 |-  ( s = ( h ` i ) -> ( (/) e. dom s <-> (/) e. dom ( h ` i ) ) )
74 72 eleq1d 
 |-  ( s = ( h ` i ) -> ( dom s e. _om <-> dom ( h ` i ) e. _om ) )
75 73 74 anbi12d 
 |-  ( s = ( h ` i ) -> ( ( (/) e. dom s /\ dom s e. _om ) <-> ( (/) e. dom ( h ` i ) /\ dom ( h ` i ) e. _om ) ) )
76 71 75 elab 
 |-  ( ( h ` i ) e. { s | ( (/) e. dom s /\ dom s e. _om ) } <-> ( (/) e. dom ( h ` i ) /\ dom ( h ` i ) e. _om ) )
77 70 76 sylib 
 |-  ( ( h ` i ) e. S -> ( (/) e. dom ( h ` i ) /\ dom ( h ` i ) e. _om ) )
78 77 simprd 
 |-  ( ( h ` i ) e. S -> dom ( h ` i ) e. _om )
79 nnord 
 |-  ( dom ( h ` i ) e. _om -> Ord dom ( h ` i ) )
80 ordsucelsuc 
 |-  ( Ord dom ( h ` i ) -> ( i e. dom ( h ` i ) <-> suc i e. suc dom ( h ` i ) ) )
81 78 79 80 3syl 
 |-  ( ( h ` i ) e. S -> ( i e. dom ( h ` i ) <-> suc i e. suc dom ( h ` i ) ) )
82 81 adantr 
 |-  ( ( ( h ` i ) e. S /\ ( h ` suc i ) e. ( G ` ( h ` i ) ) ) -> ( i e. dom ( h ` i ) <-> suc i e. suc dom ( h ` i ) ) )
83 dmeq 
 |-  ( x = ( h ` i ) -> dom x = dom ( h ` i ) )
84 suceq 
 |-  ( dom x = dom ( h ` i ) -> suc dom x = suc dom ( h ` i ) )
85 83 84 syl 
 |-  ( x = ( h ` i ) -> suc dom x = suc dom ( h ` i ) )
86 85 eqeq2d 
 |-  ( x = ( h ` i ) -> ( dom y = suc dom x <-> dom y = suc dom ( h ` i ) ) )
87 83 reseq2d 
 |-  ( x = ( h ` i ) -> ( y |` dom x ) = ( y |` dom ( h ` i ) ) )
88 id 
 |-  ( x = ( h ` i ) -> x = ( h ` i ) )
89 87 88 eqeq12d 
 |-  ( x = ( h ` i ) -> ( ( y |` dom x ) = x <-> ( y |` dom ( h ` i ) ) = ( h ` i ) ) )
90 86 89 anbi12d 
 |-  ( x = ( h ` i ) -> ( ( dom y = suc dom x /\ ( y |` dom x ) = x ) <-> ( dom y = suc dom ( h ` i ) /\ ( y |` dom ( h ` i ) ) = ( h ` i ) ) ) )
91 90 rabbidv 
 |-  ( x = ( h ` i ) -> { y e. S | ( dom y = suc dom x /\ ( y |` dom x ) = x ) } = { y e. S | ( dom y = suc dom ( h ` i ) /\ ( y |` dom ( h ` i ) ) = ( h ` i ) ) } )
92 1 2 axdc3lem 
 |-  S e. _V
93 92 rabex 
 |-  { y e. S | ( dom y = suc dom ( h ` i ) /\ ( y |` dom ( h ` i ) ) = ( h ` i ) ) } e. _V
94 91 3 93 fvmpt 
 |-  ( ( h ` i ) e. S -> ( G ` ( h ` i ) ) = { y e. S | ( dom y = suc dom ( h ` i ) /\ ( y |` dom ( h ` i ) ) = ( h ` i ) ) } )
95 94 eleq2d 
 |-  ( ( h ` i ) e. S -> ( ( h ` suc i ) e. ( G ` ( h ` i ) ) <-> ( h ` suc i ) e. { y e. S | ( dom y = suc dom ( h ` i ) /\ ( y |` dom ( h ` i ) ) = ( h ` i ) ) } ) )
96 dmeq 
 |-  ( y = ( h ` suc i ) -> dom y = dom ( h ` suc i ) )
97 96 eqeq1d 
 |-  ( y = ( h ` suc i ) -> ( dom y = suc dom ( h ` i ) <-> dom ( h ` suc i ) = suc dom ( h ` i ) ) )
98 reseq1 
 |-  ( y = ( h ` suc i ) -> ( y |` dom ( h ` i ) ) = ( ( h ` suc i ) |` dom ( h ` i ) ) )
99 98 eqeq1d 
 |-  ( y = ( h ` suc i ) -> ( ( y |` dom ( h ` i ) ) = ( h ` i ) <-> ( ( h ` suc i ) |` dom ( h ` i ) ) = ( h ` i ) ) )
100 97 99 anbi12d 
 |-  ( y = ( h ` suc i ) -> ( ( dom y = suc dom ( h ` i ) /\ ( y |` dom ( h ` i ) ) = ( h ` i ) ) <-> ( dom ( h ` suc i ) = suc dom ( h ` i ) /\ ( ( h ` suc i ) |` dom ( h ` i ) ) = ( h ` i ) ) ) )
101 100 elrab 
 |-  ( ( h ` suc i ) e. { y e. S | ( dom y = suc dom ( h ` i ) /\ ( y |` dom ( h ` i ) ) = ( h ` i ) ) } <-> ( ( h ` suc i ) e. S /\ ( dom ( h ` suc i ) = suc dom ( h ` i ) /\ ( ( h ` suc i ) |` dom ( h ` i ) ) = ( h ` i ) ) ) )
102 95 101 bitrdi 
 |-  ( ( h ` i ) e. S -> ( ( h ` suc i ) e. ( G ` ( h ` i ) ) <-> ( ( h ` suc i ) e. S /\ ( dom ( h ` suc i ) = suc dom ( h ` i ) /\ ( ( h ` suc i ) |` dom ( h ` i ) ) = ( h ` i ) ) ) ) )
103 102 simplbda 
 |-  ( ( ( h ` i ) e. S /\ ( h ` suc i ) e. ( G ` ( h ` i ) ) ) -> ( dom ( h ` suc i ) = suc dom ( h ` i ) /\ ( ( h ` suc i ) |` dom ( h ` i ) ) = ( h ` i ) ) )
104 103 simpld 
 |-  ( ( ( h ` i ) e. S /\ ( h ` suc i ) e. ( G ` ( h ` i ) ) ) -> dom ( h ` suc i ) = suc dom ( h ` i ) )
105 104 eleq2d 
 |-  ( ( ( h ` i ) e. S /\ ( h ` suc i ) e. ( G ` ( h ` i ) ) ) -> ( suc i e. dom ( h ` suc i ) <-> suc i e. suc dom ( h ` i ) ) )
106 82 105 bitr4d 
 |-  ( ( ( h ` i ) e. S /\ ( h ` suc i ) e. ( G ` ( h ` i ) ) ) -> ( i e. dom ( h ` i ) <-> suc i e. dom ( h ` suc i ) ) )
107 106 biimpd 
 |-  ( ( ( h ` i ) e. S /\ ( h ` suc i ) e. ( G ` ( h ` i ) ) ) -> ( i e. dom ( h ` i ) -> suc i e. dom ( h ` suc i ) ) )
108 103 simprd 
 |-  ( ( ( h ` i ) e. S /\ ( h ` suc i ) e. ( G ` ( h ` i ) ) ) -> ( ( h ` suc i ) |` dom ( h ` i ) ) = ( h ` i ) )
109 resss 
 |-  ( ( h ` suc i ) |` dom ( h ` i ) ) C_ ( h ` suc i )
110 sseq1 
 |-  ( ( ( h ` suc i ) |` dom ( h ` i ) ) = ( h ` i ) -> ( ( ( h ` suc i ) |` dom ( h ` i ) ) C_ ( h ` suc i ) <-> ( h ` i ) C_ ( h ` suc i ) ) )
111 109 110 mpbii 
 |-  ( ( ( h ` suc i ) |` dom ( h ` i ) ) = ( h ` i ) -> ( h ` i ) C_ ( h ` suc i ) )
112 elsuci 
 |-  ( j e. suc i -> ( j e. i \/ j = i ) )
113 pm2.27 
 |-  ( j e. i -> ( ( j e. i -> ( h ` j ) C_ ( h ` i ) ) -> ( h ` j ) C_ ( h ` i ) ) )
114 sstr2 
 |-  ( ( h ` j ) C_ ( h ` i ) -> ( ( h ` i ) C_ ( h ` suc i ) -> ( h ` j ) C_ ( h ` suc i ) ) )
115 113 114 syl6 
 |-  ( j e. i -> ( ( j e. i -> ( h ` j ) C_ ( h ` i ) ) -> ( ( h ` i ) C_ ( h ` suc i ) -> ( h ` j ) C_ ( h ` suc i ) ) ) )
116 fveq2 
 |-  ( j = i -> ( h ` j ) = ( h ` i ) )
117 116 sseq1d 
 |-  ( j = i -> ( ( h ` j ) C_ ( h ` suc i ) <-> ( h ` i ) C_ ( h ` suc i ) ) )
118 117 biimprd 
 |-  ( j = i -> ( ( h ` i ) C_ ( h ` suc i ) -> ( h ` j ) C_ ( h ` suc i ) ) )
119 118 a1d 
 |-  ( j = i -> ( ( j e. i -> ( h ` j ) C_ ( h ` i ) ) -> ( ( h ` i ) C_ ( h ` suc i ) -> ( h ` j ) C_ ( h ` suc i ) ) ) )
120 115 119 jaoi 
 |-  ( ( j e. i \/ j = i ) -> ( ( j e. i -> ( h ` j ) C_ ( h ` i ) ) -> ( ( h ` i ) C_ ( h ` suc i ) -> ( h ` j ) C_ ( h ` suc i ) ) ) )
121 112 120 syl 
 |-  ( j e. suc i -> ( ( j e. i -> ( h ` j ) C_ ( h ` i ) ) -> ( ( h ` i ) C_ ( h ` suc i ) -> ( h ` j ) C_ ( h ` suc i ) ) ) )
122 121 com13 
 |-  ( ( h ` i ) C_ ( h ` suc i ) -> ( ( j e. i -> ( h ` j ) C_ ( h ` i ) ) -> ( j e. suc i -> ( h ` j ) C_ ( h ` suc i ) ) ) )
123 108 111 122 3syl 
 |-  ( ( ( h ` i ) e. S /\ ( h ` suc i ) e. ( G ` ( h ` i ) ) ) -> ( ( j e. i -> ( h ` j ) C_ ( h ` i ) ) -> ( j e. suc i -> ( h ` j ) C_ ( h ` suc i ) ) ) )
124 107 123 anim12d 
 |-  ( ( ( h ` i ) e. S /\ ( h ` suc i ) e. ( G ` ( h ` i ) ) ) -> ( ( i e. dom ( h ` i ) /\ ( j e. i -> ( h ` j ) C_ ( h ` i ) ) ) -> ( suc i e. dom ( h ` suc i ) /\ ( j e. suc i -> ( h ` j ) C_ ( h ` suc i ) ) ) ) )
125 63 69 124 syl2anc 
 |-  ( ( i e. _om /\ ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) ) -> ( ( i e. dom ( h ` i ) /\ ( j e. i -> ( h ` j ) C_ ( h ` i ) ) ) -> ( suc i e. dom ( h ` suc i ) /\ ( j e. suc i -> ( h ` j ) C_ ( h ` suc i ) ) ) ) )
126 125 ex 
 |-  ( i e. _om -> ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( ( i e. dom ( h ` i ) /\ ( j e. i -> ( h ` j ) C_ ( h ` i ) ) ) -> ( suc i e. dom ( h ` suc i ) /\ ( j e. suc i -> ( h ` j ) C_ ( h ` suc i ) ) ) ) ) )
127 11 19 27 60 126 finds2 
 |-  ( m e. _om -> ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( m e. dom ( h ` m ) /\ ( j e. m -> ( h ` j ) C_ ( h ` m ) ) ) ) )
128 127 imp 
 |-  ( ( m e. _om /\ ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) ) -> ( m e. dom ( h ` m ) /\ ( j e. m -> ( h ` j ) C_ ( h ` m ) ) ) )
129 128 simprd 
 |-  ( ( m e. _om /\ ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) ) -> ( j e. m -> ( h ` j ) C_ ( h ` m ) ) )
130 129 expcom 
 |-  ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( m e. _om -> ( j e. m -> ( h ` j ) C_ ( h ` m ) ) ) )
131 130 ralrimdv 
 |-  ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( m e. _om -> A. j e. m ( h ` j ) C_ ( h ` m ) ) )
132 131 ralrimiv 
 |-  ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) )
133 frn 
 |-  ( h : _om --> S -> ran h C_ S )
134 ffun 
 |-  ( s : suc n --> A -> Fun s )
135 134 3ad2ant1 
 |-  ( ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) -> Fun s )
136 135 rexlimivw 
 |-  ( E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) -> Fun s )
137 136 ss2abi 
 |-  { s | E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) } C_ { s | Fun s }
138 2 137 eqsstri 
 |-  S C_ { s | Fun s }
139 133 138 sstrdi 
 |-  ( h : _om --> S -> ran h C_ { s | Fun s } )
140 139 sseld 
 |-  ( h : _om --> S -> ( u e. ran h -> u e. { s | Fun s } ) )
141 vex 
 |-  u e. _V
142 funeq 
 |-  ( s = u -> ( Fun s <-> Fun u ) )
143 141 142 elab 
 |-  ( u e. { s | Fun s } <-> Fun u )
144 140 143 imbitrdi 
 |-  ( h : _om --> S -> ( u e. ran h -> Fun u ) )
145 144 adantr 
 |-  ( ( h : _om --> S /\ A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) ) -> ( u e. ran h -> Fun u ) )
146 ffn 
 |-  ( h : _om --> S -> h Fn _om )
147 fvelrnb 
 |-  ( h Fn _om -> ( v e. ran h <-> E. b e. _om ( h ` b ) = v ) )
148 fvelrnb 
 |-  ( h Fn _om -> ( u e. ran h <-> E. a e. _om ( h ` a ) = u ) )
149 nnord 
 |-  ( a e. _om -> Ord a )
150 nnord 
 |-  ( b e. _om -> Ord b )
151 149 150 anim12i 
 |-  ( ( a e. _om /\ b e. _om ) -> ( Ord a /\ Ord b ) )
152 ordtri3or 
 |-  ( ( Ord a /\ Ord b ) -> ( a e. b \/ a = b \/ b e. a ) )
153 fveq2 
 |-  ( m = b -> ( h ` m ) = ( h ` b ) )
154 153 sseq2d 
 |-  ( m = b -> ( ( h ` j ) C_ ( h ` m ) <-> ( h ` j ) C_ ( h ` b ) ) )
155 154 raleqbi1dv 
 |-  ( m = b -> ( A. j e. m ( h ` j ) C_ ( h ` m ) <-> A. j e. b ( h ` j ) C_ ( h ` b ) ) )
156 155 rspcv 
 |-  ( b e. _om -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> A. j e. b ( h ` j ) C_ ( h ` b ) ) )
157 fveq2 
 |-  ( j = a -> ( h ` j ) = ( h ` a ) )
158 157 sseq1d 
 |-  ( j = a -> ( ( h ` j ) C_ ( h ` b ) <-> ( h ` a ) C_ ( h ` b ) ) )
159 158 rspccv 
 |-  ( A. j e. b ( h ` j ) C_ ( h ` b ) -> ( a e. b -> ( h ` a ) C_ ( h ` b ) ) )
160 156 159 syl6 
 |-  ( b e. _om -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( a e. b -> ( h ` a ) C_ ( h ` b ) ) ) )
161 160 adantl 
 |-  ( ( a e. _om /\ b e. _om ) -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( a e. b -> ( h ` a ) C_ ( h ` b ) ) ) )
162 161 3imp 
 |-  ( ( ( a e. _om /\ b e. _om ) /\ A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) /\ a e. b ) -> ( h ` a ) C_ ( h ` b ) )
163 162 orcd 
 |-  ( ( ( a e. _om /\ b e. _om ) /\ A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) /\ a e. b ) -> ( ( h ` a ) C_ ( h ` b ) \/ ( h ` b ) C_ ( h ` a ) ) )
164 163 3exp 
 |-  ( ( a e. _om /\ b e. _om ) -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( a e. b -> ( ( h ` a ) C_ ( h ` b ) \/ ( h ` b ) C_ ( h ` a ) ) ) ) )
165 164 com3r 
 |-  ( a e. b -> ( ( a e. _om /\ b e. _om ) -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( ( h ` a ) C_ ( h ` b ) \/ ( h ` b ) C_ ( h ` a ) ) ) ) )
166 fveq2 
 |-  ( a = b -> ( h ` a ) = ( h ` b ) )
167 eqimss 
 |-  ( ( h ` a ) = ( h ` b ) -> ( h ` a ) C_ ( h ` b ) )
168 167 orcd 
 |-  ( ( h ` a ) = ( h ` b ) -> ( ( h ` a ) C_ ( h ` b ) \/ ( h ` b ) C_ ( h ` a ) ) )
169 166 168 syl 
 |-  ( a = b -> ( ( h ` a ) C_ ( h ` b ) \/ ( h ` b ) C_ ( h ` a ) ) )
170 169 2a1d 
 |-  ( a = b -> ( ( a e. _om /\ b e. _om ) -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( ( h ` a ) C_ ( h ` b ) \/ ( h ` b ) C_ ( h ` a ) ) ) ) )
171 fveq2 
 |-  ( m = a -> ( h ` m ) = ( h ` a ) )
172 171 sseq2d 
 |-  ( m = a -> ( ( h ` j ) C_ ( h ` m ) <-> ( h ` j ) C_ ( h ` a ) ) )
173 172 raleqbi1dv 
 |-  ( m = a -> ( A. j e. m ( h ` j ) C_ ( h ` m ) <-> A. j e. a ( h ` j ) C_ ( h ` a ) ) )
174 173 rspcv 
 |-  ( a e. _om -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> A. j e. a ( h ` j ) C_ ( h ` a ) ) )
175 fveq2 
 |-  ( j = b -> ( h ` j ) = ( h ` b ) )
176 175 sseq1d 
 |-  ( j = b -> ( ( h ` j ) C_ ( h ` a ) <-> ( h ` b ) C_ ( h ` a ) ) )
177 176 rspccv 
 |-  ( A. j e. a ( h ` j ) C_ ( h ` a ) -> ( b e. a -> ( h ` b ) C_ ( h ` a ) ) )
178 174 177 syl6 
 |-  ( a e. _om -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( b e. a -> ( h ` b ) C_ ( h ` a ) ) ) )
179 178 adantr 
 |-  ( ( a e. _om /\ b e. _om ) -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( b e. a -> ( h ` b ) C_ ( h ` a ) ) ) )
180 179 3imp 
 |-  ( ( ( a e. _om /\ b e. _om ) /\ A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) /\ b e. a ) -> ( h ` b ) C_ ( h ` a ) )
181 180 olcd 
 |-  ( ( ( a e. _om /\ b e. _om ) /\ A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) /\ b e. a ) -> ( ( h ` a ) C_ ( h ` b ) \/ ( h ` b ) C_ ( h ` a ) ) )
182 181 3exp 
 |-  ( ( a e. _om /\ b e. _om ) -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( b e. a -> ( ( h ` a ) C_ ( h ` b ) \/ ( h ` b ) C_ ( h ` a ) ) ) ) )
183 182 com3r 
 |-  ( b e. a -> ( ( a e. _om /\ b e. _om ) -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( ( h ` a ) C_ ( h ` b ) \/ ( h ` b ) C_ ( h ` a ) ) ) ) )
184 165 170 183 3jaoi 
 |-  ( ( a e. b \/ a = b \/ b e. a ) -> ( ( a e. _om /\ b e. _om ) -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( ( h ` a ) C_ ( h ` b ) \/ ( h ` b ) C_ ( h ` a ) ) ) ) )
185 152 184 syl 
 |-  ( ( Ord a /\ Ord b ) -> ( ( a e. _om /\ b e. _om ) -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( ( h ` a ) C_ ( h ` b ) \/ ( h ` b ) C_ ( h ` a ) ) ) ) )
186 151 185 mpcom 
 |-  ( ( a e. _om /\ b e. _om ) -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( ( h ` a ) C_ ( h ` b ) \/ ( h ` b ) C_ ( h ` a ) ) ) )
187 sseq12 
 |-  ( ( ( h ` a ) = u /\ ( h ` b ) = v ) -> ( ( h ` a ) C_ ( h ` b ) <-> u C_ v ) )
188 sseq12 
 |-  ( ( ( h ` b ) = v /\ ( h ` a ) = u ) -> ( ( h ` b ) C_ ( h ` a ) <-> v C_ u ) )
189 188 ancoms 
 |-  ( ( ( h ` a ) = u /\ ( h ` b ) = v ) -> ( ( h ` b ) C_ ( h ` a ) <-> v C_ u ) )
190 187 189 orbi12d 
 |-  ( ( ( h ` a ) = u /\ ( h ` b ) = v ) -> ( ( ( h ` a ) C_ ( h ` b ) \/ ( h ` b ) C_ ( h ` a ) ) <-> ( u C_ v \/ v C_ u ) ) )
191 190 biimpcd 
 |-  ( ( ( h ` a ) C_ ( h ` b ) \/ ( h ` b ) C_ ( h ` a ) ) -> ( ( ( h ` a ) = u /\ ( h ` b ) = v ) -> ( u C_ v \/ v C_ u ) ) )
192 186 191 syl6 
 |-  ( ( a e. _om /\ b e. _om ) -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( ( ( h ` a ) = u /\ ( h ` b ) = v ) -> ( u C_ v \/ v C_ u ) ) ) )
193 192 com23 
 |-  ( ( a e. _om /\ b e. _om ) -> ( ( ( h ` a ) = u /\ ( h ` b ) = v ) -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( u C_ v \/ v C_ u ) ) ) )
194 193 exp4b 
 |-  ( a e. _om -> ( b e. _om -> ( ( h ` a ) = u -> ( ( h ` b ) = v -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( u C_ v \/ v C_ u ) ) ) ) ) )
195 194 com23 
 |-  ( a e. _om -> ( ( h ` a ) = u -> ( b e. _om -> ( ( h ` b ) = v -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( u C_ v \/ v C_ u ) ) ) ) ) )
196 195 rexlimiv 
 |-  ( E. a e. _om ( h ` a ) = u -> ( b e. _om -> ( ( h ` b ) = v -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( u C_ v \/ v C_ u ) ) ) ) )
197 196 rexlimdv 
 |-  ( E. a e. _om ( h ` a ) = u -> ( E. b e. _om ( h ` b ) = v -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( u C_ v \/ v C_ u ) ) ) )
198 148 197 biimtrdi 
 |-  ( h Fn _om -> ( u e. ran h -> ( E. b e. _om ( h ` b ) = v -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( u C_ v \/ v C_ u ) ) ) ) )
199 198 com23 
 |-  ( h Fn _om -> ( E. b e. _om ( h ` b ) = v -> ( u e. ran h -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( u C_ v \/ v C_ u ) ) ) ) )
200 147 199 sylbid 
 |-  ( h Fn _om -> ( v e. ran h -> ( u e. ran h -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( u C_ v \/ v C_ u ) ) ) ) )
201 200 com24 
 |-  ( h Fn _om -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( u e. ran h -> ( v e. ran h -> ( u C_ v \/ v C_ u ) ) ) ) )
202 201 imp 
 |-  ( ( h Fn _om /\ A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) ) -> ( u e. ran h -> ( v e. ran h -> ( u C_ v \/ v C_ u ) ) ) )
203 202 ralrimdv 
 |-  ( ( h Fn _om /\ A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) ) -> ( u e. ran h -> A. v e. ran h ( u C_ v \/ v C_ u ) ) )
204 146 203 sylan 
 |-  ( ( h : _om --> S /\ A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) ) -> ( u e. ran h -> A. v e. ran h ( u C_ v \/ v C_ u ) ) )
205 145 204 jcad 
 |-  ( ( h : _om --> S /\ A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) ) -> ( u e. ran h -> ( Fun u /\ A. v e. ran h ( u C_ v \/ v C_ u ) ) ) )
206 205 ralrimiv 
 |-  ( ( h : _om --> S /\ A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) ) -> A. u e. ran h ( Fun u /\ A. v e. ran h ( u C_ v \/ v C_ u ) ) )
207 fununi 
 |-  ( A. u e. ran h ( Fun u /\ A. v e. ran h ( u C_ v \/ v C_ u ) ) -> Fun U. ran h )
208 206 207 syl 
 |-  ( ( h : _om --> S /\ A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) ) -> Fun U. ran h )
209 132 208 syldan 
 |-  ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> Fun U. ran h )
210 vex 
 |-  m e. _V
211 210 eldm2 
 |-  ( m e. dom U. ran h <-> E. u <. m , u >. e. U. ran h )
212 eluni2 
 |-  ( <. m , u >. e. U. ran h <-> E. v e. ran h <. m , u >. e. v )
213 210 141 opeldm 
 |-  ( <. m , u >. e. v -> m e. dom v )
214 213 a1i 
 |-  ( h : _om --> S -> ( <. m , u >. e. v -> m e. dom v ) )
215 133 46 sstrdi 
 |-  ( h : _om --> S -> ran h C_ { s | ( (/) e. dom s /\ dom s e. _om ) } )
216 ssel 
 |-  ( ran h C_ { s | ( (/) e. dom s /\ dom s e. _om ) } -> ( v e. ran h -> v e. { s | ( (/) e. dom s /\ dom s e. _om ) } ) )
217 vex 
 |-  v e. _V
218 dmeq 
 |-  ( s = v -> dom s = dom v )
219 218 eleq2d 
 |-  ( s = v -> ( (/) e. dom s <-> (/) e. dom v ) )
220 218 eleq1d 
 |-  ( s = v -> ( dom s e. _om <-> dom v e. _om ) )
221 219 220 anbi12d 
 |-  ( s = v -> ( ( (/) e. dom s /\ dom s e. _om ) <-> ( (/) e. dom v /\ dom v e. _om ) ) )
222 217 221 elab 
 |-  ( v e. { s | ( (/) e. dom s /\ dom s e. _om ) } <-> ( (/) e. dom v /\ dom v e. _om ) )
223 222 simprbi 
 |-  ( v e. { s | ( (/) e. dom s /\ dom s e. _om ) } -> dom v e. _om )
224 216 223 syl6 
 |-  ( ran h C_ { s | ( (/) e. dom s /\ dom s e. _om ) } -> ( v e. ran h -> dom v e. _om ) )
225 215 224 syl 
 |-  ( h : _om --> S -> ( v e. ran h -> dom v e. _om ) )
226 214 225 anim12d 
 |-  ( h : _om --> S -> ( ( <. m , u >. e. v /\ v e. ran h ) -> ( m e. dom v /\ dom v e. _om ) ) )
227 elnn 
 |-  ( ( m e. dom v /\ dom v e. _om ) -> m e. _om )
228 226 227 syl6 
 |-  ( h : _om --> S -> ( ( <. m , u >. e. v /\ v e. ran h ) -> m e. _om ) )
229 228 expcomd 
 |-  ( h : _om --> S -> ( v e. ran h -> ( <. m , u >. e. v -> m e. _om ) ) )
230 229 rexlimdv 
 |-  ( h : _om --> S -> ( E. v e. ran h <. m , u >. e. v -> m e. _om ) )
231 212 230 biimtrid 
 |-  ( h : _om --> S -> ( <. m , u >. e. U. ran h -> m e. _om ) )
232 231 exlimdv 
 |-  ( h : _om --> S -> ( E. u <. m , u >. e. U. ran h -> m e. _om ) )
233 211 232 biimtrid 
 |-  ( h : _om --> S -> ( m e. dom U. ran h -> m e. _om ) )
234 233 adantr 
 |-  ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( m e. dom U. ran h -> m e. _om ) )
235 id 
 |-  ( m e. _om -> m e. _om )
236 fnfvelrn 
 |-  ( ( h Fn _om /\ m e. _om ) -> ( h ` m ) e. ran h )
237 146 235 236 syl2anr 
 |-  ( ( m e. _om /\ h : _om --> S ) -> ( h ` m ) e. ran h )
238 237 adantrr 
 |-  ( ( m e. _om /\ ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) ) -> ( h ` m ) e. ran h )
239 128 simpld 
 |-  ( ( m e. _om /\ ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) ) -> m e. dom ( h ` m ) )
240 dmeq 
 |-  ( u = ( h ` m ) -> dom u = dom ( h ` m ) )
241 240 eliuni 
 |-  ( ( ( h ` m ) e. ran h /\ m e. dom ( h ` m ) ) -> m e. U_ u e. ran h dom u )
242 238 239 241 syl2anc 
 |-  ( ( m e. _om /\ ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) ) -> m e. U_ u e. ran h dom u )
243 dmuni 
 |-  dom U. ran h = U_ u e. ran h dom u
244 242 243 eleqtrrdi 
 |-  ( ( m e. _om /\ ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) ) -> m e. dom U. ran h )
245 244 expcom 
 |-  ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( m e. _om -> m e. dom U. ran h ) )
246 234 245 impbid 
 |-  ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( m e. dom U. ran h <-> m e. _om ) )
247 246 eqrdv 
 |-  ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> dom U. ran h = _om )
248 rnuni 
 |-  ran U. ran h = U_ s e. ran h ran s
249 frn 
 |-  ( s : suc n --> A -> ran s C_ A )
250 249 3ad2ant1 
 |-  ( ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) -> ran s C_ A )
251 250 rexlimivw 
 |-  ( E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) -> ran s C_ A )
252 251 ss2abi 
 |-  { s | E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) } C_ { s | ran s C_ A }
253 2 252 eqsstri 
 |-  S C_ { s | ran s C_ A }
254 133 253 sstrdi 
 |-  ( h : _om --> S -> ran h C_ { s | ran s C_ A } )
255 ssel 
 |-  ( ran h C_ { s | ran s C_ A } -> ( s e. ran h -> s e. { s | ran s C_ A } ) )
256 abid 
 |-  ( s e. { s | ran s C_ A } <-> ran s C_ A )
257 255 256 imbitrdi 
 |-  ( ran h C_ { s | ran s C_ A } -> ( s e. ran h -> ran s C_ A ) )
258 254 257 syl 
 |-  ( h : _om --> S -> ( s e. ran h -> ran s C_ A ) )
259 258 ralrimiv 
 |-  ( h : _om --> S -> A. s e. ran h ran s C_ A )
260 iunss 
 |-  ( U_ s e. ran h ran s C_ A <-> A. s e. ran h ran s C_ A )
261 259 260 sylibr 
 |-  ( h : _om --> S -> U_ s e. ran h ran s C_ A )
262 248 261 eqsstrid 
 |-  ( h : _om --> S -> ran U. ran h C_ A )
263 262 adantr 
 |-  ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ran U. ran h C_ A )
264 df-fn 
 |-  ( U. ran h Fn _om <-> ( Fun U. ran h /\ dom U. ran h = _om ) )
265 df-f 
 |-  ( U. ran h : _om --> A <-> ( U. ran h Fn _om /\ ran U. ran h C_ A ) )
266 265 biimpri 
 |-  ( ( U. ran h Fn _om /\ ran U. ran h C_ A ) -> U. ran h : _om --> A )
267 264 266 sylanbr 
 |-  ( ( ( Fun U. ran h /\ dom U. ran h = _om ) /\ ran U. ran h C_ A ) -> U. ran h : _om --> A )
268 209 247 263 267 syl21anc 
 |-  ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> U. ran h : _om --> A )
269 fnfvelrn 
 |-  ( ( h Fn _om /\ (/) e. _om ) -> ( h ` (/) ) e. ran h )
270 146 28 269 sylancl 
 |-  ( h : _om --> S -> ( h ` (/) ) e. ran h )
271 270 adantr 
 |-  ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( h ` (/) ) e. ran h )
272 elssuni 
 |-  ( ( h ` (/) ) e. ran h -> ( h ` (/) ) C_ U. ran h )
273 271 272 syl 
 |-  ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( h ` (/) ) C_ U. ran h )
274 56 adantr 
 |-  ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> (/) e. dom ( h ` (/) ) )
275 funssfv 
 |-  ( ( Fun U. ran h /\ ( h ` (/) ) C_ U. ran h /\ (/) e. dom ( h ` (/) ) ) -> ( U. ran h ` (/) ) = ( ( h ` (/) ) ` (/) ) )
276 209 273 274 275 syl3anc 
 |-  ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( U. ran h ` (/) ) = ( ( h ` (/) ) ` (/) ) )
277 simp2 
 |-  ( ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) -> ( s ` (/) ) = C )
278 277 rexlimivw 
 |-  ( E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) -> ( s ` (/) ) = C )
279 278 ss2abi 
 |-  { s | E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) } C_ { s | ( s ` (/) ) = C }
280 2 279 eqsstri 
 |-  S C_ { s | ( s ` (/) ) = C }
281 133 280 sstrdi 
 |-  ( h : _om --> S -> ran h C_ { s | ( s ` (/) ) = C } )
282 ssel 
 |-  ( ran h C_ { s | ( s ` (/) ) = C } -> ( ( h ` (/) ) e. ran h -> ( h ` (/) ) e. { s | ( s ` (/) ) = C } ) )
283 fveq1 
 |-  ( s = ( h ` (/) ) -> ( s ` (/) ) = ( ( h ` (/) ) ` (/) ) )
284 283 eqeq1d 
 |-  ( s = ( h ` (/) ) -> ( ( s ` (/) ) = C <-> ( ( h ` (/) ) ` (/) ) = C ) )
285 48 284 elab 
 |-  ( ( h ` (/) ) e. { s | ( s ` (/) ) = C } <-> ( ( h ` (/) ) ` (/) ) = C )
286 282 285 imbitrdi 
 |-  ( ran h C_ { s | ( s ` (/) ) = C } -> ( ( h ` (/) ) e. ran h -> ( ( h ` (/) ) ` (/) ) = C ) )
287 281 286 syl 
 |-  ( h : _om --> S -> ( ( h ` (/) ) e. ran h -> ( ( h ` (/) ) ` (/) ) = C ) )
288 287 adantr 
 |-  ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( ( h ` (/) ) e. ran h -> ( ( h ` (/) ) ` (/) ) = C ) )
289 271 288 mpd 
 |-  ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( ( h ` (/) ) ` (/) ) = C )
290 276 289 eqtrd 
 |-  ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( U. ran h ` (/) ) = C )
291 nfv 
 |-  F/ k h : _om --> S
292 nfra1 
 |-  F/ k A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) )
293 291 292 nfan 
 |-  F/ k ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) )
294 133 ad2antrr 
 |-  ( ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) /\ k e. _om ) -> ran h C_ S )
295 peano2 
 |-  ( k e. _om -> suc k e. _om )
296 fnfvelrn 
 |-  ( ( h Fn _om /\ suc k e. _om ) -> ( h ` suc k ) e. ran h )
297 146 295 296 syl2an 
 |-  ( ( h : _om --> S /\ k e. _om ) -> ( h ` suc k ) e. ran h )
298 297 adantlr 
 |-  ( ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) /\ k e. _om ) -> ( h ` suc k ) e. ran h )
299 239 expcom 
 |-  ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( m e. _om -> m e. dom ( h ` m ) ) )
300 299 ralrimiv 
 |-  ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> A. m e. _om m e. dom ( h ` m ) )
301 id 
 |-  ( m = suc k -> m = suc k )
302 fveq2 
 |-  ( m = suc k -> ( h ` m ) = ( h ` suc k ) )
303 302 dmeqd 
 |-  ( m = suc k -> dom ( h ` m ) = dom ( h ` suc k ) )
304 301 303 eleq12d 
 |-  ( m = suc k -> ( m e. dom ( h ` m ) <-> suc k e. dom ( h ` suc k ) ) )
305 304 rspcv 
 |-  ( suc k e. _om -> ( A. m e. _om m e. dom ( h ` m ) -> suc k e. dom ( h ` suc k ) ) )
306 295 305 syl 
 |-  ( k e. _om -> ( A. m e. _om m e. dom ( h ` m ) -> suc k e. dom ( h ` suc k ) ) )
307 300 306 mpan9 
 |-  ( ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) /\ k e. _om ) -> suc k e. dom ( h ` suc k ) )
308 eleq2 
 |-  ( dom s = suc n -> ( suc k e. dom s <-> suc k e. suc n ) )
309 308 biimpa 
 |-  ( ( dom s = suc n /\ suc k e. dom s ) -> suc k e. suc n )
310 31 309 sylan 
 |-  ( ( s : suc n --> A /\ suc k e. dom s ) -> suc k e. suc n )
311 ordsucelsuc 
 |-  ( Ord n -> ( k e. n <-> suc k e. suc n ) )
312 32 311 syl 
 |-  ( n e. _om -> ( k e. n <-> suc k e. suc n ) )
313 312 biimprd 
 |-  ( n e. _om -> ( suc k e. suc n -> k e. n ) )
314 rsp 
 |-  ( A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) -> ( k e. n -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) )
315 313 314 syl9r 
 |-  ( A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) -> ( n e. _om -> ( suc k e. suc n -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) ) )
316 315 com13 
 |-  ( suc k e. suc n -> ( n e. _om -> ( A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) ) )
317 310 316 syl 
 |-  ( ( s : suc n --> A /\ suc k e. dom s ) -> ( n e. _om -> ( A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) ) )
318 317 ex 
 |-  ( s : suc n --> A -> ( suc k e. dom s -> ( n e. _om -> ( A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) ) ) )
319 318 com24 
 |-  ( s : suc n --> A -> ( A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) -> ( n e. _om -> ( suc k e. dom s -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) ) ) )
320 319 imp 
 |-  ( ( s : suc n --> A /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) -> ( n e. _om -> ( suc k e. dom s -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) ) )
321 320 3adant2 
 |-  ( ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) -> ( n e. _om -> ( suc k e. dom s -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) ) )
322 321 impcom 
 |-  ( ( n e. _om /\ ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) ) -> ( suc k e. dom s -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) )
323 322 rexlimiva 
 |-  ( E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) -> ( suc k e. dom s -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) )
324 323 ss2abi 
 |-  { s | E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) } C_ { s | ( suc k e. dom s -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) }
325 2 324 eqsstri 
 |-  S C_ { s | ( suc k e. dom s -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) }
326 sstr 
 |-  ( ( ran h C_ S /\ S C_ { s | ( suc k e. dom s -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) } ) -> ran h C_ { s | ( suc k e. dom s -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) } )
327 325 326 mpan2 
 |-  ( ran h C_ S -> ran h C_ { s | ( suc k e. dom s -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) } )
328 327 sseld 
 |-  ( ran h C_ S -> ( ( h ` suc k ) e. ran h -> ( h ` suc k ) e. { s | ( suc k e. dom s -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) } ) )
329 fvex 
 |-  ( h ` suc k ) e. _V
330 dmeq 
 |-  ( s = ( h ` suc k ) -> dom s = dom ( h ` suc k ) )
331 330 eleq2d 
 |-  ( s = ( h ` suc k ) -> ( suc k e. dom s <-> suc k e. dom ( h ` suc k ) ) )
332 fveq1 
 |-  ( s = ( h ` suc k ) -> ( s ` suc k ) = ( ( h ` suc k ) ` suc k ) )
333 fveq1 
 |-  ( s = ( h ` suc k ) -> ( s ` k ) = ( ( h ` suc k ) ` k ) )
334 333 fveq2d 
 |-  ( s = ( h ` suc k ) -> ( F ` ( s ` k ) ) = ( F ` ( ( h ` suc k ) ` k ) ) )
335 332 334 eleq12d 
 |-  ( s = ( h ` suc k ) -> ( ( s ` suc k ) e. ( F ` ( s ` k ) ) <-> ( ( h ` suc k ) ` suc k ) e. ( F ` ( ( h ` suc k ) ` k ) ) ) )
336 331 335 imbi12d 
 |-  ( s = ( h ` suc k ) -> ( ( suc k e. dom s -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) <-> ( suc k e. dom ( h ` suc k ) -> ( ( h ` suc k ) ` suc k ) e. ( F ` ( ( h ` suc k ) ` k ) ) ) ) )
337 329 336 elab 
 |-  ( ( h ` suc k ) e. { s | ( suc k e. dom s -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) } <-> ( suc k e. dom ( h ` suc k ) -> ( ( h ` suc k ) ` suc k ) e. ( F ` ( ( h ` suc k ) ` k ) ) ) )
338 328 337 imbitrdi 
 |-  ( ran h C_ S -> ( ( h ` suc k ) e. ran h -> ( suc k e. dom ( h ` suc k ) -> ( ( h ` suc k ) ` suc k ) e. ( F ` ( ( h ` suc k ) ` k ) ) ) ) )
339 294 298 307 338 syl3c 
 |-  ( ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) /\ k e. _om ) -> ( ( h ` suc k ) ` suc k ) e. ( F ` ( ( h ` suc k ) ` k ) ) )
340 209 adantr 
 |-  ( ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) /\ k e. _om ) -> Fun U. ran h )
341 elssuni 
 |-  ( ( h ` suc k ) e. ran h -> ( h ` suc k ) C_ U. ran h )
342 297 341 syl 
 |-  ( ( h : _om --> S /\ k e. _om ) -> ( h ` suc k ) C_ U. ran h )
343 342 adantlr 
 |-  ( ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) /\ k e. _om ) -> ( h ` suc k ) C_ U. ran h )
344 funssfv 
 |-  ( ( Fun U. ran h /\ ( h ` suc k ) C_ U. ran h /\ suc k e. dom ( h ` suc k ) ) -> ( U. ran h ` suc k ) = ( ( h ` suc k ) ` suc k ) )
345 340 343 307 344 syl3anc 
 |-  ( ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) /\ k e. _om ) -> ( U. ran h ` suc k ) = ( ( h ` suc k ) ` suc k ) )
346 215 sseld 
 |-  ( h : _om --> S -> ( ( h ` suc k ) e. ran h -> ( h ` suc k ) e. { s | ( (/) e. dom s /\ dom s e. _om ) } ) )
347 330 eleq2d 
 |-  ( s = ( h ` suc k ) -> ( (/) e. dom s <-> (/) e. dom ( h ` suc k ) ) )
348 330 eleq1d 
 |-  ( s = ( h ` suc k ) -> ( dom s e. _om <-> dom ( h ` suc k ) e. _om ) )
349 347 348 anbi12d 
 |-  ( s = ( h ` suc k ) -> ( ( (/) e. dom s /\ dom s e. _om ) <-> ( (/) e. dom ( h ` suc k ) /\ dom ( h ` suc k ) e. _om ) ) )
350 329 349 elab 
 |-  ( ( h ` suc k ) e. { s | ( (/) e. dom s /\ dom s e. _om ) } <-> ( (/) e. dom ( h ` suc k ) /\ dom ( h ` suc k ) e. _om ) )
351 346 350 imbitrdi 
 |-  ( h : _om --> S -> ( ( h ` suc k ) e. ran h -> ( (/) e. dom ( h ` suc k ) /\ dom ( h ` suc k ) e. _om ) ) )
352 351 adantr 
 |-  ( ( h : _om --> S /\ k e. _om ) -> ( ( h ` suc k ) e. ran h -> ( (/) e. dom ( h ` suc k ) /\ dom ( h ` suc k ) e. _om ) ) )
353 297 352 mpd 
 |-  ( ( h : _om --> S /\ k e. _om ) -> ( (/) e. dom ( h ` suc k ) /\ dom ( h ` suc k ) e. _om ) )
354 353 simprd 
 |-  ( ( h : _om --> S /\ k e. _om ) -> dom ( h ` suc k ) e. _om )
355 nnord 
 |-  ( dom ( h ` suc k ) e. _om -> Ord dom ( h ` suc k ) )
356 ordtr 
 |-  ( Ord dom ( h ` suc k ) -> Tr dom ( h ` suc k ) )
357 trsuc 
 |-  ( ( Tr dom ( h ` suc k ) /\ suc k e. dom ( h ` suc k ) ) -> k e. dom ( h ` suc k ) )
358 357 ex 
 |-  ( Tr dom ( h ` suc k ) -> ( suc k e. dom ( h ` suc k ) -> k e. dom ( h ` suc k ) ) )
359 354 355 356 358 4syl 
 |-  ( ( h : _om --> S /\ k e. _om ) -> ( suc k e. dom ( h ` suc k ) -> k e. dom ( h ` suc k ) ) )
360 359 adantlr 
 |-  ( ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) /\ k e. _om ) -> ( suc k e. dom ( h ` suc k ) -> k e. dom ( h ` suc k ) ) )
361 307 360 mpd 
 |-  ( ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) /\ k e. _om ) -> k e. dom ( h ` suc k ) )
362 funssfv 
 |-  ( ( Fun U. ran h /\ ( h ` suc k ) C_ U. ran h /\ k e. dom ( h ` suc k ) ) -> ( U. ran h ` k ) = ( ( h ` suc k ) ` k ) )
363 340 343 361 362 syl3anc 
 |-  ( ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) /\ k e. _om ) -> ( U. ran h ` k ) = ( ( h ` suc k ) ` k ) )
364 simpl 
 |-  ( ( ( U. ran h ` suc k ) = ( ( h ` suc k ) ` suc k ) /\ ( U. ran h ` k ) = ( ( h ` suc k ) ` k ) ) -> ( U. ran h ` suc k ) = ( ( h ` suc k ) ` suc k ) )
365 simpr 
 |-  ( ( ( U. ran h ` suc k ) = ( ( h ` suc k ) ` suc k ) /\ ( U. ran h ` k ) = ( ( h ` suc k ) ` k ) ) -> ( U. ran h ` k ) = ( ( h ` suc k ) ` k ) )
366 365 fveq2d 
 |-  ( ( ( U. ran h ` suc k ) = ( ( h ` suc k ) ` suc k ) /\ ( U. ran h ` k ) = ( ( h ` suc k ) ` k ) ) -> ( F ` ( U. ran h ` k ) ) = ( F ` ( ( h ` suc k ) ` k ) ) )
367 364 366 eleq12d 
 |-  ( ( ( U. ran h ` suc k ) = ( ( h ` suc k ) ` suc k ) /\ ( U. ran h ` k ) = ( ( h ` suc k ) ` k ) ) -> ( ( U. ran h ` suc k ) e. ( F ` ( U. ran h ` k ) ) <-> ( ( h ` suc k ) ` suc k ) e. ( F ` ( ( h ` suc k ) ` k ) ) ) )
368 345 363 367 syl2anc 
 |-  ( ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) /\ k e. _om ) -> ( ( U. ran h ` suc k ) e. ( F ` ( U. ran h ` k ) ) <-> ( ( h ` suc k ) ` suc k ) e. ( F ` ( ( h ` suc k ) ` k ) ) ) )
369 339 368 mpbird 
 |-  ( ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) /\ k e. _om ) -> ( U. ran h ` suc k ) e. ( F ` ( U. ran h ` k ) ) )
370 369 ex 
 |-  ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( k e. _om -> ( U. ran h ` suc k ) e. ( F ` ( U. ran h ` k ) ) ) )
371 293 370 ralrimi 
 |-  ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> A. k e. _om ( U. ran h ` suc k ) e. ( F ` ( U. ran h ` k ) ) )
372 vex 
 |-  h e. _V
373 372 rnex 
 |-  ran h e. _V
374 373 uniex 
 |-  U. ran h e. _V
375 feq1 
 |-  ( g = U. ran h -> ( g : _om --> A <-> U. ran h : _om --> A ) )
376 fveq1 
 |-  ( g = U. ran h -> ( g ` (/) ) = ( U. ran h ` (/) ) )
377 376 eqeq1d 
 |-  ( g = U. ran h -> ( ( g ` (/) ) = C <-> ( U. ran h ` (/) ) = C ) )
378 fveq1 
 |-  ( g = U. ran h -> ( g ` suc k ) = ( U. ran h ` suc k ) )
379 fveq1 
 |-  ( g = U. ran h -> ( g ` k ) = ( U. ran h ` k ) )
380 379 fveq2d 
 |-  ( g = U. ran h -> ( F ` ( g ` k ) ) = ( F ` ( U. ran h ` k ) ) )
381 378 380 eleq12d 
 |-  ( g = U. ran h -> ( ( g ` suc k ) e. ( F ` ( g ` k ) ) <-> ( U. ran h ` suc k ) e. ( F ` ( U. ran h ` k ) ) ) )
382 381 ralbidv 
 |-  ( g = U. ran h -> ( A. k e. _om ( g ` suc k ) e. ( F ` ( g ` k ) ) <-> A. k e. _om ( U. ran h ` suc k ) e. ( F ` ( U. ran h ` k ) ) ) )
383 375 377 382 3anbi123d 
 |-  ( g = U. ran h -> ( ( g : _om --> A /\ ( g ` (/) ) = C /\ A. k e. _om ( g ` suc k ) e. ( F ` ( g ` k ) ) ) <-> ( U. ran h : _om --> A /\ ( U. ran h ` (/) ) = C /\ A. k e. _om ( U. ran h ` suc k ) e. ( F ` ( U. ran h ` k ) ) ) ) )
384 374 383 spcev 
 |-  ( ( U. ran h : _om --> A /\ ( U. ran h ` (/) ) = C /\ A. k e. _om ( U. ran h ` suc k ) e. ( F ` ( U. ran h ` k ) ) ) -> E. g ( g : _om --> A /\ ( g ` (/) ) = C /\ A. k e. _om ( g ` suc k ) e. ( F ` ( g ` k ) ) ) )
385 268 290 371 384 syl3anc 
 |-  ( ( h : _om --> S /\ 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. ( F ` ( g ` k ) ) ) )
386 385 exlimiv 
 |-  ( E. h ( h : _om --> S /\ 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. ( F ` ( g ` k ) ) ) )