Theorem winainf

Description: A weakly inaccessible cardinal is infinite. (Contributed by Mario Carneiro, 29-May-2014)

	Ref	Expression
Assertion	winainf	$$⊢A\in {\mathrm{Inacc}}_{𝑤}\to \mathrm{\omega }\subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		elwina	$$⊢A\in {\mathrm{Inacc}}_{𝑤}\leftrightarrow \left(A\ne \varnothing \wedge \mathrm{cf}\left(A\right)=A\wedge \forall x\in A\exists y\in Ax\prec y\right)$$
2		cfon	$$⊢\mathrm{cf}\left(A\right)\in \mathrm{On}$$
3		eleq1	$$⊢\mathrm{cf}\left(A\right)=A\to \left(\mathrm{cf}\left(A\right)\in \mathrm{On}\leftrightarrow A\in \mathrm{On}\right)$$
4	2 3	mpbii	$$⊢\mathrm{cf}\left(A\right)=A\to A\in \mathrm{On}$$
5		winainflem	$$⊢\left(A\ne \varnothing \wedge A\in \mathrm{On}\wedge \forall x\in A\exists y\in Ax\prec y\right)\to \mathrm{\omega }\subseteq A$$
6	4 5	syl3an2	$$⊢\left(A\ne \varnothing \wedge \mathrm{cf}\left(A\right)=A\wedge \forall x\in A\exists y\in Ax\prec y\right)\to \mathrm{\omega }\subseteq A$$
7	1 6	sylbi	$$⊢A\in {\mathrm{Inacc}}_{𝑤}\to \mathrm{\omega }\subseteq A$$