Step |
Hyp |
Ref |
Expression |
1 |
|
isfinite2 |
|- ( A ~< _om -> A e. Fin ) |
2 |
|
isfinite2 |
|- ( x ~< _om -> x e. Fin ) |
3 |
2
|
ralimi |
|- ( A. x e. A x ~< _om -> A. x e. A x e. Fin ) |
4 |
|
dfss3 |
|- ( A C_ Fin <-> A. x e. A x e. Fin ) |
5 |
3 4
|
sylibr |
|- ( A. x e. A x ~< _om -> A C_ Fin ) |
6 |
|
unifi |
|- ( ( A e. Fin /\ A C_ Fin ) -> U. A e. Fin ) |
7 |
1 5 6
|
syl2an |
|- ( ( A ~< _om /\ A. x e. A x ~< _om ) -> U. A e. Fin ) |
8 |
|
fin2inf |
|- ( A ~< _om -> _om e. _V ) |
9 |
8
|
adantr |
|- ( ( A ~< _om /\ A. x e. A x ~< _om ) -> _om e. _V ) |
10 |
|
isfiniteg |
|- ( _om e. _V -> ( U. A e. Fin <-> U. A ~< _om ) ) |
11 |
9 10
|
syl |
|- ( ( A ~< _om /\ A. x e. A x ~< _om ) -> ( U. A e. Fin <-> U. A ~< _om ) ) |
12 |
7 11
|
mpbid |
|- ( ( A ~< _om /\ A. x e. A x ~< _om ) -> U. A ~< _om ) |