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 ) )