Step |
Hyp |
Ref |
Expression |
1 |
|
elex |
|- ( A e. B -> A e. _V ) |
2 |
|
isinfcard |
|- ( ( _om C_ ( F ` x ) /\ ( card ` ( F ` x ) ) = ( F ` x ) ) <-> ( F ` x ) e. ran aleph ) |
3 |
2
|
bicomi |
|- ( ( F ` x ) e. ran aleph <-> ( _om C_ ( F ` x ) /\ ( card ` ( F ` x ) ) = ( F ` x ) ) ) |
4 |
3
|
simplbi |
|- ( ( F ` x ) e. ran aleph -> _om C_ ( F ` x ) ) |
5 |
|
ffn |
|- ( F : A --> ( _om u. ran aleph ) -> F Fn A ) |
6 |
|
fnfvelrn |
|- ( ( F Fn A /\ x e. A ) -> ( F ` x ) e. ran F ) |
7 |
6
|
ex |
|- ( F Fn A -> ( x e. A -> ( F ` x ) e. ran F ) ) |
8 |
|
fnima |
|- ( F Fn A -> ( F " A ) = ran F ) |
9 |
8
|
eleq2d |
|- ( F Fn A -> ( ( F ` x ) e. ( F " A ) <-> ( F ` x ) e. ran F ) ) |
10 |
7 9
|
sylibrd |
|- ( F Fn A -> ( x e. A -> ( F ` x ) e. ( F " A ) ) ) |
11 |
|
elssuni |
|- ( ( F ` x ) e. ( F " A ) -> ( F ` x ) C_ U. ( F " A ) ) |
12 |
10 11
|
syl6 |
|- ( F Fn A -> ( x e. A -> ( F ` x ) C_ U. ( F " A ) ) ) |
13 |
12
|
imp |
|- ( ( F Fn A /\ x e. A ) -> ( F ` x ) C_ U. ( F " A ) ) |
14 |
5 13
|
sylan |
|- ( ( F : A --> ( _om u. ran aleph ) /\ x e. A ) -> ( F ` x ) C_ U. ( F " A ) ) |
15 |
4 14
|
sylan9ssr |
|- ( ( ( F : A --> ( _om u. ran aleph ) /\ x e. A ) /\ ( F ` x ) e. ran aleph ) -> _om C_ U. ( F " A ) ) |
16 |
15
|
anasss |
|- ( ( F : A --> ( _om u. ran aleph ) /\ ( x e. A /\ ( F ` x ) e. ran aleph ) ) -> _om C_ U. ( F " A ) ) |
17 |
16
|
a1i |
|- ( A e. _V -> ( ( F : A --> ( _om u. ran aleph ) /\ ( x e. A /\ ( F ` x ) e. ran aleph ) ) -> _om C_ U. ( F " A ) ) ) |
18 |
|
carduniima |
|- ( A e. _V -> ( F : A --> ( _om u. ran aleph ) -> U. ( F " A ) e. ( _om u. ran aleph ) ) ) |
19 |
|
iscard3 |
|- ( ( card ` U. ( F " A ) ) = U. ( F " A ) <-> U. ( F " A ) e. ( _om u. ran aleph ) ) |
20 |
18 19
|
syl6ibr |
|- ( A e. _V -> ( F : A --> ( _om u. ran aleph ) -> ( card ` U. ( F " A ) ) = U. ( F " A ) ) ) |
21 |
20
|
adantrd |
|- ( A e. _V -> ( ( F : A --> ( _om u. ran aleph ) /\ ( x e. A /\ ( F ` x ) e. ran aleph ) ) -> ( card ` U. ( F " A ) ) = U. ( F " A ) ) ) |
22 |
17 21
|
jcad |
|- ( A e. _V -> ( ( F : A --> ( _om u. ran aleph ) /\ ( x e. A /\ ( F ` x ) e. ran aleph ) ) -> ( _om C_ U. ( F " A ) /\ ( card ` U. ( F " A ) ) = U. ( F " A ) ) ) ) |
23 |
|
isinfcard |
|- ( ( _om C_ U. ( F " A ) /\ ( card ` U. ( F " A ) ) = U. ( F " A ) ) <-> U. ( F " A ) e. ran aleph ) |
24 |
22 23
|
syl6ib |
|- ( A e. _V -> ( ( F : A --> ( _om u. ran aleph ) /\ ( x e. A /\ ( F ` x ) e. ran aleph ) ) -> U. ( F " A ) e. ran aleph ) ) |
25 |
24
|
exp4d |
|- ( A e. _V -> ( F : A --> ( _om u. ran aleph ) -> ( x e. A -> ( ( F ` x ) e. ran aleph -> U. ( F " A ) e. ran aleph ) ) ) ) |
26 |
25
|
imp |
|- ( ( A e. _V /\ F : A --> ( _om u. ran aleph ) ) -> ( x e. A -> ( ( F ` x ) e. ran aleph -> U. ( F " A ) e. ran aleph ) ) ) |
27 |
26
|
rexlimdv |
|- ( ( A e. _V /\ F : A --> ( _om u. ran aleph ) ) -> ( E. x e. A ( F ` x ) e. ran aleph -> U. ( F " A ) e. ran aleph ) ) |
28 |
27
|
expimpd |
|- ( A e. _V -> ( ( F : A --> ( _om u. ran aleph ) /\ E. x e. A ( F ` x ) e. ran aleph ) -> U. ( F " A ) e. ran aleph ) ) |
29 |
1 28
|
syl |
|- ( A e. B -> ( ( F : A --> ( _om u. ran aleph ) /\ E. x e. A ( F ` x ) e. ran aleph ) -> U. ( F " A ) e. ran aleph ) ) |