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	$⊢ 𝒫 x \in V$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (𝒫 z \subseteq y \land \exists w \in y 𝒫 z \subseteq w) \to 𝒫 z \subseteq y$
2	1	ralimi	$⊢ \forall z \in y (𝒫 z \subseteq y \land \exists w \in y 𝒫 z \subseteq w) \to \forall z \in y 𝒫 z \subseteq y$
3		pweq	$⊢ z = x \to 𝒫 z = 𝒫 x$
4	3	sseq1d	$⊢ z = x \to (𝒫 z \subseteq y \leftrightarrow 𝒫 x \subseteq y)$
5	4	rspccv	$⊢ \forall z \in y 𝒫 z \subseteq y \to (x \in y \to 𝒫 x \subseteq y)$
6	2 5	syl	$⊢ \forall z \in y (𝒫 z \subseteq y \land \exists w \in y 𝒫 z \subseteq w) \to (x \in y \to 𝒫 x \subseteq y)$
7	6	anim2i	$⊢ (x \in y \land \forall z \in y (𝒫 z \subseteq y \land \exists w \in y 𝒫 z \subseteq w)) \to (x \in y \land (x \in y \to 𝒫 x \subseteq y))$
8	7	3adant3	$⊢ (x \in y \land \forall z \in y (𝒫 z \subseteq y \land \exists w \in y 𝒫 z \subseteq w) \land \forall z \in 𝒫 y (z \approx y \lor z \in y)) \to (x \in y \land (x \in y \to 𝒫 x \subseteq y))$
9		pm3.35	$⊢ (x \in y \land (x \in y \to 𝒫 x \subseteq y)) \to 𝒫 x \subseteq y$
10		vex	$⊢ y \in V$
11	10	ssex	$⊢ 𝒫 x \subseteq y \to 𝒫 x \in V$
12	8 9 11	3syl	$⊢ (x \in y \land \forall z \in y (𝒫 z \subseteq y \land \exists w \in y 𝒫 z \subseteq w) \land \forall z \in 𝒫 y (z \approx y \lor z \in y)) \to 𝒫 x \in V$
13		axgroth5	$⊢ \exists y (x \in y \land \forall z \in y (𝒫 z \subseteq y \land \exists w \in y 𝒫 z \subseteq w) \land \forall z \in 𝒫 y (z \approx y \lor z \in y))$
14	12 13	exlimiiv	$⊢ 𝒫 x \in V$

Metamath Proof Explorer

Theorem grothpwex

Proof