Theorem grothpwex

Description: Derive the Axiom of Power Sets from the Tarski-Grothendieck axiom ax-groth . Note that ax-pow is not used by the proof. Use axpweq to obtain ax-pow . Use pwex or pwexg instead. (Contributed by Gérard Lang, 22-Jun-2009) (New usage is discouraged.)

	Ref	Expression
Assertion	grothpwex	⊢ 𝒫 𝑥 ∈ V

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ) → 𝒫 𝑧 ⊆ 𝑦 )
2	1	ralimi	⊢ ( ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ) → ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑦 )
3		pweq	⊢ ( 𝑧 = 𝑥 → 𝒫 𝑧 = 𝒫 𝑥 )
4	3	sseq1d	⊢ ( 𝑧 = 𝑥 → ( 𝒫 𝑧 ⊆ 𝑦 ↔ 𝒫 𝑥 ⊆ 𝑦 ) )
5	4	rspccv	⊢ ( ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑦 → ( 𝑥 ∈ 𝑦 → 𝒫 𝑥 ⊆ 𝑦 ) )
6	2 5	syl	⊢ ( ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ) → ( 𝑥 ∈ 𝑦 → 𝒫 𝑥 ⊆ 𝑦 ) )
7	6	anim2i	⊢ ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ) ) → ( 𝑥 ∈ 𝑦 ∧ ( 𝑥 ∈ 𝑦 → 𝒫 𝑥 ⊆ 𝑦 ) ) )
8	7	3adant3	⊢ ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ) ∧ ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ) → ( 𝑥 ∈ 𝑦 ∧ ( 𝑥 ∈ 𝑦 → 𝒫 𝑥 ⊆ 𝑦 ) ) )
9		pm3.35	⊢ ( ( 𝑥 ∈ 𝑦 ∧ ( 𝑥 ∈ 𝑦 → 𝒫 𝑥 ⊆ 𝑦 ) ) → 𝒫 𝑥 ⊆ 𝑦 )
10		vex	⊢ 𝑦 ∈ V
11	10	ssex	⊢ ( 𝒫 𝑥 ⊆ 𝑦 → 𝒫 𝑥 ∈ V )
12	8 9 11	3syl	⊢ ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ) ∧ ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ) → 𝒫 𝑥 ∈ V )
13		axgroth5	⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ) ∧ ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) )
14	12 13	exlimiiv	⊢ 𝒫 𝑥 ∈ V