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) Avoid ax-pow . (Revised by BTernaryTau, 29-Nov-2024)

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

Proof

Step Hyp Ref Expression
1 nnfi ⊢ A ∈ ω → A ∈ Fin
2 domnsymfi ⊢ A ∈ Fin ∧ A ≼ B → ¬ B ≺ A
3 1 2 sylan ⊢ A ∈ ω ∧ A ≼ B → ¬ B ≺ A
4 3 ex ⊢ A ∈ ω → A ≼ B → ¬ B ≺ A
5 php2 ⊢ A ∈ ω ∧ B ⊂ A → B ≺ A
6 5 ex ⊢ A ∈ ω → B ⊂ A → B ≺ A
7 4 6 nsyld ⊢ A ∈ ω → A ≼ B → ¬ B ⊂ A
8 7 adantr ⊢ A ∈ ω ∧ B ∈ On → A ≼ B → ¬ B ⊂ A
9 nnord ⊢ A ∈ ω → Ord ⁡ A
10 eloni ⊢ B ∈ On → Ord ⁡ B
11 ordtri1 ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ⊆ B ↔ ¬ B ∈ A
12 ordelpss ⊢ Ord ⁡ B ∧ Ord ⁡ A → B ∈ A ↔ B ⊂ A
13 12 ancoms ⊢ Ord ⁡ A ∧ Ord ⁡ B → B ∈ A ↔ B ⊂ A
14 13 notbid ⊢ Ord ⁡ A ∧ Ord ⁡ B → ¬ B ∈ A ↔ ¬ B ⊂ A
15 11 14 bitrd ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ⊆ B ↔ ¬ B ⊂ A
16 9 10 15 syl2an ⊢ A ∈ ω ∧ B ∈ On → A ⊆ B ↔ ¬ B ⊂ A
17 8 16 sylibrd ⊢ A ∈ ω ∧ B ∈ On → A ≼ B → A ⊆ B
18 ssdomfi2 ⊢ A ∈ Fin ∧ B ∈ On ∧ A ⊆ B → A ≼ B
19 18 3expia ⊢ A ∈ Fin ∧ B ∈ On → A ⊆ B → A ≼ B
20 1 19 sylan ⊢ A ∈ ω ∧ B ∈ On → A ⊆ B → A ≼ B
21 17 20 impbid ⊢ A ∈ ω ∧ B ∈ On → A ≼ B ↔ A ⊆ B