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 ∈ ω ∧ B ∈ ω → A ∈ B ↔ A ≺ B

Proof

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