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	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ∈ 𝐵 ↔ 𝐴 ≺ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		cardnn	⊢ ( 𝐴 ∈ ω → ( card ‘ 𝐴 ) = 𝐴 )
2		cardnn	⊢ ( 𝐵 ∈ ω → ( card ‘ 𝐵 ) = 𝐵 )
3		eleq12	⊢ ( ( ( card ‘ 𝐴 ) = 𝐴 ∧ ( card ‘ 𝐵 ) = 𝐵 ) → ( ( card ‘ 𝐴 ) ∈ ( card ‘ 𝐵 ) ↔ 𝐴 ∈ 𝐵 ) )
4	1 2 3	syl2an	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( card ‘ 𝐴 ) ∈ ( card ‘ 𝐵 ) ↔ 𝐴 ∈ 𝐵 ) )
5		nnon	⊢ ( 𝐴 ∈ ω → 𝐴 ∈ On )
6		onenon	⊢ ( 𝐴 ∈ On → 𝐴 ∈ dom card )
7	5 6	syl	⊢ ( 𝐴 ∈ ω → 𝐴 ∈ dom card )
8		nnon	⊢ ( 𝐵 ∈ ω → 𝐵 ∈ On )
9		onenon	⊢ ( 𝐵 ∈ On → 𝐵 ∈ dom card )
10	8 9	syl	⊢ ( 𝐵 ∈ ω → 𝐵 ∈ dom card )
11		cardsdom2	⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( card ‘ 𝐴 ) ∈ ( card ‘ 𝐵 ) ↔ 𝐴 ≺ 𝐵 ) )
12	7 10 11	syl2an	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( card ‘ 𝐴 ) ∈ ( card ‘ 𝐵 ) ↔ 𝐴 ≺ 𝐵 ) )
13	4 12	bitr3d	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ∈ 𝐵 ↔ 𝐴 ≺ 𝐵 ) )