Step |
Hyp |
Ref |
Expression |
1 |
|
dfac8alem.2 |
|- F = recs ( G ) |
2 |
|
dfac8alem.3 |
|- G = ( f e. _V |-> ( g ` ( A \ ran f ) ) ) |
3 |
|
elex |
|- ( A e. C -> A e. _V ) |
4 |
|
difss |
|- ( A \ ( F " x ) ) C_ A |
5 |
|
elpw2g |
|- ( A e. _V -> ( ( A \ ( F " x ) ) e. ~P A <-> ( A \ ( F " x ) ) C_ A ) ) |
6 |
4 5
|
mpbiri |
|- ( A e. _V -> ( A \ ( F " x ) ) e. ~P A ) |
7 |
|
neeq1 |
|- ( y = ( A \ ( F " x ) ) -> ( y =/= (/) <-> ( A \ ( F " x ) ) =/= (/) ) ) |
8 |
|
fveq2 |
|- ( y = ( A \ ( F " x ) ) -> ( g ` y ) = ( g ` ( A \ ( F " x ) ) ) ) |
9 |
|
id |
|- ( y = ( A \ ( F " x ) ) -> y = ( A \ ( F " x ) ) ) |
10 |
8 9
|
eleq12d |
|- ( y = ( A \ ( F " x ) ) -> ( ( g ` y ) e. y <-> ( g ` ( A \ ( F " x ) ) ) e. ( A \ ( F " x ) ) ) ) |
11 |
7 10
|
imbi12d |
|- ( y = ( A \ ( F " x ) ) -> ( ( y =/= (/) -> ( g ` y ) e. y ) <-> ( ( A \ ( F " x ) ) =/= (/) -> ( g ` ( A \ ( F " x ) ) ) e. ( A \ ( F " x ) ) ) ) ) |
12 |
11
|
rspcv |
|- ( ( A \ ( F " x ) ) e. ~P A -> ( A. y e. ~P A ( y =/= (/) -> ( g ` y ) e. y ) -> ( ( A \ ( F " x ) ) =/= (/) -> ( g ` ( A \ ( F " x ) ) ) e. ( A \ ( F " x ) ) ) ) ) |
13 |
6 12
|
syl |
|- ( A e. _V -> ( A. y e. ~P A ( y =/= (/) -> ( g ` y ) e. y ) -> ( ( A \ ( F " x ) ) =/= (/) -> ( g ` ( A \ ( F " x ) ) ) e. ( A \ ( F " x ) ) ) ) ) |
14 |
13
|
3imp |
|- ( ( A e. _V /\ A. y e. ~P A ( y =/= (/) -> ( g ` y ) e. y ) /\ ( A \ ( F " x ) ) =/= (/) ) -> ( g ` ( A \ ( F " x ) ) ) e. ( A \ ( F " x ) ) ) |
15 |
1
|
tfr2 |
|- ( x e. On -> ( F ` x ) = ( G ` ( F |` x ) ) ) |
16 |
1
|
tfr1 |
|- F Fn On |
17 |
|
fnfun |
|- ( F Fn On -> Fun F ) |
18 |
16 17
|
ax-mp |
|- Fun F |
19 |
|
vex |
|- x e. _V |
20 |
|
resfunexg |
|- ( ( Fun F /\ x e. _V ) -> ( F |` x ) e. _V ) |
21 |
18 19 20
|
mp2an |
|- ( F |` x ) e. _V |
22 |
|
rneq |
|- ( f = ( F |` x ) -> ran f = ran ( F |` x ) ) |
23 |
|
df-ima |
|- ( F " x ) = ran ( F |` x ) |
24 |
22 23
|
eqtr4di |
|- ( f = ( F |` x ) -> ran f = ( F " x ) ) |
25 |
24
|
difeq2d |
|- ( f = ( F |` x ) -> ( A \ ran f ) = ( A \ ( F " x ) ) ) |
26 |
25
|
fveq2d |
|- ( f = ( F |` x ) -> ( g ` ( A \ ran f ) ) = ( g ` ( A \ ( F " x ) ) ) ) |
27 |
|
fvex |
|- ( g ` ( A \ ( F " x ) ) ) e. _V |
28 |
26 2 27
|
fvmpt |
|- ( ( F |` x ) e. _V -> ( G ` ( F |` x ) ) = ( g ` ( A \ ( F " x ) ) ) ) |
29 |
21 28
|
ax-mp |
|- ( G ` ( F |` x ) ) = ( g ` ( A \ ( F " x ) ) ) |
30 |
15 29
|
eqtrdi |
|- ( x e. On -> ( F ` x ) = ( g ` ( A \ ( F " x ) ) ) ) |
31 |
30
|
eleq1d |
|- ( x e. On -> ( ( F ` x ) e. ( A \ ( F " x ) ) <-> ( g ` ( A \ ( F " x ) ) ) e. ( A \ ( F " x ) ) ) ) |
32 |
14 31
|
syl5ibrcom |
|- ( ( A e. _V /\ A. y e. ~P A ( y =/= (/) -> ( g ` y ) e. y ) /\ ( A \ ( F " x ) ) =/= (/) ) -> ( x e. On -> ( F ` x ) e. ( A \ ( F " x ) ) ) ) |
33 |
32
|
3expia |
|- ( ( A e. _V /\ A. y e. ~P A ( y =/= (/) -> ( g ` y ) e. y ) ) -> ( ( A \ ( F " x ) ) =/= (/) -> ( x e. On -> ( F ` x ) e. ( A \ ( F " x ) ) ) ) ) |
34 |
33
|
com23 |
|- ( ( A e. _V /\ A. y e. ~P A ( y =/= (/) -> ( g ` y ) e. y ) ) -> ( x e. On -> ( ( A \ ( F " x ) ) =/= (/) -> ( F ` x ) e. ( A \ ( F " x ) ) ) ) ) |
35 |
34
|
ralrimiv |
|- ( ( A e. _V /\ A. y e. ~P A ( y =/= (/) -> ( g ` y ) e. y ) ) -> A. x e. On ( ( A \ ( F " x ) ) =/= (/) -> ( F ` x ) e. ( A \ ( F " x ) ) ) ) |
36 |
35
|
ex |
|- ( A e. _V -> ( A. y e. ~P A ( y =/= (/) -> ( g ` y ) e. y ) -> A. x e. On ( ( A \ ( F " x ) ) =/= (/) -> ( F ` x ) e. ( A \ ( F " x ) ) ) ) ) |
37 |
16
|
tz7.49c |
|- ( ( A e. _V /\ A. x e. On ( ( A \ ( F " x ) ) =/= (/) -> ( F ` x ) e. ( A \ ( F " x ) ) ) ) -> E. x e. On ( F |` x ) : x -1-1-onto-> A ) |
38 |
37
|
ex |
|- ( A e. _V -> ( A. x e. On ( ( A \ ( F " x ) ) =/= (/) -> ( F ` x ) e. ( A \ ( F " x ) ) ) -> E. x e. On ( F |` x ) : x -1-1-onto-> A ) ) |
39 |
19
|
f1oen |
|- ( ( F |` x ) : x -1-1-onto-> A -> x ~~ A ) |
40 |
|
isnumi |
|- ( ( x e. On /\ x ~~ A ) -> A e. dom card ) |
41 |
39 40
|
sylan2 |
|- ( ( x e. On /\ ( F |` x ) : x -1-1-onto-> A ) -> A e. dom card ) |
42 |
41
|
rexlimiva |
|- ( E. x e. On ( F |` x ) : x -1-1-onto-> A -> A e. dom card ) |
43 |
38 42
|
syl6 |
|- ( A e. _V -> ( A. x e. On ( ( A \ ( F " x ) ) =/= (/) -> ( F ` x ) e. ( A \ ( F " x ) ) ) -> A e. dom card ) ) |
44 |
36 43
|
syld |
|- ( A e. _V -> ( A. y e. ~P A ( y =/= (/) -> ( g ` y ) e. y ) -> A e. dom card ) ) |
45 |
3 44
|
syl |
|- ( A e. C -> ( A. y e. ~P A ( y =/= (/) -> ( g ` y ) e. y ) -> A e. dom card ) ) |
46 |
45
|
exlimdv |
|- ( A e. C -> ( E. g A. y e. ~P A ( y =/= (/) -> ( g ` y ) e. y ) -> A e. dom card ) ) |