Theorem inawina

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

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

Proof

Step	Hyp	Ref	Expression
1		cfon	$$⊢\mathrm{cf}\left(A\right)\in \mathrm{On}$$
2		eleq1	$$⊢\mathrm{cf}\left(A\right)=A\to \left(\mathrm{cf}\left(A\right)\in \mathrm{On}\leftrightarrow A\in \mathrm{On}\right)$$
3	1 2	mpbii	$$⊢\mathrm{cf}\left(A\right)=A\to A\in \mathrm{On}$$
4	3	3ad2ant2	$$⊢\left(A\ne \varnothing \wedge \mathrm{cf}\left(A\right)=A\wedge \forall x\in A𝒫x\prec A\right)\to A\in \mathrm{On}$$
5		idd	$$⊢A\in \mathrm{On}\to \left(A\ne \varnothing \to A\ne \varnothing \right)$$
6		idd	$$⊢A\in \mathrm{On}\to \left(\mathrm{cf}\left(A\right)=A\to \mathrm{cf}\left(A\right)=A\right)$$
7		inawinalem	$$⊢A\in \mathrm{On}\to \left(\forall x\in A𝒫x\prec A\to \forall x\in A\exists y\in Ax\prec y\right)$$
8	5 6 7	3anim123d	$$⊢A\in \mathrm{On}\to \left(\left(A\ne \varnothing \wedge \mathrm{cf}\left(A\right)=A\wedge \forall x\in A𝒫x\prec A\right)\to \left(A\ne \varnothing \wedge \mathrm{cf}\left(A\right)=A\wedge \forall x\in A\exists y\in Ax\prec y\right)\right)$$
9	4 8	mpcom	$$⊢\left(A\ne \varnothing \wedge \mathrm{cf}\left(A\right)=A\wedge \forall x\in A𝒫x\prec A\right)\to \left(A\ne \varnothing \wedge \mathrm{cf}\left(A\right)=A\wedge \forall x\in A\exists y\in Ax\prec y\right)$$
10		elina	$$⊢A\in \mathrm{Inacc}\leftrightarrow \left(A\ne \varnothing \wedge \mathrm{cf}\left(A\right)=A\wedge \forall x\in A𝒫x\prec A\right)$$
11		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)$$
12	9 10 11	3imtr4i	$$⊢A\in \mathrm{Inacc}\to A\in {\mathrm{Inacc}}_{𝑤}$$