Metamath Proof Explorer

Theorem 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 ∈ Univ ∧ A ∈ U → 𝒫 A ∈ U

Proof

Step Hyp Ref Expression
1 elgrug ⊢ U ∈ Univ → U ∈ Univ ↔ Tr ⁡ U ∧ ∀ y ∈ U 𝒫 y ∈ U ∧ ∀ x ∈ U y x ∈ U ∧ ∀ x ∈ U y ⋃ ran ⁡ x ∈ U
2 1 ibi ⊢ U ∈ Univ → Tr ⁡ U ∧ ∀ y ∈ U 𝒫 y ∈ U ∧ ∀ x ∈ U y x ∈ U ∧ ∀ x ∈ U y ⋃ ran ⁡ x ∈ U
3 2 simprd ⊢ U ∈ Univ → ∀ y ∈ U 𝒫 y ∈ U ∧ ∀ x ∈ U y x ∈ U ∧ ∀ x ∈ U y ⋃ ran ⁡ x ∈ U
4 simp1 ⊢ 𝒫 y ∈ U ∧ ∀ x ∈ U y x ∈ U ∧ ∀ x ∈ U y ⋃ ran ⁡ x ∈ U → 𝒫 y ∈ U
5 4 ralimi ⊢ ∀ y ∈ U 𝒫 y ∈ U ∧ ∀ x ∈ U y x ∈ U ∧ ∀ x ∈ U y ⋃ ran ⁡ x ∈ U → ∀ y ∈ U 𝒫 y ∈ U
6 pweq ⊢ y = A → 𝒫 y = 𝒫 A
7 6 eleq1d ⊢ y = A → 𝒫 y ∈ U ↔ 𝒫 A ∈ U
8 7 rspccv ⊢ ∀ y ∈ U 𝒫 y ∈ U → A ∈ U → 𝒫 A ∈ U
9 3 5 8 3syl ⊢ U ∈ Univ → A ∈ U → 𝒫 A ∈ U
10 9 imp ⊢ U ∈ Univ ∧ A ∈ U → 𝒫 A ∈ U