Theorem rr-grothshort

Description: A shorter equivalent of ax-groth than rr-groth using a few more simple defined symbols. (Contributed by Rohan Ridenour, 8-Oct-2024)

	Ref	Expression
Assertion	rr-grothshort	$$⊢\exists y\left(x\in y\wedge \forall z\in y\forall f\in 𝒫y\exists w\in y\left(𝒫z\subseteq y\cap w\wedge z\cap \bigcup f\subseteq \bigcup \left(f\cap 𝒫𝒫w\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		gruex	$$⊢\exists y\in \mathrm{Univ}x\in y$$
2	1	ax-gen	$$⊢\forall x\exists y\in \mathrm{Univ}x\in y$$
3		rr-grothshortbi	$$⊢\forall x\exists y\in \mathrm{Univ}x\in y\leftrightarrow \forall x\exists y\left(x\in y\wedge \forall z\in y\forall f\in 𝒫y\exists w\in y\left(𝒫z\subseteq y\cap w\wedge z\cap \bigcup f\subseteq \bigcup \left(f\cap 𝒫𝒫w\right)\right)\right)$$
4	2 3	mpbi	$$⊢\forall x\exists y\left(x\in y\wedge \forall z\in y\forall f\in 𝒫y\exists w\in y\left(𝒫z\subseteq y\cap w\wedge z\cap \bigcup f\subseteq \bigcup \left(f\cap 𝒫𝒫w\right)\right)\right)$$
5	4	spi	$$⊢\exists y\left(x\in y\wedge \forall z\in y\forall f\in 𝒫y\exists w\in y\left(𝒫z\subseteq y\cap w\wedge z\cap \bigcup f\subseteq \bigcup \left(f\cap 𝒫𝒫w\right)\right)\right)$$