prtlem15

		Ref	Expression
	Assertion	prtlem15	$⊢ Prt A \to (\exists x \in A \exists y \in A ((u \in x \land w \in x) \land (w \in y \land v \in y)) \to \exists z \in A (u \in z \land v \in z))$

Proof

Step	Hyp	Ref	Expression
1		anabs7	$⊢ ((w \in x \land w \in y) \land ((u \in x \land v \in y) \land (w \in x \land w \in y))) \leftrightarrow ((u \in x \land v \in y) \land (w \in x \land w \in y))$
2		an43	$⊢ ((u \in x \land w \in x) \land (w \in y \land v \in y)) \leftrightarrow ((u \in x \land v \in y) \land (w \in x \land w \in y))$
3	2	anbi2i	$⊢ ((w \in x \land w \in y) \land ((u \in x \land w \in x) \land (w \in y \land v \in y))) \leftrightarrow ((w \in x \land w \in y) \land ((u \in x \land v \in y) \land (w \in x \land w \in y)))$
4	1 3 2	3bitr4ri	$⊢ ((u \in x \land w \in x) \land (w \in y \land v \in y)) \leftrightarrow ((w \in x \land w \in y) \land ((u \in x \land w \in x) \land (w \in y \land v \in y)))$
5		prtlem14	$⊢ Prt A \to ((x \in A \land y \in A) \to ((w \in x \land w \in y) \to x = y))$
6		an3	$⊢ ((u \in x \land w \in x) \land (w \in y \land v \in y)) \to (u \in x \land v \in y)$
7		elequ2	$⊢ x = y \to (v \in x \leftrightarrow v \in y)$
8	7	anbi2d	$⊢ x = y \to ((u \in x \land v \in x) \leftrightarrow (u \in x \land v \in y))$
9	6 8	imbitrrid	$⊢ x = y \to (((u \in x \land w \in x) \land (w \in y \land v \in y)) \to (u \in x \land v \in x))$
10	5 9	syl8	$⊢ Prt A \to ((x \in A \land y \in A) \to ((w \in x \land w \in y) \to (((u \in x \land w \in x) \land (w \in y \land v \in y)) \to (u \in x \land v \in x))))$
11	10	imp4a	$⊢ Prt A \to ((x \in A \land y \in A) \to (((w \in x \land w \in y) \land ((u \in x \land w \in x) \land (w \in y \land v \in y))) \to (u \in x \land v \in x)))$
12	4 11	syl7bi	$⊢ Prt A \to ((x \in A \land y \in A) \to (((u \in x \land w \in x) \land (w \in y \land v \in y)) \to (u \in x \land v \in x)))$
13	12	expdimp	$⊢ (Prt A \land x \in A) \to (y \in A \to (((u \in x \land w \in x) \land (w \in y \land v \in y)) \to (u \in x \land v \in x)))$
14	13	rexlimdv	$⊢ (Prt A \land x \in A) \to (\exists y \in A ((u \in x \land w \in x) \land (w \in y \land v \in y)) \to (u \in x \land v \in x))$
15	14	reximdva	$⊢ Prt A \to (\exists x \in A \exists y \in A ((u \in x \land w \in x) \land (w \in y \land v \in y)) \to \exists x \in A (u \in x \land v \in x))$
16		elequ2	$⊢ x = z \to (u \in x \leftrightarrow u \in z)$
17		elequ2	$⊢ x = z \to (v \in x \leftrightarrow v \in z)$
18	16 17	anbi12d	$⊢ x = z \to ((u \in x \land v \in x) \leftrightarrow (u \in z \land v \in z))$
19	18	cbvrexvw	$⊢ \exists x \in A (u \in x \land v \in x) \leftrightarrow \exists z \in A (u \in z \land v \in z)$
20	15 19	imbitrdi	$⊢ Prt A \to (\exists x \in A \exists y \in A ((u \in x \land w \in x) \land (w \in y \land v \in y)) \to \exists z \in A (u \in z \land v \in z))$

Metamath Proof Explorer

Theorem prtlem15

Proof