axgroth4

Description: Alternate version of the Tarski-Grothendieck Axiom. ax-ac is used to derive this version. (Contributed by NM, 16-Apr-2007)

		Ref	Expression
	Assertion	axgroth4	$⊢ \exists y (x \in y \land \forall z \in y \exists v \in y \forall w (w \subseteq z \to w \in (y \cap v)) \land \forall z (z \subseteq y \to ((y ∖ z) ≼ z \lor z \in y)))$

Proof

Step	Hyp	Ref	Expression
1		axgroth3	$⊢ \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 u (u \subseteq z \to u \in w)) \land \forall z (z \subseteq y \to ((y ∖ z) ≼ z \lor z \in y)))$
2		elequ2	$⊢ w = v \to (u \in w \leftrightarrow u \in v)$
3	2	imbi2d	$⊢ w = v \to ((u \subseteq z \to u \in w) \leftrightarrow (u \subseteq z \to u \in v))$
4	3	albidv	$⊢ w = v \to (\forall u (u \subseteq z \to u \in w) \leftrightarrow \forall u (u \subseteq z \to u \in v))$
5	4	cbvrexvw	$⊢ \exists w \in y \forall u (u \subseteq z \to u \in w) \leftrightarrow \exists v \in y \forall u (u \subseteq z \to u \in v)$
6	5	anbi2i	$⊢ (\forall w (w \subseteq z \to w \in y) \land \exists w \in y \forall u (u \subseteq z \to u \in w)) \leftrightarrow (\forall w (w \subseteq z \to w \in y) \land \exists v \in y \forall u (u \subseteq z \to u \in v))$
7		r19.42v	$⊢ \exists v \in y (\forall w (w \subseteq z \to w \in y) \land \forall u (u \subseteq z \to u \in v)) \leftrightarrow (\forall w (w \subseteq z \to w \in y) \land \exists v \in y \forall u (u \subseteq z \to u \in v))$
8		sseq1	$⊢ u = w \to (u \subseteq z \leftrightarrow w \subseteq z)$
9		elequ1	$⊢ u = w \to (u \in v \leftrightarrow w \in v)$
10	8 9	imbi12d	$⊢ u = w \to ((u \subseteq z \to u \in v) \leftrightarrow (w \subseteq z \to w \in v))$
11	10	cbvalvw	$⊢ \forall u (u \subseteq z \to u \in v) \leftrightarrow \forall w (w \subseteq z \to w \in v)$
12	11	anbi2i	$⊢ (\forall w (w \subseteq z \to w \in y) \land \forall u (u \subseteq z \to u \in v)) \leftrightarrow (\forall w (w \subseteq z \to w \in y) \land \forall w (w \subseteq z \to w \in v))$
13		19.26	$⊢ \forall w ((w \subseteq z \to w \in y) \land (w \subseteq z \to w \in v)) \leftrightarrow (\forall w (w \subseteq z \to w \in y) \land \forall w (w \subseteq z \to w \in v))$
14		pm4.76	$⊢ ((w \subseteq z \to w \in y) \land (w \subseteq z \to w \in v)) \leftrightarrow (w \subseteq z \to (w \in y \land w \in v))$
15		elin	$⊢ w \in (y \cap v) \leftrightarrow (w \in y \land w \in v)$
16	15	imbi2i	$⊢ (w \subseteq z \to w \in (y \cap v)) \leftrightarrow (w \subseteq z \to (w \in y \land w \in v))$
17	14 16	bitr4i	$⊢ ((w \subseteq z \to w \in y) \land (w \subseteq z \to w \in v)) \leftrightarrow (w \subseteq z \to w \in (y \cap v))$
18	17	albii	$⊢ \forall w ((w \subseteq z \to w \in y) \land (w \subseteq z \to w \in v)) \leftrightarrow \forall w (w \subseteq z \to w \in (y \cap v))$
19	12 13 18	3bitr2i	$⊢ (\forall w (w \subseteq z \to w \in y) \land \forall u (u \subseteq z \to u \in v)) \leftrightarrow \forall w (w \subseteq z \to w \in (y \cap v))$
20	19	rexbii	$⊢ \exists v \in y (\forall w (w \subseteq z \to w \in y) \land \forall u (u \subseteq z \to u \in v)) \leftrightarrow \exists v \in y \forall w (w \subseteq z \to w \in (y \cap v))$
21	6 7 20	3bitr2i	$⊢ (\forall w (w \subseteq z \to w \in y) \land \exists w \in y \forall u (u \subseteq z \to u \in w)) \leftrightarrow \exists v \in y \forall w (w \subseteq z \to w \in (y \cap v))$
22	21	ralbii	$⊢ \forall z \in y (\forall w (w \subseteq z \to w \in y) \land \exists w \in y \forall u (u \subseteq z \to u \in w)) \leftrightarrow \forall z \in y \exists v \in y \forall w (w \subseteq z \to w \in (y \cap v))$
23	22	3anbi2i	$⊢ (x \in y \land \forall z \in y (\forall w (w \subseteq z \to w \in y) \land \exists w \in y \forall u (u \subseteq z \to u \in w)) \land \forall z (z \subseteq y \to ((y ∖ z) ≼ z \lor z \in y))) \leftrightarrow (x \in y \land \forall z \in y \exists v \in y \forall w (w \subseteq z \to w \in (y \cap v)) \land \forall z (z \subseteq y \to ((y ∖ z) ≼ z \lor z \in y)))$
24	23	exbii	$⊢ \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 u (u \subseteq z \to u \in w)) \land \forall z (z \subseteq y \to ((y ∖ z) ≼ z \lor z \in y))) \leftrightarrow \exists y (x \in y \land \forall z \in y \exists v \in y \forall w (w \subseteq z \to w \in (y \cap v)) \land \forall z (z \subseteq y \to ((y ∖ z) ≼ z \lor z \in y)))$
25	1 24	mpbi	$⊢ \exists y (x \in y \land \forall z \in y \exists v \in y \forall w (w \subseteq z \to w \in (y \cap v)) \land \forall z (z \subseteq y \to ((y ∖ z) ≼ z \lor z \in y)))$

Metamath Proof Explorer

Theorem axgroth4

Proof