Theorem winaon

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

	Ref	Expression
Assertion	winaon	$$⊢A\in {\mathrm{Inacc}}_{𝑤}\to A\in \mathrm{On}$$

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	4	3ad2ant2	$$⊢\left(A\ne \varnothing \wedge \mathrm{cf}\left(A\right)=A\wedge \forall x\in A\exists y\in Ax\prec y\right)\to A\in \mathrm{On}$$
6	1 5	sylbi	$$⊢A\in {\mathrm{Inacc}}_{𝑤}\to A\in \mathrm{On}$$