Theorem prtlem14

Description: Lemma for prter1 , prter2 and prtex . (Contributed by Rodolfo Medina, 13-Oct-2010)

	Ref	Expression
Assertion	prtlem14	$$⊢\mathrm{Prt}A\to \left(\left(x\in A\wedge y\in A\right)\to \left(\left(w\in x\wedge w\in y\right)\to x=y\right)\right)$$

Proof

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