Theorem sucomisnotcard

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

	Ref	Expression
Assertion	sucomisnotcard	⊢ ¬ ( ω +o 1o ) ∈ ran card

Proof

Step	Hyp	Ref	Expression
1		omelon	⊢ ω ∈ On
2		sucidg	⊢ ( ω ∈ On → ω ∈ suc ω )
3	1 2	ax-mp	⊢ ω ∈ suc ω
4		omensuc	⊢ ω ≈ suc ω
5		breq1	⊢ ( 𝑥 = ω → ( 𝑥 ≈ suc ω ↔ ω ≈ suc ω ) )
6	5	rspcev	⊢ ( ( ω ∈ suc ω ∧ ω ≈ suc ω ) → ∃ 𝑥 ∈ suc ω 𝑥 ≈ suc ω )
7	3 4 6	mp2an	⊢ ∃ 𝑥 ∈ suc ω 𝑥 ≈ suc ω
8		dfrex2	⊢ ( ∃ 𝑥 ∈ suc ω 𝑥 ≈ suc ω ↔ ¬ ∀ 𝑥 ∈ suc ω ¬ 𝑥 ≈ suc ω )
9	7 8	mpbi	⊢ ¬ ∀ 𝑥 ∈ suc ω ¬ 𝑥 ≈ suc ω
10	9	intnan	⊢ ¬ ( suc ω ∈ On ∧ ∀ 𝑥 ∈ suc ω ¬ 𝑥 ≈ suc ω )
11		oa1suc	⊢ ( ω ∈ On → ( ω +o 1o ) = suc ω )
12	1 11	ax-mp	⊢ ( ω +o 1o ) = suc ω
13	12	eleq1i	⊢ ( ( ω +o 1o ) ∈ ran card ↔ suc ω ∈ ran card )
14		elrncard	⊢ ( suc ω ∈ ran card ↔ ( suc ω ∈ On ∧ ∀ 𝑥 ∈ suc ω ¬ 𝑥 ≈ suc ω ) )
15	13 14	sylbb	⊢ ( ( ω +o 1o ) ∈ ran card → ( suc ω ∈ On ∧ ∀ 𝑥 ∈ suc ω ¬ 𝑥 ≈ suc ω ) )
16	10 15	mto	⊢ ¬ ( ω +o 1o ) ∈ ran card