alephord2i

Description: Ordering property of the aleph function. Theorem 66 of Suppes p. 229. (Contributed by NM, 25-Oct-2003)

		Ref	Expression
	Assertion	alephord2i	$⊢ B \in On \to (A \in B \to ℵ (A) \in ℵ (B))$

Step	Hyp	Ref	Expression
1		onelon	$⊢ (B \in On \land A \in B) \to A \in On$
2		alephord2	$⊢ (A \in On \land B \in On) \to (A \in B \leftrightarrow ℵ (A) \in ℵ (B))$
3	2	biimpd	$⊢ (A \in On \land B \in On) \to (A \in B \to ℵ (A) \in ℵ (B))$
4	3	expimpd	$⊢ A \in On \to ((B \in On \land A \in B) \to ℵ (A) \in ℵ (B))$
5	1 4	mpcom	$⊢ (B \in On \land A \in B) \to ℵ (A) \in ℵ (B)$
6	5	ex	$⊢ B \in On \to (A \in B \to ℵ (A) \in ℵ (B))$

Metamath Proof Explorer