omssrncard

Description: All natural numbers are cardinals. (Contributed by RP, 1-Oct-2023)

		Ref	Expression
	Assertion	omssrncard	$⊢ ω \subseteq ran card$

Step	Hyp	Ref	Expression
1		nnon	$⊢ x \in ω \to x \in On$
2		onelon	$⊢ (x \in On \land y \in x) \to y \in On$
3		simpl	$⊢ (x \in On \land y \in x) \to x \in On$
4		simpr	$⊢ (x \in On \land y \in x) \to y \in x$
5		onelpss	$⊢ (y \in On \land x \in On) \to (y \in x \leftrightarrow (y \subseteq x \land y \neq x))$
6	5	biimpa	$⊢ ((y \in On \land x \in On) \land y \in x) \to (y \subseteq x \land y \neq x)$
7	2 3 4 6	syl21anc	$⊢ (x \in On \land y \in x) \to (y \subseteq x \land y \neq x)$
8		df-pss	$⊢ y \subset x \leftrightarrow (y \subseteq x \land y \neq x)$
9	7 8	sylibr	$⊢ (x \in On \land y \in x) \to y \subset x$
10	9	ex	$⊢ x \in On \to (y \in x \to y \subset x)$
11	1 10	syl	$⊢ x \in ω \to (y \in x \to y \subset x)$
12	11	imdistani	$⊢ (x \in ω \land y \in x) \to (x \in ω \land y \subset x)$
13		php	$⊢ (x \in ω \land y \subset x) \to \neg x \approx y$
14	12 13	syl	$⊢ (x \in ω \land y \in x) \to \neg x \approx y$
15		ensymb	$⊢ x \approx y \leftrightarrow y \approx x$
16	14 15	sylnib	$⊢ (x \in ω \land y \in x) \to \neg y \approx x$
17	16	ralrimiva	$⊢ x \in ω \to \forall y \in x \neg y \approx x$
18		elrncard	$⊢ x \in ran card \leftrightarrow (x \in On \land \forall y \in x \neg y \approx x)$
19	1 17 18	sylanbrc	$⊢ x \in ω \to x \in ran card$
20	19	ssriv	$⊢ ω \subseteq ran card$

Metamath Proof Explorer