Theorem prtlem14

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

	Ref	Expression
Assertion	prtlem14	⊢ ( Prt 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝑦 ) → 𝑥 = 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-prt	⊢ ( Prt 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
2		rsp2	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) )
3	1 2	sylbi	⊢ ( Prt 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) )
4		elin	⊢ ( 𝑤 ∈ ( 𝑥 ∩ 𝑦 ) ↔ ( 𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝑦 ) )
5		eq0	⊢ ( ( 𝑥 ∩ 𝑦 ) = ∅ ↔ ∀ 𝑤 ¬ 𝑤 ∈ ( 𝑥 ∩ 𝑦 ) )
6		sp	⊢ ( ∀ 𝑤 ¬ 𝑤 ∈ ( 𝑥 ∩ 𝑦 ) → ¬ 𝑤 ∈ ( 𝑥 ∩ 𝑦 ) )
7	5 6	sylbi	⊢ ( ( 𝑥 ∩ 𝑦 ) = ∅ → ¬ 𝑤 ∈ ( 𝑥 ∩ 𝑦 ) )
8	7	pm2.21d	⊢ ( ( 𝑥 ∩ 𝑦 ) = ∅ → ( 𝑤 ∈ ( 𝑥 ∩ 𝑦 ) → 𝑥 = 𝑦 ) )
9	4 8	syl5bir	⊢ ( ( 𝑥 ∩ 𝑦 ) = ∅ → ( ( 𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝑦 ) → 𝑥 = 𝑦 ) )
10	9	jao1i	⊢ ( ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( ( 𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝑦 ) → 𝑥 = 𝑦 ) )
11	3 10	syl6	⊢ ( Prt 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝑦 ) → 𝑥 = 𝑦 ) ) )