nnsdomo

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

		Ref	Expression
	Assertion	nnsdomo	$⊢ (A \in ω \land B \in ω) \to (A ≺ B \leftrightarrow A \subset B)$

Step	Hyp	Ref	Expression
1		nndomo	$⊢ (A \in ω \land B \in ω) \to (A ≼ B \leftrightarrow A \subseteq B)$
2		nneneq	$⊢ (A \in ω \land B \in ω) \to (A \approx B \leftrightarrow A = B)$
3	2	notbid	$⊢ (A \in ω \land B \in ω) \to (\neg A \approx B \leftrightarrow \neg A = B)$
4	1 3	anbi12d	$⊢ (A \in ω \land B \in ω) \to ((A ≼ B \land \neg A \approx B) \leftrightarrow (A \subseteq B \land \neg A = B))$
5		brsdom	$⊢ A ≺ B \leftrightarrow (A ≼ B \land \neg A \approx B)$
6		dfpss2	$⊢ A \subset B \leftrightarrow (A \subseteq B \land \neg A = B)$
7	4 5 6	3bitr4g	$⊢ (A \in ω \land B \in ω) \to (A ≺ B \leftrightarrow A \subset B)$

Metamath Proof Explorer