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

Metamath Proof Explorer

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 biimtrrid ⊢ ( ( 𝑥 ∩ 𝑦 ) = ∅ → ( ( 𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝑦 ) → 𝑥 = 𝑦 ) )
10 9 jao1i ⊢ ( ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( ( 𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝑦 ) → 𝑥 = 𝑦 ) )
11 3 10 syl6 ⊢ ( Prt 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝑦 ) → 𝑥 = 𝑦 ) ) )