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