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	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ) → 𝒫 𝐴 ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		elgrug	⊢ ( 𝑈 ∈ Univ → ( 𝑈 ∈ Univ ↔ ( Tr 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝒫 𝑦 ∈ 𝑈 ∧ ∀ 𝑥 ∈ 𝑈 { 𝑦 , 𝑥 } ∈ 𝑈 ∧ ∀ 𝑥 ∈ ( 𝑈 ↑m 𝑦 ) ∪ ran 𝑥 ∈ 𝑈 ) ) ) )
2	1	ibi	⊢ ( 𝑈 ∈ Univ → ( Tr 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 ( 𝒫 𝑦 ∈ 𝑈 ∧ ∀ 𝑥 ∈ 𝑈 { 𝑦 , 𝑥 } ∈ 𝑈 ∧ ∀ 𝑥 ∈ ( 𝑈 ↑m 𝑦 ) ∪ ran 𝑥 ∈ 𝑈 ) ) )
3	2	simprd	⊢ ( 𝑈 ∈ Univ → ∀ 𝑦 ∈ 𝑈 ( 𝒫 𝑦 ∈ 𝑈 ∧ ∀ 𝑥 ∈ 𝑈 { 𝑦 , 𝑥 } ∈ 𝑈 ∧ ∀ 𝑥 ∈ ( 𝑈 ↑m 𝑦 ) ∪ ran 𝑥 ∈ 𝑈 ) )
4		simp1	⊢ ( ( 𝒫 𝑦 ∈ 𝑈 ∧ ∀ 𝑥 ∈ 𝑈 { 𝑦 , 𝑥 } ∈ 𝑈 ∧ ∀ 𝑥 ∈ ( 𝑈 ↑m 𝑦 ) ∪ ran 𝑥 ∈ 𝑈 ) → 𝒫 𝑦 ∈ 𝑈 )
5	4	ralimi	⊢ ( ∀ 𝑦 ∈ 𝑈 ( 𝒫 𝑦 ∈ 𝑈 ∧ ∀ 𝑥 ∈ 𝑈 { 𝑦 , 𝑥 } ∈ 𝑈 ∧ ∀ 𝑥 ∈ ( 𝑈 ↑m 𝑦 ) ∪ ran 𝑥 ∈ 𝑈 ) → ∀ 𝑦 ∈ 𝑈 𝒫 𝑦 ∈ 𝑈 )
6		pweq	⊢ ( 𝑦 = 𝐴 → 𝒫 𝑦 = 𝒫 𝐴 )
7	6	eleq1d	⊢ ( 𝑦 = 𝐴 → ( 𝒫 𝑦 ∈ 𝑈 ↔ 𝒫 𝐴 ∈ 𝑈 ) )
8	7	rspccv	⊢ ( ∀ 𝑦 ∈ 𝑈 𝒫 𝑦 ∈ 𝑈 → ( 𝐴 ∈ 𝑈 → 𝒫 𝐴 ∈ 𝑈 ) )
9	3 5 8	3syl	⊢ ( 𝑈 ∈ Univ → ( 𝐴 ∈ 𝑈 → 𝒫 𝐴 ∈ 𝑈 ) )
10	9	imp	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ) → 𝒫 𝐴 ∈ 𝑈 )