Metamath Proof Explorer

Theorem rr-grothshortbi

Description: Express "every set is contained in a Grothendieck universe" in a short form while avoiding complicated definitions. (Contributed by Rohan Ridenour, 8-Oct-2024)

		Ref	Expression
	Assertion	rr-grothshortbi	$⊢ \forall x \exists y \in Univ x \in y \leftrightarrow \forall x \exists y (x \in y \land \forall z \in y \forall f \in 𝒫 y \exists w \in y (𝒫 z \subseteq y \cap w \land z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 w)))$

Proof

Step	Hyp	Ref	Expression
1		df-rex	$⊢ \exists y \in Univ x \in y \leftrightarrow \exists y (y \in Univ \land x \in y)$
2		exancom	$⊢ \exists y (y \in Univ \land x \in y) \leftrightarrow \exists y (x \in y \land y \in Univ)$
3		dfuniv2	$⊢ Univ = \{y \| \forall z \in y \forall f \in 𝒫 y \exists w \in y (𝒫 z \subseteq y \cap w \land z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 w))\}$
4	3	eqabri	$⊢ y \in Univ \leftrightarrow \forall z \in y \forall f \in 𝒫 y \exists w \in y (𝒫 z \subseteq y \cap w \land z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 w))$
5	4	anbi2i	$⊢ (x \in y \land y \in Univ) \leftrightarrow (x \in y \land \forall z \in y \forall f \in 𝒫 y \exists w \in y (𝒫 z \subseteq y \cap w \land z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 w)))$
6	5	exbii	$⊢ \exists y (x \in y \land y \in Univ) \leftrightarrow \exists y (x \in y \land \forall z \in y \forall f \in 𝒫 y \exists w \in y (𝒫 z \subseteq y \cap w \land z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 w)))$
7	1 2 6	3bitri	$⊢ \exists y \in Univ x \in y \leftrightarrow \exists y (x \in y \land \forall z \in y \forall f \in 𝒫 y \exists w \in y (𝒫 z \subseteq y \cap w \land z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 w)))$
8	7	albii	$⊢ \forall x \exists y \in Univ x \in y \leftrightarrow \forall x \exists y (x \in y \land \forall z \in y \forall f \in 𝒫 y \exists w \in y (𝒫 z \subseteq y \cap w \land z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 w)))$