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