Step |
Hyp |
Ref |
Expression |
1 |
|
ssdomg |
|- ( _om e. _V -> ( A C_ _om -> A ~<_ _om ) ) |
2 |
|
ordom |
|- Ord _om |
3 |
|
ordelss |
|- ( ( Ord _om /\ A e. _om ) -> A C_ _om ) |
4 |
2 3
|
mpan |
|- ( A e. _om -> A C_ _om ) |
5 |
1 4
|
impel |
|- ( ( _om e. _V /\ A e. _om ) -> A ~<_ _om ) |
6 |
|
ominf |
|- -. _om e. Fin |
7 |
|
ensym |
|- ( A ~~ _om -> _om ~~ A ) |
8 |
|
breq2 |
|- ( x = A -> ( _om ~~ x <-> _om ~~ A ) ) |
9 |
8
|
rspcev |
|- ( ( A e. _om /\ _om ~~ A ) -> E. x e. _om _om ~~ x ) |
10 |
|
isfi |
|- ( _om e. Fin <-> E. x e. _om _om ~~ x ) |
11 |
9 10
|
sylibr |
|- ( ( A e. _om /\ _om ~~ A ) -> _om e. Fin ) |
12 |
11
|
ex |
|- ( A e. _om -> ( _om ~~ A -> _om e. Fin ) ) |
13 |
7 12
|
syl5 |
|- ( A e. _om -> ( A ~~ _om -> _om e. Fin ) ) |
14 |
6 13
|
mtoi |
|- ( A e. _om -> -. A ~~ _om ) |
15 |
14
|
adantl |
|- ( ( _om e. _V /\ A e. _om ) -> -. A ~~ _om ) |
16 |
|
brsdom |
|- ( A ~< _om <-> ( A ~<_ _om /\ -. A ~~ _om ) ) |
17 |
5 15 16
|
sylanbrc |
|- ( ( _om e. _V /\ A e. _om ) -> A ~< _om ) |