cardom

Description: The set of natural numbers is a cardinal number. Theorem 18.11 of Monk1 p. 133. (Contributed by NM, 28-Oct-2003)

		Ref	Expression
	Assertion	cardom	$⊢ card (ω) = ω$

Step	Hyp	Ref	Expression
1		omelon	$⊢ ω \in On$
2		oncardid	$⊢ ω \in On \to card (ω) \approx ω$
3	1 2	ax-mp	$⊢ card (ω) \approx ω$
4		nnsdom	$⊢ card (ω) \in ω \to card (ω) ≺ ω$
5		sdomnen	$⊢ card (ω) ≺ ω \to \neg card (ω) \approx ω$
6	4 5	syl	$⊢ card (ω) \in ω \to \neg card (ω) \approx ω$
7	3 6	mt2	$⊢ \neg card (ω) \in ω$
8		cardonle	$⊢ ω \in On \to card (ω) \subseteq ω$
9	1 8	ax-mp	$⊢ card (ω) \subseteq ω$
10		cardon	$⊢ card (ω) \in On$
11	10 1	onsseli	$⊢ card (ω) \subseteq ω \leftrightarrow (card (ω) \in ω \lor card (ω) = ω)$
12	9 11	mpbi	$⊢ (card (ω) \in ω \lor card (ω) = ω)$
13	7 12	mtpor	$⊢ card (ω) = ω$

Metamath Proof Explorer