Metamath Proof Explorer

Theorem alephsdom

Description: If an ordinal is smaller than an initial ordinal, it is strictly dominated by it. (Contributed by Jeff Hankins, 24-Oct-2009) (Proof shortened by Mario Carneiro, 20-Sep-2014)

		Ref	Expression
	Assertion	alephsdom	$⊢ (A \in On \land B \in On) \to (A \in ℵ (B) \leftrightarrow A ≺ ℵ (B))$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (A \in On \land B \in On) \to A \in On$
2		alephon	$⊢ ℵ (B) \in On$
3		onenon	$⊢ ℵ (B) \in On \to ℵ (B) \in dom card$
4	2 3	ax-mp	$⊢ ℵ (B) \in dom card$
5		cardsdomel	$⊢ (A \in On \land ℵ (B) \in dom card) \to (A ≺ ℵ (B) \leftrightarrow A \in card (ℵ (B)))$
6	1 4 5	sylancl	$⊢ (A \in On \land B \in On) \to (A ≺ ℵ (B) \leftrightarrow A \in card (ℵ (B)))$
7		alephcard	$⊢ card (ℵ (B)) = ℵ (B)$
8	7	eleq2i	$⊢ A \in card (ℵ (B)) \leftrightarrow A \in ℵ (B)$
9	6 8	bitr2di	$⊢ (A \in On \land B \in On) \to (A \in ℵ (B) \leftrightarrow A ≺ ℵ (B))$