grupw

Description: A Grothendieck universe contains the powerset of each of its members. (Contributed by Mario Carneiro, 9-Jun-2013)

		Ref	Expression
	Assertion	grupw	$⊢ (U \in Univ \land A \in U) \to 𝒫 A \in U$

Step	Hyp	Ref	Expression
1		elgrug	$⊢ U \in Univ \to (U \in Univ \leftrightarrow (Tr U \land \forall y \in U (𝒫 y \in U \land \forall x \in U \{y, x\} \in U \land \forall x \in (U^{y}) ⋃ ran x \in U)))$
2	1	ibi	$⊢ U \in Univ \to (Tr U \land \forall y \in U (𝒫 y \in U \land \forall x \in U \{y, x\} \in U \land \forall x \in (U^{y}) ⋃ ran x \in U))$
3	2	simprd	$⊢ U \in Univ \to \forall y \in U (𝒫 y \in U \land \forall x \in U \{y, x\} \in U \land \forall x \in (U^{y}) ⋃ ran x \in U)$
4		simp1	$⊢ (𝒫 y \in U \land \forall x \in U \{y, x\} \in U \land \forall x \in (U^{y}) ⋃ ran x \in U) \to 𝒫 y \in U$
5	4	ralimi	$⊢ \forall y \in U (𝒫 y \in U \land \forall x \in U \{y, x\} \in U \land \forall x \in (U^{y}) ⋃ ran x \in U) \to \forall y \in U 𝒫 y \in U$
6		pweq	$⊢ y = A \to 𝒫 y = 𝒫 A$
7	6	eleq1d	$⊢ y = A \to (𝒫 y \in U \leftrightarrow 𝒫 A \in U)$
8	7	rspccv	$⊢ \forall y \in U 𝒫 y \in U \to (A \in U \to 𝒫 A \in U)$
9	3 5 8	3syl	$⊢ U \in Univ \to (A \in U \to 𝒫 A \in U)$
10	9	imp	$⊢ (U \in Univ \land A \in U) \to 𝒫 A \in U$

Metamath Proof Explorer