Theorem winacard

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

	Ref	Expression
Assertion	winacard	$$⊢A\in {\mathrm{Inacc}}_{𝑤}\to \mathrm{card}\left(A\right)=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		cardcf	$$⊢\mathrm{card}\left(\mathrm{cf}\left(A\right)\right)=\mathrm{cf}\left(A\right)$$
3		fveq2	$$⊢\mathrm{cf}\left(A\right)=A\to \mathrm{card}\left(\mathrm{cf}\left(A\right)\right)=\mathrm{card}\left(A\right)$$
4		id	$$⊢\mathrm{cf}\left(A\right)=A\to \mathrm{cf}\left(A\right)=A$$
5	2 3 4	3eqtr3a	$$⊢\mathrm{cf}\left(A\right)=A\to \mathrm{card}\left(A\right)=A$$
6	5	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 \mathrm{card}\left(A\right)=A$$
7	1 6	sylbi	$$⊢A\in {\mathrm{Inacc}}_{𝑤}\to \mathrm{card}\left(A\right)=A$$