Description: Cardinal ordering agrees with natural number ordering. (Contributed by NM, 17-Jun-1998)
Ref | Expression | ||
---|---|---|---|
Assertion | nnsdomo | ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ≺ 𝐵 ↔ 𝐴 ⊊ 𝐵 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nndomo | ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ≼ 𝐵 ↔ 𝐴 ⊆ 𝐵 ) ) | |
2 | nneneq | ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵 ) ) | |
3 | 2 | notbid | ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ¬ 𝐴 ≈ 𝐵 ↔ ¬ 𝐴 = 𝐵 ) ) |
4 | 1 3 | anbi12d | ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( 𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵 ) ↔ ( 𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵 ) ) ) |
5 | brsdom | ⊢ ( 𝐴 ≺ 𝐵 ↔ ( 𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵 ) ) | |
6 | dfpss2 | ⊢ ( 𝐴 ⊊ 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵 ) ) | |
7 | 4 5 6 | 3bitr4g | ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ≺ 𝐵 ↔ 𝐴 ⊊ 𝐵 ) ) |