Metamath Proof Explorer

Theorem elgrug

Description: Properties of a Grothendieck universe. (Contributed by Mario Carneiro, 9-Jun-2013)

		Ref	Expression
	Assertion	elgrug	$⊢ U \in V \to (U \in Univ \leftrightarrow (Tr U \land \forall x \in U (𝒫 x \in U \land \forall y \in U \{x, y\} \in U \land \forall y \in (U^{x}) ⋃ ran y \in U)))$

Proof

Step	Hyp	Ref	Expression
1		treq	$⊢ u = U \to (Tr u \leftrightarrow Tr U)$
2		eleq2	$⊢ u = U \to (𝒫 x \in u \leftrightarrow 𝒫 x \in U)$
3		eleq2	$⊢ u = U \to (\{x, y\} \in u \leftrightarrow \{x, y\} \in U)$
4	3	raleqbi1dv	$⊢ u = U \to (\forall y \in u \{x, y\} \in u \leftrightarrow \forall y \in U \{x, y\} \in U)$
5		oveq1	$⊢ u = U \to u^{x} = U^{x}$
6		eleq2	$⊢ u = U \to (⋃ ran y \in u \leftrightarrow ⋃ ran y \in U)$
7	5 6	raleqbidv	$⊢ u = U \to (\forall y \in (u^{x}) ⋃ ran y \in u \leftrightarrow \forall y \in (U^{x}) ⋃ ran y \in U)$
8	2 4 7	3anbi123d	$⊢ u = U \to ((𝒫 x \in u \land \forall y \in u \{x, y\} \in u \land \forall y \in (u^{x}) ⋃ ran y \in u) \leftrightarrow (𝒫 x \in U \land \forall y \in U \{x, y\} \in U \land \forall y \in (U^{x}) ⋃ ran y \in U))$
9	8	raleqbi1dv	$⊢ u = U \to (\forall x \in u (𝒫 x \in u \land \forall y \in u \{x, y\} \in u \land \forall y \in (u^{x}) ⋃ ran y \in u) \leftrightarrow \forall x \in U (𝒫 x \in U \land \forall y \in U \{x, y\} \in U \land \forall y \in (U^{x}) ⋃ ran y \in U))$
10	1 9	anbi12d	$⊢ u = U \to ((Tr u \land \forall x \in u (𝒫 x \in u \land \forall y \in u \{x, y\} \in u \land \forall y \in (u^{x}) ⋃ ran y \in u)) \leftrightarrow (Tr U \land \forall x \in U (𝒫 x \in U \land \forall y \in U \{x, y\} \in U \land \forall y \in (U^{x}) ⋃ ran y \in U)))$
11		df-gru	$⊢ Univ = \{u \| (Tr u \land \forall x \in u (𝒫 x \in u \land \forall y \in u \{x, y\} \in u \land \forall y \in (u^{x}) ⋃ ran y \in u))\}$
12	10 11	elab2g	$⊢ U \in V \to (U \in Univ \leftrightarrow (Tr U \land \forall x \in U (𝒫 x \in U \land \forall y \in U \{x, y\} \in U \land \forall y \in (U^{x}) ⋃ ran y \in U)))$