Metamath Proof Explorer

Theorem nndomo

Description: Cardinal ordering agrees with natural number ordering. Example 3 of Enderton p. 146. (Contributed by NM, 17-Jun-1998)

Ref Expression
Assertion nndomo ⊢ A ∈ ω ∧ B ∈ ω → A ≼ B ↔ A ⊆ B

Proof

Step Hyp Ref Expression
1 nnon ⊢ B ∈ ω → B ∈ On
2 nndomog ⊢ A ∈ ω ∧ B ∈ On → A ≼ B ↔ A ⊆ B
3 1 2 sylan2 ⊢ A ∈ ω ∧ B ∈ ω → A ≼ B ↔ A ⊆ B