This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ On ) → ( 𝐴 ≼ 𝐵 ↔ 𝐴 ⊆ 𝐵 ) )

Proof

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