Metamath Proof Explorer

Theorem nnsdomo

Description: Cardinal ordering agrees with natural number ordering. (Contributed by NM, 17-Jun-1998)

Ref Expression
Assertion nnsdomo ⊢ A ∈ ω ∧ B ∈ ω → A ≺ B ↔ A ⊂ B

Proof

Step Hyp Ref Expression
1 nndomo ⊢ A ∈ ω ∧ B ∈ ω → A ≼ B ↔ A ⊆ B
2 nneneq ⊢ A ∈ ω ∧ B ∈ ω → A ≈ B ↔ A = B
3 2 notbid ⊢ A ∈ ω ∧ B ∈ ω → ¬ A ≈ B ↔ ¬ A = B
4 1 3 anbi12d ⊢ A ∈ ω ∧ B ∈ ω → A ≼ B ∧ ¬ A ≈ B ↔ A ⊆ B ∧ ¬ A = B
5 brsdom ⊢ A ≺ B ↔ A ≼ B ∧ ¬ A ≈ B
6 dfpss2 ⊢ A ⊂ B ↔ A ⊆ B ∧ ¬ A = B
7 4 5 6 3bitr4g ⊢ A ∈ ω ∧ B ∈ ω → A ≺ B ↔ A ⊂ B