Metamath Proof Explorer

Theorem nndomog

Description: Cardinal ordering agrees with ordinal number ordering when the smaller number is a natural number. Compare with nndomo when both are natural numbers. (Contributed by NM, 17-Jun-1998) Generalize from nndomo . (Revised by RP, 5-Nov-2023)

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

Proof

Step Hyp Ref Expression
1 php2 ⊢ A ∈ ω ∧ B ⊂ A → B ≺ A
2 1 ex ⊢ A ∈ ω → B ⊂ A → B ≺ A
3 domnsym ⊢ A ≼ B → ¬ B ≺ A
4 2 3 nsyli ⊢ A ∈ ω → A ≼ B → ¬ B ⊂ A
5 4 adantr ⊢ A ∈ ω ∧ B ∈ On → A ≼ B → ¬ B ⊂ A
6 nnord ⊢ A ∈ ω → Ord ⁡ A
7 eloni ⊢ B ∈ On → Ord ⁡ B
8 ordtri1 ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ⊆ B ↔ ¬ B ∈ A
9 ordelpss ⊢ Ord ⁡ B ∧ Ord ⁡ A → B ∈ A ↔ B ⊂ A
10 9 ancoms ⊢ Ord ⁡ A ∧ Ord ⁡ B → B ∈ A ↔ B ⊂ A
11 10 notbid ⊢ Ord ⁡ A ∧ Ord ⁡ B → ¬ B ∈ A ↔ ¬ B ⊂ A
12 8 11 bitrd ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ⊆ B ↔ ¬ B ⊂ A
13 6 7 12 syl2an ⊢ A ∈ ω ∧ B ∈ On → A ⊆ B ↔ ¬ B ⊂ A
14 5 13 sylibrd ⊢ A ∈ ω ∧ B ∈ On → A ≼ B → A ⊆ B
15 ssdomg ⊢ B ∈ On → A ⊆ B → A ≼ B
16 15 adantl ⊢ A ∈ ω ∧ B ∈ On → A ⊆ B → A ≼ B
17 14 16 impbid ⊢ A ∈ ω ∧ B ∈ On → A ≼ B ↔ A ⊆ B