Theorem wunpw

Description: A weak universe is closed under powerset. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	wununi.1	⊢ ( 𝜑 → 𝑈 ∈ WUni )
	wununi.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
Assertion	wunpw	⊢ ( 𝜑 → 𝒫 𝐴 ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		wununi.1	⊢ ( 𝜑 → 𝑈 ∈ WUni )
2		wununi.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
3		pweq	⊢ ( 𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴 )
4	3	eleq1d	⊢ ( 𝑥 = 𝐴 → ( 𝒫 𝑥 ∈ 𝑈 ↔ 𝒫 𝐴 ∈ 𝑈 ) )
5		iswun	⊢ ( 𝑈 ∈ WUni → ( 𝑈 ∈ WUni ↔ ( Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑈 ( ∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) ) ) )
6	5	ibi	⊢ ( 𝑈 ∈ WUni → ( Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑈 ( ∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) ) )
7	6	simp3d	⊢ ( 𝑈 ∈ WUni → ∀ 𝑥 ∈ 𝑈 ( ∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) )
8		simp2	⊢ ( ( ∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) → 𝒫 𝑥 ∈ 𝑈 )
9	8	ralimi	⊢ ( ∀ 𝑥 ∈ 𝑈 ( ∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) → ∀ 𝑥 ∈ 𝑈 𝒫 𝑥 ∈ 𝑈 )
10	1 7 9	3syl	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑈 𝒫 𝑥 ∈ 𝑈 )
11	4 10 2	rspcdva	⊢ ( 𝜑 → 𝒫 𝐴 ∈ 𝑈 )