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

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