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 ) ) ) ) |