Metamath Proof Explorer


Theorem nnsdomgOLD

Description: Obsolete version of nnsdomg as of 7-Jan-2025. (Contributed by NM, 15-Jun-1998) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion nnsdomgOLD
|- ( ( _om e. _V /\ A e. _om ) -> A ~< _om )

Proof

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 )