Metamath Proof Explorer

Theorem cardalephex

Description: Every transfinite cardinal is an aleph and vice-versa. Theorem 8A(b) of Enderton p. 213 and its converse. (Contributed by NM, 5-Nov-2003)

		Ref	Expression
	Assertion	cardalephex	$⊢ ω \subseteq A \to (card (A) = A \leftrightarrow \exists x \in On A = ℵ (x))$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (ω \subseteq A \land card (A) = A) \to ω \subseteq A$
2		cardaleph	$⊢ (ω \subseteq A \land card (A) = A) \to A = ℵ (⋂ \{y \in On \| A \subseteq ℵ (y)\})$
3	2	sseq2d	$⊢ (ω \subseteq A \land card (A) = A) \to (ω \subseteq A \leftrightarrow ω \subseteq ℵ (⋂ \{y \in On \| A \subseteq ℵ (y)\}))$
4		alephgeom	$⊢ ⋂ \{y \in On \| A \subseteq ℵ (y)\} \in On \leftrightarrow ω \subseteq ℵ (⋂ \{y \in On \| A \subseteq ℵ (y)\})$
5	3 4	bitr4di	$⊢ (ω \subseteq A \land card (A) = A) \to (ω \subseteq A \leftrightarrow ⋂ \{y \in On \| A \subseteq ℵ (y)\} \in On)$
6	1 5	mpbid	$⊢ (ω \subseteq A \land card (A) = A) \to ⋂ \{y \in On \| A \subseteq ℵ (y)\} \in On$
7		fveq2	$⊢ x = ⋂ \{y \in On \| A \subseteq ℵ (y)\} \to ℵ (x) = ℵ (⋂ \{y \in On \| A \subseteq ℵ (y)\})$
8	7	rspceeqv	$⊢ (⋂ \{y \in On \| A \subseteq ℵ (y)\} \in On \land A = ℵ (⋂ \{y \in On \| A \subseteq ℵ (y)\})) \to \exists x \in On A = ℵ (x)$
9	6 2 8	syl2anc	$⊢ (ω \subseteq A \land card (A) = A) \to \exists x \in On A = ℵ (x)$
10	9	ex	$⊢ ω \subseteq A \to (card (A) = A \to \exists x \in On A = ℵ (x))$
11		alephcard	$⊢ card (ℵ (x)) = ℵ (x)$
12		fveq2	$⊢ A = ℵ (x) \to card (A) = card (ℵ (x))$
13		id	$⊢ A = ℵ (x) \to A = ℵ (x)$
14	11 12 13	3eqtr4a	$⊢ A = ℵ (x) \to card (A) = A$
15	14	rexlimivw	$⊢ \exists x \in On A = ℵ (x) \to card (A) = A$
16	10 15	impbid1	$⊢ ω \subseteq A \to (card (A) = A \leftrightarrow \exists x \in On A = ℵ (x))$