sucomisnotcard

Description: _om +o 1o is not a cardinal number. (Contributed by RP, 1-Oct-2023)

		Ref	Expression
	Assertion	sucomisnotcard	$⊢ \neg ω +_{𝑜} 1_{𝑜} \in ran card$

Step	Hyp	Ref	Expression
1		omelon	$⊢ ω \in On$
2		sucidg	$⊢ ω \in On \to ω \in suc ω$
3	1 2	ax-mp	$⊢ ω \in suc ω$
4		omensuc	$⊢ ω \approx suc ω$
5		breq1	$⊢ x = ω \to (x \approx suc ω \leftrightarrow ω \approx suc ω)$
6	5	rspcev	$⊢ (ω \in suc ω \land ω \approx suc ω) \to \exists x \in suc ω x \approx suc ω$
7	3 4 6	mp2an	$⊢ \exists x \in suc ω x \approx suc ω$
8		dfrex2	$⊢ \exists x \in suc ω x \approx suc ω \leftrightarrow \neg \forall x \in suc ω \neg x \approx suc ω$
9	7 8	mpbi	$⊢ \neg \forall x \in suc ω \neg x \approx suc ω$
10	9	intnan	$⊢ \neg (suc ω \in On \land \forall x \in suc ω \neg x \approx suc ω)$
11		oa1suc	$⊢ ω \in On \to ω +_{𝑜} 1_{𝑜} = suc ω$
12	1 11	ax-mp	$⊢ ω +_{𝑜} 1_{𝑜} = suc ω$
13	12	eleq1i	$⊢ ω +_{𝑜} 1_{𝑜} \in ran card \leftrightarrow suc ω \in ran card$
14		elrncard	$⊢ suc ω \in ran card \leftrightarrow (suc ω \in On \land \forall x \in suc ω \neg x \approx suc ω)$
15	13 14	sylbb	$⊢ ω +_{𝑜} 1_{𝑜} \in ran card \to (suc ω \in On \land \forall x \in suc ω \neg x \approx suc ω)$
16	10 15	mto	$⊢ \neg ω +_{𝑜} 1_{𝑜} \in ran card$

Metamath Proof Explorer