Step |
Hyp |
Ref |
Expression |
1 |
|
tfrlem.1 |
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) } |
2 |
|
eldm2g |
|- ( B e. dom recs ( F ) -> ( B e. dom recs ( F ) <-> E. z <. B , z >. e. recs ( F ) ) ) |
3 |
2
|
ibi |
|- ( B e. dom recs ( F ) -> E. z <. B , z >. e. recs ( F ) ) |
4 |
|
dfrecs3 |
|- recs ( F ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) } |
5 |
4
|
eleq2i |
|- ( <. B , z >. e. recs ( F ) <-> <. B , z >. e. U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) } ) |
6 |
|
eluniab |
|- ( <. B , z >. e. U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) } <-> E. f ( <. B , z >. e. f /\ E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) ) ) |
7 |
5 6
|
bitri |
|- ( <. B , z >. e. recs ( F ) <-> E. f ( <. B , z >. e. f /\ E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) ) ) |
8 |
|
fnop |
|- ( ( f Fn x /\ <. B , z >. e. f ) -> B e. x ) |
9 |
|
rspe |
|- ( ( x e. On /\ ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) ) -> E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) ) |
10 |
1
|
abeq2i |
|- ( f e. A <-> E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) ) |
11 |
|
elssuni |
|- ( f e. A -> f C_ U. A ) |
12 |
1
|
recsfval |
|- recs ( F ) = U. A |
13 |
11 12
|
sseqtrrdi |
|- ( f e. A -> f C_ recs ( F ) ) |
14 |
10 13
|
sylbir |
|- ( E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) -> f C_ recs ( F ) ) |
15 |
9 14
|
syl |
|- ( ( x e. On /\ ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) ) -> f C_ recs ( F ) ) |
16 |
|
fveq2 |
|- ( y = B -> ( f ` y ) = ( f ` B ) ) |
17 |
|
reseq2 |
|- ( y = B -> ( f |` y ) = ( f |` B ) ) |
18 |
17
|
fveq2d |
|- ( y = B -> ( F ` ( f |` y ) ) = ( F ` ( f |` B ) ) ) |
19 |
16 18
|
eqeq12d |
|- ( y = B -> ( ( f ` y ) = ( F ` ( f |` y ) ) <-> ( f ` B ) = ( F ` ( f |` B ) ) ) ) |
20 |
19
|
rspcv |
|- ( B e. x -> ( A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) -> ( f ` B ) = ( F ` ( f |` B ) ) ) ) |
21 |
|
fndm |
|- ( f Fn x -> dom f = x ) |
22 |
21
|
eleq2d |
|- ( f Fn x -> ( B e. dom f <-> B e. x ) ) |
23 |
1
|
tfrlem7 |
|- Fun recs ( F ) |
24 |
|
funssfv |
|- ( ( Fun recs ( F ) /\ f C_ recs ( F ) /\ B e. dom f ) -> ( recs ( F ) ` B ) = ( f ` B ) ) |
25 |
23 24
|
mp3an1 |
|- ( ( f C_ recs ( F ) /\ B e. dom f ) -> ( recs ( F ) ` B ) = ( f ` B ) ) |
26 |
25
|
adantrl |
|- ( ( f C_ recs ( F ) /\ ( ( f Fn x /\ x e. On ) /\ B e. dom f ) ) -> ( recs ( F ) ` B ) = ( f ` B ) ) |
27 |
21
|
eleq1d |
|- ( f Fn x -> ( dom f e. On <-> x e. On ) ) |
28 |
|
onelss |
|- ( dom f e. On -> ( B e. dom f -> B C_ dom f ) ) |
29 |
27 28
|
syl6bir |
|- ( f Fn x -> ( x e. On -> ( B e. dom f -> B C_ dom f ) ) ) |
30 |
29
|
imp31 |
|- ( ( ( f Fn x /\ x e. On ) /\ B e. dom f ) -> B C_ dom f ) |
31 |
|
fun2ssres |
|- ( ( Fun recs ( F ) /\ f C_ recs ( F ) /\ B C_ dom f ) -> ( recs ( F ) |` B ) = ( f |` B ) ) |
32 |
31
|
fveq2d |
|- ( ( Fun recs ( F ) /\ f C_ recs ( F ) /\ B C_ dom f ) -> ( F ` ( recs ( F ) |` B ) ) = ( F ` ( f |` B ) ) ) |
33 |
23 32
|
mp3an1 |
|- ( ( f C_ recs ( F ) /\ B C_ dom f ) -> ( F ` ( recs ( F ) |` B ) ) = ( F ` ( f |` B ) ) ) |
34 |
30 33
|
sylan2 |
|- ( ( f C_ recs ( F ) /\ ( ( f Fn x /\ x e. On ) /\ B e. dom f ) ) -> ( F ` ( recs ( F ) |` B ) ) = ( F ` ( f |` B ) ) ) |
35 |
26 34
|
eqeq12d |
|- ( ( f C_ recs ( F ) /\ ( ( f Fn x /\ x e. On ) /\ B e. dom f ) ) -> ( ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) <-> ( f ` B ) = ( F ` ( f |` B ) ) ) ) |
36 |
35
|
exbiri |
|- ( f C_ recs ( F ) -> ( ( ( f Fn x /\ x e. On ) /\ B e. dom f ) -> ( ( f ` B ) = ( F ` ( f |` B ) ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) ) ) |
37 |
36
|
com3l |
|- ( ( ( f Fn x /\ x e. On ) /\ B e. dom f ) -> ( ( f ` B ) = ( F ` ( f |` B ) ) -> ( f C_ recs ( F ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) ) ) |
38 |
37
|
exp31 |
|- ( f Fn x -> ( x e. On -> ( B e. dom f -> ( ( f ` B ) = ( F ` ( f |` B ) ) -> ( f C_ recs ( F ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) ) ) ) ) |
39 |
38
|
com34 |
|- ( f Fn x -> ( x e. On -> ( ( f ` B ) = ( F ` ( f |` B ) ) -> ( B e. dom f -> ( f C_ recs ( F ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) ) ) ) ) |
40 |
39
|
com24 |
|- ( f Fn x -> ( B e. dom f -> ( ( f ` B ) = ( F ` ( f |` B ) ) -> ( x e. On -> ( f C_ recs ( F ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) ) ) ) ) |
41 |
22 40
|
sylbird |
|- ( f Fn x -> ( B e. x -> ( ( f ` B ) = ( F ` ( f |` B ) ) -> ( x e. On -> ( f C_ recs ( F ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) ) ) ) ) |
42 |
41
|
com3l |
|- ( B e. x -> ( ( f ` B ) = ( F ` ( f |` B ) ) -> ( f Fn x -> ( x e. On -> ( f C_ recs ( F ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) ) ) ) ) |
43 |
20 42
|
syld |
|- ( B e. x -> ( A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) -> ( f Fn x -> ( x e. On -> ( f C_ recs ( F ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) ) ) ) ) |
44 |
43
|
com24 |
|- ( B e. x -> ( x e. On -> ( f Fn x -> ( A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) -> ( f C_ recs ( F ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) ) ) ) ) |
45 |
44
|
imp4d |
|- ( B e. x -> ( ( x e. On /\ ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) ) -> ( f C_ recs ( F ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) ) ) |
46 |
15 45
|
mpdi |
|- ( B e. x -> ( ( x e. On /\ ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) ) |
47 |
8 46
|
syl |
|- ( ( f Fn x /\ <. B , z >. e. f ) -> ( ( x e. On /\ ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) ) |
48 |
47
|
exp4d |
|- ( ( f Fn x /\ <. B , z >. e. f ) -> ( x e. On -> ( f Fn x -> ( A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) ) ) ) |
49 |
48
|
ex |
|- ( f Fn x -> ( <. B , z >. e. f -> ( x e. On -> ( f Fn x -> ( A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) ) ) ) ) |
50 |
49
|
com4r |
|- ( f Fn x -> ( f Fn x -> ( <. B , z >. e. f -> ( x e. On -> ( A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) ) ) ) ) |
51 |
50
|
pm2.43i |
|- ( f Fn x -> ( <. B , z >. e. f -> ( x e. On -> ( A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) ) ) ) |
52 |
51
|
com3l |
|- ( <. B , z >. e. f -> ( x e. On -> ( f Fn x -> ( A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) ) ) ) |
53 |
52
|
imp4a |
|- ( <. B , z >. e. f -> ( x e. On -> ( ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) ) ) |
54 |
53
|
rexlimdv |
|- ( <. B , z >. e. f -> ( E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) ) |
55 |
54
|
imp |
|- ( ( <. B , z >. e. f /\ E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) |
56 |
55
|
exlimiv |
|- ( E. f ( <. B , z >. e. f /\ E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) |
57 |
7 56
|
sylbi |
|- ( <. B , z >. e. recs ( F ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) |
58 |
57
|
exlimiv |
|- ( E. z <. B , z >. e. recs ( F ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) |
59 |
3 58
|
syl |
|- ( B e. dom recs ( F ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) |