Theorem cardsucinf

Description: The cardinality of the successor of an infinite ordinal. (Contributed by Mario Carneiro, 11-Jan-2013)

	Ref	Expression
Assertion	cardsucinf	$$⊢\left(A\in \mathrm{On}\wedge \mathrm{\omega }\subseteq A\right)\to \mathrm{card}\left(\mathrm{suc}A\right)=\mathrm{card}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		infensuc	$$⊢\left(A\in \mathrm{On}\wedge \mathrm{\omega }\subseteq A\right)\to A\approx \mathrm{suc}A$$
2		carden2b	$$⊢A\approx \mathrm{suc}A\to \mathrm{card}\left(A\right)=\mathrm{card}\left(\mathrm{suc}A\right)$$
3	1 2	syl	$$⊢\left(A\in \mathrm{On}\wedge \mathrm{\omega }\subseteq A\right)\to \mathrm{card}\left(A\right)=\mathrm{card}\left(\mathrm{suc}A\right)$$
4	3	eqcomd	$$⊢\left(A\in \mathrm{On}\wedge \mathrm{\omega }\subseteq A\right)\to \mathrm{card}\left(\mathrm{suc}A\right)=\mathrm{card}\left(A\right)$$