Theorem elwina

Description: Conditions of weak inaccessibility. (Contributed by Mario Carneiro, 22-Jun-2013)

	Ref	Expression
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		elex	$$⊢A\in {\mathrm{Inacc}}_{𝑤}\to A\in \mathrm{V}$$
2		fvex	$$⊢\mathrm{cf}\left(A\right)\in \mathrm{V}$$
3		eleq1	$$⊢\mathrm{cf}\left(A\right)=A\to \left(\mathrm{cf}\left(A\right)\in \mathrm{V}\leftrightarrow A\in \mathrm{V}\right)$$
4	2 3	mpbii	$$⊢\mathrm{cf}\left(A\right)=A\to A\in \mathrm{V}$$
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{V}$$
6		neeq1	$$⊢z=A\to \left(z\ne \varnothing \leftrightarrow A\ne \varnothing \right)$$
7		fveq2	$$⊢z=A\to \mathrm{cf}\left(z\right)=\mathrm{cf}\left(A\right)$$
8		eqeq12	$$⊢\left(\mathrm{cf}\left(z\right)=\mathrm{cf}\left(A\right)\wedge z=A\right)\to \left(\mathrm{cf}\left(z\right)=z\leftrightarrow \mathrm{cf}\left(A\right)=A\right)$$
9	7 8	mpancom	$$⊢z=A\to \left(\mathrm{cf}\left(z\right)=z\leftrightarrow \mathrm{cf}\left(A\right)=A\right)$$
10		rexeq	$$⊢z=A\to \left(\exists y\in zx\prec y\leftrightarrow \exists y\in Ax\prec y\right)$$
11	10	raleqbi1dv	$$⊢z=A\to \left(\forall x\in z\exists y\in zx\prec y\leftrightarrow \forall x\in A\exists y\in Ax\prec y\right)$$
12	6 9 11	3anbi123d	$$⊢z=A\to \left(\left(z\ne \varnothing \wedge \mathrm{cf}\left(z\right)=z\wedge \forall x\in z\exists y\in zx\prec y\right)\leftrightarrow \left(A\ne \varnothing \wedge \mathrm{cf}\left(A\right)=A\wedge \forall x\in A\exists y\in Ax\prec y\right)\right)$$
13		df-wina	$$⊢{\mathrm{Inacc}}_{𝑤}=\left\{z|\left(z\ne \varnothing \wedge \mathrm{cf}\left(z\right)=z\wedge \forall x\in z\exists y\in zx\prec y\right)\right\}$$
14	12 13	elab2g	$$⊢A\in \mathrm{V}\to \left(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)\right)$$
15	1 5 14	pm5.21nii	$$⊢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)$$