Step |
Hyp |
Ref |
Expression |
1 |
|
ffun |
|- ( F : A --> ( _om u. ran aleph ) -> Fun F ) |
2 |
|
funimaexg |
|- ( ( Fun F /\ A e. B ) -> ( F " A ) e. _V ) |
3 |
1 2
|
sylan |
|- ( ( F : A --> ( _om u. ran aleph ) /\ A e. B ) -> ( F " A ) e. _V ) |
4 |
3
|
expcom |
|- ( A e. B -> ( F : A --> ( _om u. ran aleph ) -> ( F " A ) e. _V ) ) |
5 |
|
fimass |
|- ( F : A --> ( _om u. ran aleph ) -> ( F " A ) C_ ( _om u. ran aleph ) ) |
6 |
5
|
sseld |
|- ( F : A --> ( _om u. ran aleph ) -> ( x e. ( F " A ) -> x e. ( _om u. ran aleph ) ) ) |
7 |
|
iscard3 |
|- ( ( card ` x ) = x <-> x e. ( _om u. ran aleph ) ) |
8 |
6 7
|
syl6ibr |
|- ( F : A --> ( _om u. ran aleph ) -> ( x e. ( F " A ) -> ( card ` x ) = x ) ) |
9 |
8
|
ralrimiv |
|- ( F : A --> ( _om u. ran aleph ) -> A. x e. ( F " A ) ( card ` x ) = x ) |
10 |
|
carduni |
|- ( ( F " A ) e. _V -> ( A. x e. ( F " A ) ( card ` x ) = x -> ( card ` U. ( F " A ) ) = U. ( F " A ) ) ) |
11 |
9 10
|
syl5 |
|- ( ( F " A ) e. _V -> ( F : A --> ( _om u. ran aleph ) -> ( card ` U. ( F " A ) ) = U. ( F " A ) ) ) |
12 |
4 11
|
syli |
|- ( A e. B -> ( F : A --> ( _om u. ran aleph ) -> ( card ` U. ( F " A ) ) = U. ( F " A ) ) ) |
13 |
|
iscard3 |
|- ( ( card ` U. ( F " A ) ) = U. ( F " A ) <-> U. ( F " A ) e. ( _om u. ran aleph ) ) |
14 |
12 13
|
syl6ib |
|- ( A e. B -> ( F : A --> ( _om u. ran aleph ) -> U. ( F " A ) e. ( _om u. ran aleph ) ) ) |