Metamath Proof Explorer


Theorem nnsdomo

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

Ref Expression
Assertion nnsdomo ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴𝐵𝐴𝐵 ) )

Proof

Step Hyp Ref Expression
1 nndomo ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴𝐵𝐴𝐵 ) )
2 nneneq ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴𝐵𝐴 = 𝐵 ) )
3 2 notbid ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ¬ 𝐴𝐵 ↔ ¬ 𝐴 = 𝐵 ) )
4 1 3 anbi12d ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( 𝐴𝐵 ∧ ¬ 𝐴𝐵 ) ↔ ( 𝐴𝐵 ∧ ¬ 𝐴 = 𝐵 ) ) )
5 brsdom ( 𝐴𝐵 ↔ ( 𝐴𝐵 ∧ ¬ 𝐴𝐵 ) )
6 dfpss2 ( 𝐴𝐵 ↔ ( 𝐴𝐵 ∧ ¬ 𝐴 = 𝐵 ) )
7 4 5 6 3bitr4g ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴𝐵𝐴𝐵 ) )