This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem axgroth5

Description: The Tarski-Grothendieck axiom using abbreviations. (Contributed by NM, 22-Jun-2009)

		Ref	Expression
	Assertion	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))$

Proof

Step	Hyp	Ref	Expression
1		ax-groth	$⊢ \exists y (x \in y \land \forall z \in y (\forall w (w \subseteq z \to w \in y) \land \exists w \in y \forall v (v \subseteq z \to v \in w)) \land \forall z (z \subseteq y \to (z \approx y \lor z \in y)))$
2		biid	$⊢ x \in y \leftrightarrow x \in y$
3		pwss	$⊢ 𝒫 z \subseteq y \leftrightarrow \forall w (w \subseteq z \to w \in y)$
4		pwss	$⊢ 𝒫 z \subseteq w \leftrightarrow \forall v (v \subseteq z \to v \in w)$
5	4	rexbii	$⊢ \exists w \in y 𝒫 z \subseteq w \leftrightarrow \exists w \in y \forall v (v \subseteq z \to v \in w)$
6	3 5	anbi12i	$⊢ (𝒫 z \subseteq y \land \exists w \in y 𝒫 z \subseteq w) \leftrightarrow (\forall w (w \subseteq z \to w \in y) \land \exists w \in y \forall v (v \subseteq z \to v \in w))$
7	6	ralbii	$⊢ \forall z \in y (𝒫 z \subseteq y \land \exists w \in y 𝒫 z \subseteq w) \leftrightarrow \forall z \in y (\forall w (w \subseteq z \to w \in y) \land \exists w \in y \forall v (v \subseteq z \to v \in w))$
8		df-ral	$⊢ \forall z \in 𝒫 y (z \approx y \lor z \in y) \leftrightarrow \forall z (z \in 𝒫 y \to (z \approx y \lor z \in y))$
9		velpw	$⊢ z \in 𝒫 y \leftrightarrow z \subseteq y$
10	9	imbi1i	$⊢ (z \in 𝒫 y \to (z \approx y \lor z \in y)) \leftrightarrow (z \subseteq y \to (z \approx y \lor z \in y))$
11	10	albii	$⊢ \forall z (z \in 𝒫 y \to (z \approx y \lor z \in y)) \leftrightarrow \forall z (z \subseteq y \to (z \approx y \lor z \in y))$
12	8 11	bitri	$⊢ \forall z \in 𝒫 y (z \approx y \lor z \in y) \leftrightarrow \forall z (z \subseteq y \to (z \approx y \lor z \in y))$
13	2 7 12	3anbi123i	$⊢ (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)) \leftrightarrow (x \in y \land \forall z \in y (\forall w (w \subseteq z \to w \in y) \land \exists w \in y \forall v (v \subseteq z \to v \in w)) \land \forall z (z \subseteq y \to (z \approx y \lor z \in y)))$
14	13	exbii	$⊢ \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)) \leftrightarrow \exists y (x \in y \land \forall z \in y (\forall w (w \subseteq z \to w \in y) \land \exists w \in y \forall v (v \subseteq z \to v \in w)) \land \forall z (z \subseteq y \to (z \approx y \lor z \in y)))$
15	1 14	mpbir	$⊢ \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))$