Step |
Hyp |
Ref |
Expression |
1 |
|
rdgssun.1 |
|- F = ( w e. _V |-> ( w u. B ) ) |
2 |
|
rdgssun.2 |
|- B e. _V |
3 |
|
nfsbc1v |
|- F/ x [. (/) / x ]. A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) |
4 |
|
0ex |
|- (/) e. _V |
5 |
|
rzal |
|- ( x = (/) -> A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) ) |
6 |
|
sbceq1a |
|- ( x = (/) -> ( A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) <-> [. (/) / x ]. A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) ) ) |
7 |
5 6
|
mpbid |
|- ( x = (/) -> [. (/) / x ]. A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) ) |
8 |
3 4 7
|
vtoclef |
|- [. (/) / x ]. A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) |
9 |
|
vex |
|- y e. _V |
10 |
9
|
elsuc |
|- ( y e. suc x <-> ( y e. x \/ y = x ) ) |
11 |
|
ssun1 |
|- ( rec ( F , A ) ` x ) C_ ( ( rec ( F , A ) ` x ) u. [_ ( rec ( F , A ) ` x ) / w ]_ B ) |
12 |
|
fvex |
|- ( rec ( F , A ) ` x ) e. _V |
13 |
2
|
csbex |
|- [_ ( rec ( F , A ) ` x ) / w ]_ B e. _V |
14 |
12 13
|
unex |
|- ( ( rec ( F , A ) ` x ) u. [_ ( rec ( F , A ) ` x ) / w ]_ B ) e. _V |
15 |
|
nfcv |
|- F/_ w A |
16 |
|
nfcv |
|- F/_ w x |
17 |
|
nfmpt1 |
|- F/_ w ( w e. _V |-> ( w u. B ) ) |
18 |
1 17
|
nfcxfr |
|- F/_ w F |
19 |
18 15
|
nfrdg |
|- F/_ w rec ( F , A ) |
20 |
19 16
|
nffv |
|- F/_ w ( rec ( F , A ) ` x ) |
21 |
20
|
nfcsb1 |
|- F/_ w [_ ( rec ( F , A ) ` x ) / w ]_ B |
22 |
20 21
|
nfun |
|- F/_ w ( ( rec ( F , A ) ` x ) u. [_ ( rec ( F , A ) ` x ) / w ]_ B ) |
23 |
|
rdgeq1 |
|- ( F = ( w e. _V |-> ( w u. B ) ) -> rec ( F , A ) = rec ( ( w e. _V |-> ( w u. B ) ) , A ) ) |
24 |
1 23
|
ax-mp |
|- rec ( F , A ) = rec ( ( w e. _V |-> ( w u. B ) ) , A ) |
25 |
|
id |
|- ( w = ( rec ( F , A ) ` x ) -> w = ( rec ( F , A ) ` x ) ) |
26 |
|
csbeq1a |
|- ( w = ( rec ( F , A ) ` x ) -> B = [_ ( rec ( F , A ) ` x ) / w ]_ B ) |
27 |
25 26
|
uneq12d |
|- ( w = ( rec ( F , A ) ` x ) -> ( w u. B ) = ( ( rec ( F , A ) ` x ) u. [_ ( rec ( F , A ) ` x ) / w ]_ B ) ) |
28 |
15 16 22 24 27
|
rdgsucmptf |
|- ( ( x e. On /\ ( ( rec ( F , A ) ` x ) u. [_ ( rec ( F , A ) ` x ) / w ]_ B ) e. _V ) -> ( rec ( F , A ) ` suc x ) = ( ( rec ( F , A ) ` x ) u. [_ ( rec ( F , A ) ` x ) / w ]_ B ) ) |
29 |
14 28
|
mpan2 |
|- ( x e. On -> ( rec ( F , A ) ` suc x ) = ( ( rec ( F , A ) ` x ) u. [_ ( rec ( F , A ) ` x ) / w ]_ B ) ) |
30 |
11 29
|
sseqtrrid |
|- ( x e. On -> ( rec ( F , A ) ` x ) C_ ( rec ( F , A ) ` suc x ) ) |
31 |
|
sstr2 |
|- ( ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) -> ( ( rec ( F , A ) ` x ) C_ ( rec ( F , A ) ` suc x ) -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` suc x ) ) ) |
32 |
30 31
|
syl5com |
|- ( x e. On -> ( ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` suc x ) ) ) |
33 |
32
|
imim2d |
|- ( x e. On -> ( ( y e. x -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) ) -> ( y e. x -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` suc x ) ) ) ) |
34 |
33
|
imp |
|- ( ( x e. On /\ ( y e. x -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) ) ) -> ( y e. x -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` suc x ) ) ) |
35 |
|
fveq2 |
|- ( y = x -> ( rec ( F , A ) ` y ) = ( rec ( F , A ) ` x ) ) |
36 |
35
|
sseq1d |
|- ( y = x -> ( ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` suc x ) <-> ( rec ( F , A ) ` x ) C_ ( rec ( F , A ) ` suc x ) ) ) |
37 |
30 36
|
syl5ibrcom |
|- ( x e. On -> ( y = x -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` suc x ) ) ) |
38 |
37
|
adantr |
|- ( ( x e. On /\ ( y e. x -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) ) ) -> ( y = x -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` suc x ) ) ) |
39 |
34 38
|
jaod |
|- ( ( x e. On /\ ( y e. x -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) ) ) -> ( ( y e. x \/ y = x ) -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` suc x ) ) ) |
40 |
10 39
|
syl5bi |
|- ( ( x e. On /\ ( y e. x -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) ) ) -> ( y e. suc x -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` suc x ) ) ) |
41 |
40
|
ex |
|- ( x e. On -> ( ( y e. x -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) ) -> ( y e. suc x -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` suc x ) ) ) ) |
42 |
41
|
ralimdv2 |
|- ( x e. On -> ( A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) -> A. y e. suc x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` suc x ) ) ) |
43 |
|
df-sbc |
|- ( [. suc x / x ]. A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) <-> suc x e. { x | A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) } ) |
44 |
|
vex |
|- x e. _V |
45 |
44
|
sucex |
|- suc x e. _V |
46 |
|
fveq2 |
|- ( z = suc x -> ( rec ( F , A ) ` z ) = ( rec ( F , A ) ` suc x ) ) |
47 |
46
|
sseq2d |
|- ( z = suc x -> ( ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` z ) <-> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` suc x ) ) ) |
48 |
47
|
raleqbi1dv |
|- ( z = suc x -> ( A. y e. z ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` z ) <-> A. y e. suc x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` suc x ) ) ) |
49 |
|
fveq2 |
|- ( x = z -> ( rec ( F , A ) ` x ) = ( rec ( F , A ) ` z ) ) |
50 |
49
|
sseq2d |
|- ( x = z -> ( ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) <-> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` z ) ) ) |
51 |
50
|
raleqbi1dv |
|- ( x = z -> ( A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) <-> A. y e. z ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` z ) ) ) |
52 |
51
|
cbvabv |
|- { x | A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) } = { z | A. y e. z ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` z ) } |
53 |
45 48 52
|
elab2 |
|- ( suc x e. { x | A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) } <-> A. y e. suc x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` suc x ) ) |
54 |
43 53
|
bitri |
|- ( [. suc x / x ]. A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) <-> A. y e. suc x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` suc x ) ) |
55 |
42 54
|
syl6ibr |
|- ( x e. On -> ( A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) -> [. suc x / x ]. A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) ) ) |
56 |
|
ssiun2 |
|- ( y e. z -> ( rec ( F , A ) ` y ) C_ U_ y e. z ( rec ( F , A ) ` y ) ) |
57 |
56
|
adantl |
|- ( ( Lim z /\ y e. z ) -> ( rec ( F , A ) ` y ) C_ U_ y e. z ( rec ( F , A ) ` y ) ) |
58 |
|
vex |
|- z e. _V |
59 |
|
rdglim2a |
|- ( ( z e. _V /\ Lim z ) -> ( rec ( F , A ) ` z ) = U_ y e. z ( rec ( F , A ) ` y ) ) |
60 |
58 59
|
mpan |
|- ( Lim z -> ( rec ( F , A ) ` z ) = U_ y e. z ( rec ( F , A ) ` y ) ) |
61 |
60
|
adantr |
|- ( ( Lim z /\ y e. z ) -> ( rec ( F , A ) ` z ) = U_ y e. z ( rec ( F , A ) ` y ) ) |
62 |
57 61
|
sseqtrrd |
|- ( ( Lim z /\ y e. z ) -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` z ) ) |
63 |
62
|
ralrimiva |
|- ( Lim z -> A. y e. z ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` z ) ) |
64 |
|
df-sbc |
|- ( [. z / x ]. A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) <-> z e. { x | A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) } ) |
65 |
52
|
eleq2i |
|- ( z e. { x | A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) } <-> z e. { z | A. y e. z ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` z ) } ) |
66 |
64 65
|
bitri |
|- ( [. z / x ]. A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) <-> z e. { z | A. y e. z ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` z ) } ) |
67 |
|
abid |
|- ( z e. { z | A. y e. z ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` z ) } <-> A. y e. z ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` z ) ) |
68 |
66 67
|
bitri |
|- ( [. z / x ]. A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) <-> A. y e. z ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` z ) ) |
69 |
63 68
|
sylibr |
|- ( Lim z -> [. z / x ]. A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) ) |
70 |
69
|
a1d |
|- ( Lim z -> ( A. x e. z A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) -> [. z / x ]. A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) ) ) |
71 |
8 55 70
|
tfindes |
|- ( x e. On -> A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) ) |
72 |
|
rsp |
|- ( A. y e. x ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) -> ( y e. x -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) ) ) |
73 |
71 72
|
syl |
|- ( x e. On -> ( y e. x -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) ) ) |
74 |
|
eleq1 |
|- ( x = X -> ( x e. On <-> X e. On ) ) |
75 |
74
|
adantl |
|- ( ( y = Y /\ x = X ) -> ( x e. On <-> X e. On ) ) |
76 |
|
eleq12 |
|- ( ( y = Y /\ x = X ) -> ( y e. x <-> Y e. X ) ) |
77 |
|
fveq2 |
|- ( y = Y -> ( rec ( F , A ) ` y ) = ( rec ( F , A ) ` Y ) ) |
78 |
77
|
adantr |
|- ( ( y = Y /\ x = X ) -> ( rec ( F , A ) ` y ) = ( rec ( F , A ) ` Y ) ) |
79 |
|
fveq2 |
|- ( x = X -> ( rec ( F , A ) ` x ) = ( rec ( F , A ) ` X ) ) |
80 |
79
|
adantl |
|- ( ( y = Y /\ x = X ) -> ( rec ( F , A ) ` x ) = ( rec ( F , A ) ` X ) ) |
81 |
78 80
|
sseq12d |
|- ( ( y = Y /\ x = X ) -> ( ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) <-> ( rec ( F , A ) ` Y ) C_ ( rec ( F , A ) ` X ) ) ) |
82 |
76 81
|
imbi12d |
|- ( ( y = Y /\ x = X ) -> ( ( y e. x -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) ) <-> ( Y e. X -> ( rec ( F , A ) ` Y ) C_ ( rec ( F , A ) ` X ) ) ) ) |
83 |
75 82
|
imbi12d |
|- ( ( y = Y /\ x = X ) -> ( ( x e. On -> ( y e. x -> ( rec ( F , A ) ` y ) C_ ( rec ( F , A ) ` x ) ) ) <-> ( X e. On -> ( Y e. X -> ( rec ( F , A ) ` Y ) C_ ( rec ( F , A ) ` X ) ) ) ) ) |
84 |
73 83
|
mpbii |
|- ( ( y = Y /\ x = X ) -> ( X e. On -> ( Y e. X -> ( rec ( F , A ) ` Y ) C_ ( rec ( F , A ) ` X ) ) ) ) |
85 |
84
|
ex |
|- ( y = Y -> ( x = X -> ( X e. On -> ( Y e. X -> ( rec ( F , A ) ` Y ) C_ ( rec ( F , A ) ` X ) ) ) ) ) |
86 |
85
|
vtocleg |
|- ( Y e. X -> ( x = X -> ( X e. On -> ( Y e. X -> ( rec ( F , A ) ` Y ) C_ ( rec ( F , A ) ` X ) ) ) ) ) |
87 |
86
|
com12 |
|- ( x = X -> ( Y e. X -> ( X e. On -> ( Y e. X -> ( rec ( F , A ) ` Y ) C_ ( rec ( F , A ) ` X ) ) ) ) ) |
88 |
87
|
vtocleg |
|- ( X e. On -> ( Y e. X -> ( X e. On -> ( Y e. X -> ( rec ( F , A ) ` Y ) C_ ( rec ( F , A ) ` X ) ) ) ) ) |
89 |
88
|
pm2.43b |
|- ( Y e. X -> ( X e. On -> ( Y e. X -> ( rec ( F , A ) ` Y ) C_ ( rec ( F , A ) ` X ) ) ) ) |
90 |
89
|
pm2.43b |
|- ( X e. On -> ( Y e. X -> ( rec ( F , A ) ` Y ) C_ ( rec ( F , A ) ` X ) ) ) |
91 |
90
|
imp |
|- ( ( X e. On /\ Y e. X ) -> ( rec ( F , A ) ` Y ) C_ ( rec ( F , A ) ` X ) ) |