Step |
Hyp |
Ref |
Expression |
1 |
|
inf3lem.1 |
|- G = ( y e. _V |-> { w e. x | ( w i^i x ) C_ y } ) |
2 |
|
inf3lem.2 |
|- F = ( rec ( G , (/) ) |` _om ) |
3 |
|
inf3lem.3 |
|- A e. _V |
4 |
|
inf3lem.4 |
|- B e. _V |
5 |
|
fveq2 |
|- ( A = (/) -> ( F ` A ) = ( F ` (/) ) ) |
6 |
1 2 3 4
|
inf3lemb |
|- ( F ` (/) ) = (/) |
7 |
5 6
|
eqtrdi |
|- ( A = (/) -> ( F ` A ) = (/) ) |
8 |
|
0ss |
|- (/) C_ x |
9 |
7 8
|
eqsstrdi |
|- ( A = (/) -> ( F ` A ) C_ x ) |
10 |
9
|
a1d |
|- ( A = (/) -> ( A e. _om -> ( F ` A ) C_ x ) ) |
11 |
|
nnsuc |
|- ( ( A e. _om /\ A =/= (/) ) -> E. v e. _om A = suc v ) |
12 |
|
vex |
|- v e. _V |
13 |
1 2 12 4
|
inf3lemc |
|- ( v e. _om -> ( F ` suc v ) = ( G ` ( F ` v ) ) ) |
14 |
13
|
eleq2d |
|- ( v e. _om -> ( u e. ( F ` suc v ) <-> u e. ( G ` ( F ` v ) ) ) ) |
15 |
|
vex |
|- u e. _V |
16 |
|
fvex |
|- ( F ` v ) e. _V |
17 |
1 2 15 16
|
inf3lema |
|- ( u e. ( G ` ( F ` v ) ) <-> ( u e. x /\ ( u i^i x ) C_ ( F ` v ) ) ) |
18 |
17
|
simplbi |
|- ( u e. ( G ` ( F ` v ) ) -> u e. x ) |
19 |
14 18
|
syl6bi |
|- ( v e. _om -> ( u e. ( F ` suc v ) -> u e. x ) ) |
20 |
19
|
ssrdv |
|- ( v e. _om -> ( F ` suc v ) C_ x ) |
21 |
|
fveq2 |
|- ( A = suc v -> ( F ` A ) = ( F ` suc v ) ) |
22 |
21
|
sseq1d |
|- ( A = suc v -> ( ( F ` A ) C_ x <-> ( F ` suc v ) C_ x ) ) |
23 |
20 22
|
syl5ibrcom |
|- ( v e. _om -> ( A = suc v -> ( F ` A ) C_ x ) ) |
24 |
23
|
rexlimiv |
|- ( E. v e. _om A = suc v -> ( F ` A ) C_ x ) |
25 |
11 24
|
syl |
|- ( ( A e. _om /\ A =/= (/) ) -> ( F ` A ) C_ x ) |
26 |
25
|
expcom |
|- ( A =/= (/) -> ( A e. _om -> ( F ` A ) C_ x ) ) |
27 |
10 26
|
pm2.61ine |
|- ( A e. _om -> ( F ` A ) C_ x ) |