This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nnsdomel

Description: Strict dominance and elementhood are the same for finite ordinals. (Contributed by Stefan O'Rear, 2-Nov-2014)

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

Proof

Step Hyp Ref Expression
1 cardnn 
 |-  ( A e. _om -> ( card ` A ) = A )
2 cardnn 
 |-  ( B e. _om -> ( card ` B ) = B )
3 eleq12 
 |-  ( ( ( card ` A ) = A /\ ( card ` B ) = B ) -> ( ( card ` A ) e. ( card ` B ) <-> A e. B ) )
4 1 2 3 syl2an 
 |-  ( ( A e. _om /\ B e. _om ) -> ( ( card ` A ) e. ( card ` B ) <-> A e. B ) )
5 nnon 
 |-  ( A e. _om -> A e. On )
6 onenon 
 |-  ( A e. On -> A e. dom card )
7 5 6 syl 
 |-  ( A e. _om -> A e. dom card )
8 nnon 
 |-  ( B e. _om -> B e. On )
9 onenon 
 |-  ( B e. On -> B e. dom card )
10 8 9 syl 
 |-  ( B e. _om -> B e. dom card )
11 cardsdom2 
 |-  ( ( A e. dom card /\ B e. dom card ) -> ( ( card ` A ) e. ( card ` B ) <-> A ~< B ) )
12 7 10 11 syl2an 
 |-  ( ( A e. _om /\ B e. _om ) -> ( ( card ` A ) e. ( card ` B ) <-> A ~< B ) )
13 4 12 bitr3d 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A e. B <-> A ~< B ) )