Metamath Proof Explorer

Theorem dfuniv2

Description: Alternative definition of Univ using only simple defined symbols. (Contributed by Rohan Ridenour, 10-Oct-2024)

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

Proof

Step	Hyp	Ref	Expression
1		grumnueq	$⊢ Univ = \{k \| \forall l \in k (𝒫 l \subseteq k \land \forall m \exists n \in k (𝒫 l \subseteq n \land \forall p \in l (\exists q \in k (p \in q \land q \in m) \to \exists r \in m (p \in r \land ⋃ r \subseteq n))))\}$
2	1	ismnu	$⊢ y \in V \to (y \in Univ \leftrightarrow \forall z \in y (𝒫 z \subseteq y \land \forall f \exists w \in y (𝒫 z \subseteq w \land \forall i \in z (\exists v \in y (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w)))))$
3	2	elv	$⊢ y \in Univ \leftrightarrow \forall z \in y (𝒫 z \subseteq y \land \forall f \exists w \in y (𝒫 z \subseteq w \land \forall i \in z (\exists v \in y (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w))))$
4		ismnushort	$⊢ \forall f \in 𝒫 y \exists w \in y (𝒫 z \subseteq y \cap w \land z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 w)) \leftrightarrow (𝒫 z \subseteq y \land \forall f \exists w \in y (𝒫 z \subseteq w \land \forall i \in z (\exists v \in y (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w))))$
5	4	ralbii	$⊢ \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)) \leftrightarrow \forall z \in y (𝒫 z \subseteq y \land \forall f \exists w \in y (𝒫 z \subseteq w \land \forall i \in z (\exists v \in y (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w))))$
6	3 5	bitr4i	$⊢ 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))$
7	6	eqabi	$⊢ 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))\}$