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

Metamath Proof Explorer

Theorem prtlem17

Description: Lemma for prter2 . (Contributed by Rodolfo Medina, 15-Oct-2010)

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

Proof

Step	Hyp	Ref	Expression
1		df-rex	$⊢ \exists y \in A (z \in y \land w \in y) \leftrightarrow \exists y (y \in A \land (z \in y \land w \in y))$
2		an32	$⊢ ((x \in A \land y \in A) \land z \in x) \leftrightarrow ((x \in A \land z \in x) \land y \in A)$
3		prtlem14	$⊢ Prt A \to ((x \in A \land y \in A) \to ((z \in x \land z \in y) \to x = y))$
4		elequ2	$⊢ x = y \to (w \in x \leftrightarrow w \in y)$
5	4	biimprd	$⊢ x = y \to (w \in y \to w \in x)$
6	3 5	syl8	$⊢ Prt A \to ((x \in A \land y \in A) \to ((z \in x \land z \in y) \to (w \in y \to w \in x)))$
7	6	exp4a	$⊢ Prt A \to ((x \in A \land y \in A) \to (z \in x \to (z \in y \to (w \in y \to w \in x))))$
8	7	impd	$⊢ Prt A \to (((x \in A \land y \in A) \land z \in x) \to (z \in y \to (w \in y \to w \in x)))$
9	2 8	biimtrrid	$⊢ Prt A \to (((x \in A \land z \in x) \land y \in A) \to (z \in y \to (w \in y \to w \in x)))$
10	9	expd	$⊢ Prt A \to ((x \in A \land z \in x) \to (y \in A \to (z \in y \to (w \in y \to w \in x))))$
11	10	imp5a	$⊢ Prt A \to ((x \in A \land z \in x) \to (y \in A \to ((z \in y \land w \in y) \to w \in x)))$
12	11	imp4b	$⊢ (Prt A \land (x \in A \land z \in x)) \to ((y \in A \land (z \in y \land w \in y)) \to w \in x)$
13	12	exlimdv	$⊢ (Prt A \land (x \in A \land z \in x)) \to (\exists y (y \in A \land (z \in y \land w \in y)) \to w \in x)$
14	1 13	biimtrid	$⊢ (Prt A \land (x \in A \land z \in x)) \to (\exists y \in A (z \in y \land w \in y) \to w \in x)$
15	14	ex	$⊢ Prt A \to ((x \in A \land z \in x) \to (\exists y \in A (z \in y \land w \in y) \to w \in x))$