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 |
|- ( v = (/) -> ( F ` v ) = ( F ` (/) ) ) |
6 |
|
suceq |
|- ( v = (/) -> suc v = suc (/) ) |
7 |
6
|
fveq2d |
|- ( v = (/) -> ( F ` suc v ) = ( F ` suc (/) ) ) |
8 |
5 7
|
sseq12d |
|- ( v = (/) -> ( ( F ` v ) C_ ( F ` suc v ) <-> ( F ` (/) ) C_ ( F ` suc (/) ) ) ) |
9 |
|
fveq2 |
|- ( v = u -> ( F ` v ) = ( F ` u ) ) |
10 |
|
suceq |
|- ( v = u -> suc v = suc u ) |
11 |
10
|
fveq2d |
|- ( v = u -> ( F ` suc v ) = ( F ` suc u ) ) |
12 |
9 11
|
sseq12d |
|- ( v = u -> ( ( F ` v ) C_ ( F ` suc v ) <-> ( F ` u ) C_ ( F ` suc u ) ) ) |
13 |
|
fveq2 |
|- ( v = suc u -> ( F ` v ) = ( F ` suc u ) ) |
14 |
|
suceq |
|- ( v = suc u -> suc v = suc suc u ) |
15 |
14
|
fveq2d |
|- ( v = suc u -> ( F ` suc v ) = ( F ` suc suc u ) ) |
16 |
13 15
|
sseq12d |
|- ( v = suc u -> ( ( F ` v ) C_ ( F ` suc v ) <-> ( F ` suc u ) C_ ( F ` suc suc u ) ) ) |
17 |
|
fveq2 |
|- ( v = A -> ( F ` v ) = ( F ` A ) ) |
18 |
|
suceq |
|- ( v = A -> suc v = suc A ) |
19 |
18
|
fveq2d |
|- ( v = A -> ( F ` suc v ) = ( F ` suc A ) ) |
20 |
17 19
|
sseq12d |
|- ( v = A -> ( ( F ` v ) C_ ( F ` suc v ) <-> ( F ` A ) C_ ( F ` suc A ) ) ) |
21 |
1 2 3 3
|
inf3lemb |
|- ( F ` (/) ) = (/) |
22 |
|
0ss |
|- (/) C_ ( F ` suc (/) ) |
23 |
21 22
|
eqsstri |
|- ( F ` (/) ) C_ ( F ` suc (/) ) |
24 |
|
sstr2 |
|- ( ( v i^i x ) C_ ( F ` u ) -> ( ( F ` u ) C_ ( F ` suc u ) -> ( v i^i x ) C_ ( F ` suc u ) ) ) |
25 |
24
|
com12 |
|- ( ( F ` u ) C_ ( F ` suc u ) -> ( ( v i^i x ) C_ ( F ` u ) -> ( v i^i x ) C_ ( F ` suc u ) ) ) |
26 |
25
|
anim2d |
|- ( ( F ` u ) C_ ( F ` suc u ) -> ( ( v e. x /\ ( v i^i x ) C_ ( F ` u ) ) -> ( v e. x /\ ( v i^i x ) C_ ( F ` suc u ) ) ) ) |
27 |
|
vex |
|- u e. _V |
28 |
1 2 27 3
|
inf3lemc |
|- ( u e. _om -> ( F ` suc u ) = ( G ` ( F ` u ) ) ) |
29 |
28
|
eleq2d |
|- ( u e. _om -> ( v e. ( F ` suc u ) <-> v e. ( G ` ( F ` u ) ) ) ) |
30 |
|
vex |
|- v e. _V |
31 |
|
fvex |
|- ( F ` u ) e. _V |
32 |
1 2 30 31
|
inf3lema |
|- ( v e. ( G ` ( F ` u ) ) <-> ( v e. x /\ ( v i^i x ) C_ ( F ` u ) ) ) |
33 |
29 32
|
bitrdi |
|- ( u e. _om -> ( v e. ( F ` suc u ) <-> ( v e. x /\ ( v i^i x ) C_ ( F ` u ) ) ) ) |
34 |
|
peano2b |
|- ( u e. _om <-> suc u e. _om ) |
35 |
27
|
sucex |
|- suc u e. _V |
36 |
1 2 35 3
|
inf3lemc |
|- ( suc u e. _om -> ( F ` suc suc u ) = ( G ` ( F ` suc u ) ) ) |
37 |
34 36
|
sylbi |
|- ( u e. _om -> ( F ` suc suc u ) = ( G ` ( F ` suc u ) ) ) |
38 |
37
|
eleq2d |
|- ( u e. _om -> ( v e. ( F ` suc suc u ) <-> v e. ( G ` ( F ` suc u ) ) ) ) |
39 |
|
fvex |
|- ( F ` suc u ) e. _V |
40 |
1 2 30 39
|
inf3lema |
|- ( v e. ( G ` ( F ` suc u ) ) <-> ( v e. x /\ ( v i^i x ) C_ ( F ` suc u ) ) ) |
41 |
38 40
|
bitrdi |
|- ( u e. _om -> ( v e. ( F ` suc suc u ) <-> ( v e. x /\ ( v i^i x ) C_ ( F ` suc u ) ) ) ) |
42 |
33 41
|
imbi12d |
|- ( u e. _om -> ( ( v e. ( F ` suc u ) -> v e. ( F ` suc suc u ) ) <-> ( ( v e. x /\ ( v i^i x ) C_ ( F ` u ) ) -> ( v e. x /\ ( v i^i x ) C_ ( F ` suc u ) ) ) ) ) |
43 |
26 42
|
syl5ibr |
|- ( u e. _om -> ( ( F ` u ) C_ ( F ` suc u ) -> ( v e. ( F ` suc u ) -> v e. ( F ` suc suc u ) ) ) ) |
44 |
43
|
imp |
|- ( ( u e. _om /\ ( F ` u ) C_ ( F ` suc u ) ) -> ( v e. ( F ` suc u ) -> v e. ( F ` suc suc u ) ) ) |
45 |
44
|
ssrdv |
|- ( ( u e. _om /\ ( F ` u ) C_ ( F ` suc u ) ) -> ( F ` suc u ) C_ ( F ` suc suc u ) ) |
46 |
45
|
ex |
|- ( u e. _om -> ( ( F ` u ) C_ ( F ` suc u ) -> ( F ` suc u ) C_ ( F ` suc suc u ) ) ) |
47 |
8 12 16 20 23 46
|
finds |
|- ( A e. _om -> ( F ` A ) C_ ( F ` suc A ) ) |