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