axgroth6

Description: The Tarski-Grothendieck axiom using abbreviations. This version is called Tarski's axiom: given a set x , there exists a set y containing x , the subsets of the members of y , the power sets of the members of y , and the subsets of y of cardinality less than that of y . (Contributed by NM, 21-Jun-2009)

		Ref	Expression
	Assertion	axgroth6	$⊢ \exists y (x \in y \land \forall z \in y (𝒫 z \subseteq y \land 𝒫 z \in y) \land \forall z \in 𝒫 y (z ≺ y \to z \in y))$

Proof

Step	Hyp	Ref	Expression
1		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))$
2		biid	$⊢ x \in y \leftrightarrow x \in y$
3		pweq	$⊢ z = v \to 𝒫 z = 𝒫 v$
4	3	sseq1d	$⊢ z = v \to (𝒫 z \subseteq y \leftrightarrow 𝒫 v \subseteq y)$
5	4	cbvralvw	$⊢ \forall z \in y 𝒫 z \subseteq y \leftrightarrow \forall v \in y 𝒫 v \subseteq y$
6		ssid	$⊢ 𝒫 z \subseteq 𝒫 z$
7		sseq2	$⊢ w = 𝒫 z \to (𝒫 z \subseteq w \leftrightarrow 𝒫 z \subseteq 𝒫 z)$
8	7	rspcev	$⊢ (𝒫 z \in y \land 𝒫 z \subseteq 𝒫 z) \to \exists w \in y 𝒫 z \subseteq w$
9	6 8	mpan2	$⊢ 𝒫 z \in y \to \exists w \in y 𝒫 z \subseteq w$
10		pweq	$⊢ v = w \to 𝒫 v = 𝒫 w$
11	10	sseq1d	$⊢ v = w \to (𝒫 v \subseteq y \leftrightarrow 𝒫 w \subseteq y)$
12	11	rspccv	$⊢ \forall v \in y 𝒫 v \subseteq y \to (w \in y \to 𝒫 w \subseteq y)$
13		pwss	$⊢ 𝒫 w \subseteq y \leftrightarrow \forall v (v \subseteq w \to v \in y)$
14		vpwex	$⊢ 𝒫 z \in V$
15		sseq1	$⊢ v = 𝒫 z \to (v \subseteq w \leftrightarrow 𝒫 z \subseteq w)$
16		eleq1	$⊢ v = 𝒫 z \to (v \in y \leftrightarrow 𝒫 z \in y)$
17	15 16	imbi12d	$⊢ v = 𝒫 z \to ((v \subseteq w \to v \in y) \leftrightarrow (𝒫 z \subseteq w \to 𝒫 z \in y))$
18	14 17	spcv	$⊢ \forall v (v \subseteq w \to v \in y) \to (𝒫 z \subseteq w \to 𝒫 z \in y)$
19	13 18	sylbi	$⊢ 𝒫 w \subseteq y \to (𝒫 z \subseteq w \to 𝒫 z \in y)$
20	12 19	syl6	$⊢ \forall v \in y 𝒫 v \subseteq y \to (w \in y \to (𝒫 z \subseteq w \to 𝒫 z \in y))$
21	20	rexlimdv	$⊢ \forall v \in y 𝒫 v \subseteq y \to (\exists w \in y 𝒫 z \subseteq w \to 𝒫 z \in y)$
22	9 21	impbid2	$⊢ \forall v \in y 𝒫 v \subseteq y \to (𝒫 z \in y \leftrightarrow \exists w \in y 𝒫 z \subseteq w)$
23	22	ralbidv	$⊢ \forall v \in y 𝒫 v \subseteq y \to (\forall z \in y 𝒫 z \in y \leftrightarrow \forall z \in y \exists w \in y 𝒫 z \subseteq w)$
24	5 23	sylbi	$⊢ \forall z \in y 𝒫 z \subseteq y \to (\forall z \in y 𝒫 z \in y \leftrightarrow \forall z \in y \exists w \in y 𝒫 z \subseteq w)$
25	24	pm5.32i	$⊢ (\forall z \in y 𝒫 z \subseteq y \land \forall z \in y 𝒫 z \in y) \leftrightarrow (\forall z \in y 𝒫 z \subseteq y \land \forall z \in y \exists w \in y 𝒫 z \subseteq w)$
26		r19.26	$⊢ \forall z \in y (𝒫 z \subseteq y \land 𝒫 z \in y) \leftrightarrow (\forall z \in y 𝒫 z \subseteq y \land \forall z \in y 𝒫 z \in y)$
27		r19.26	$⊢ \forall z \in y (𝒫 z \subseteq y \land \exists w \in y 𝒫 z \subseteq w) \leftrightarrow (\forall z \in y 𝒫 z \subseteq y \land \forall z \in y \exists w \in y 𝒫 z \subseteq w)$
28	25 26 27	3bitr4i	$⊢ \forall z \in y (𝒫 z \subseteq y \land 𝒫 z \in y) \leftrightarrow \forall z \in y (𝒫 z \subseteq y \land \exists w \in y 𝒫 z \subseteq w)$
29		velpw	$⊢ z \in 𝒫 y \leftrightarrow z \subseteq y$
30		impexp	$⊢ ((z \subseteq y \land z ≼ y) \to (\neg z \approx y \to z \in y)) \leftrightarrow (z \subseteq y \to (z ≼ y \to (\neg z \approx y \to z \in y)))$
31		ssdomg	$⊢ y \in V \to (z \subseteq y \to z ≼ y)$
32	31	elv	$⊢ z \subseteq y \to z ≼ y$
33	32	pm4.71i	$⊢ z \subseteq y \leftrightarrow (z \subseteq y \land z ≼ y)$
34	33	imbi1i	$⊢ (z \subseteq y \to (\neg z \approx y \to z \in y)) \leftrightarrow ((z \subseteq y \land z ≼ y) \to (\neg z \approx y \to z \in y))$
35		brsdom	$⊢ z ≺ y \leftrightarrow (z ≼ y \land \neg z \approx y)$
36	35	imbi1i	$⊢ (z ≺ y \to z \in y) \leftrightarrow ((z ≼ y \land \neg z \approx y) \to z \in y)$
37		impexp	$⊢ ((z ≼ y \land \neg z \approx y) \to z \in y) \leftrightarrow (z ≼ y \to (\neg z \approx y \to z \in y))$
38	36 37	bitri	$⊢ (z ≺ y \to z \in y) \leftrightarrow (z ≼ y \to (\neg z \approx y \to z \in y))$
39	38	imbi2i	$⊢ (z \subseteq y \to (z ≺ y \to z \in y)) \leftrightarrow (z \subseteq y \to (z ≼ y \to (\neg z \approx y \to z \in y)))$
40	30 34 39	3bitr4ri	$⊢ (z \subseteq y \to (z ≺ y \to z \in y)) \leftrightarrow (z \subseteq y \to (\neg z \approx y \to z \in y))$
41	40	pm5.74ri	$⊢ z \subseteq y \to ((z ≺ y \to z \in y) \leftrightarrow (\neg z \approx y \to z \in y))$
42		pm4.64	$⊢ (\neg z \approx y \to z \in y) \leftrightarrow (z \approx y \lor z \in y)$
43	41 42	bitrdi	$⊢ z \subseteq y \to ((z ≺ y \to z \in y) \leftrightarrow (z \approx y \lor z \in y))$
44	29 43	sylbi	$⊢ z \in 𝒫 y \to ((z ≺ y \to z \in y) \leftrightarrow (z \approx y \lor z \in y))$
45	44	ralbiia	$⊢ \forall z \in 𝒫 y (z ≺ y \to z \in y) \leftrightarrow \forall z \in 𝒫 y (z \approx y \lor z \in y)$
46	2 28 45	3anbi123i	$⊢ (x \in y \land \forall z \in y (𝒫 z \subseteq y \land 𝒫 z \in y) \land \forall z \in 𝒫 y (z ≺ y \to z \in y)) \leftrightarrow (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))$
47	46	exbii	$⊢ \exists y (x \in y \land \forall z \in y (𝒫 z \subseteq y \land 𝒫 z \in y) \land \forall z \in 𝒫 y (z ≺ y \to z \in y)) \leftrightarrow \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))$
48	1 47	mpbir	$⊢ \exists y (x \in y \land \forall z \in y (𝒫 z \subseteq y \land 𝒫 z \in y) \land \forall z \in 𝒫 y (z ≺ y \to z \in y))$

Metamath Proof Explorer

Theorem axgroth6

Proof