Theorem grothpw

Description: Derive the Axiom of Power Sets ax-pow from the Tarski-Grothendieck axiom ax-groth . That it follows is mentioned by Bob Solovay at http://www.cs.nyu.edu/pipermail/fom/2008-March/012783.html . Note that ax-pow is not used by the proof. (Contributed by Gérard Lang, 22-Jun-2009) (New usage is discouraged.)

	Ref	Expression
Assertion	grothpw	⊢ ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 )

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
15		axpweq	⊢ ( 𝒫 𝑥 ∈ V ↔ ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )
16	14 15	mpbi	⊢ ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 )