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 ffvelrn
 |-  ( ( 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 ffvelrn
 |-  ( ( 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 syl6ib
 |-  ( 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 syl6bi
 |-  ( 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 syl5bi
 |-  ( 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 syl5bi
 |-  ( 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 syl6ib
 |-  ( 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 syl6ib
 |-  ( 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 syl6ib
 |-  ( 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 syl6ib
 |-  ( 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 ) ) ) )