prtlem14

		Ref	Expression
	Assertion	prtlem14	$⊢ Prt A \to ((x \in A \land y \in A) \to ((w \in x \land w \in y) \to x = y))$

Step	Hyp	Ref	Expression
1		df-prt	$⊢ Prt A \leftrightarrow \forall x \in A \forall y \in A (x = y \lor x \cap y = \emptyset)$
2		rsp2	$⊢ \forall x \in A \forall y \in A (x = y \lor x \cap y = \emptyset) \to ((x \in A \land y \in A) \to (x = y \lor x \cap y = \emptyset))$
3	1 2	sylbi	$⊢ Prt A \to ((x \in A \land y \in A) \to (x = y \lor x \cap y = \emptyset))$
4		elin	$⊢ w \in (x \cap y) \leftrightarrow (w \in x \land w \in y)$
5		eq0	$⊢ x \cap y = \emptyset \leftrightarrow \forall w \neg w \in (x \cap y)$
6		sp	$⊢ \forall w \neg w \in (x \cap y) \to \neg w \in (x \cap y)$
7	5 6	sylbi	$⊢ x \cap y = \emptyset \to \neg w \in (x \cap y)$
8	7	pm2.21d	$⊢ x \cap y = \emptyset \to (w \in (x \cap y) \to x = y)$
9	4 8	biimtrrid	$⊢ x \cap y = \emptyset \to ((w \in x \land w \in y) \to x = y)$
10	9	jao1i	$⊢ (x = y \lor x \cap y = \emptyset) \to ((w \in x \land w \in y) \to x = y)$
11	3 10	syl6	$⊢ Prt A \to ((x \in A \land y \in A) \to ((w \in x \land w \in y) \to x = y))$

Metamath Proof Explorer