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

Metamath Proof Explorer

Theorem disjlem14

Description: Lemma for disjdmqseq , partim2 and petlem via disjlem17 , (general version of the former prtlem14 ). (Contributed by Peter Mazsa, 10-Sep-2021)

Ref Expression
Assertion disjlem14 ( Disj 𝑅 → ( ( 𝑥 ∈ dom 𝑅 ∧ 𝑦 ∈ dom 𝑅 ) → ( ( 𝐴 ∈ [ 𝑥 ] 𝑅 ∧ 𝐴 ∈ [ 𝑦 ] 𝑅 ) → [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 dfdisjALTV5 ⊢ ( Disj 𝑅 ↔ ( ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ dom 𝑅 ( 𝑥 = 𝑦 ∨ ( [ 𝑥 ] 𝑅 ∩ [ 𝑦 ] 𝑅 ) = ∅ ) ∧ Rel 𝑅 ) )
2 1 simplbi ⊢ ( Disj 𝑅 → ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ dom 𝑅 ( 𝑥 = 𝑦 ∨ ( [ 𝑥 ] 𝑅 ∩ [ 𝑦 ] 𝑅 ) = ∅ ) )
3 rsp2 ⊢ ( ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ dom 𝑅 ( 𝑥 = 𝑦 ∨ ( [ 𝑥 ] 𝑅 ∩ [ 𝑦 ] 𝑅 ) = ∅ ) → ( ( 𝑥 ∈ dom 𝑅 ∧ 𝑦 ∈ dom 𝑅 ) → ( 𝑥 = 𝑦 ∨ ( [ 𝑥 ] 𝑅 ∩ [ 𝑦 ] 𝑅 ) = ∅ ) ) )
4 2 3 syl ⊢ ( Disj 𝑅 → ( ( 𝑥 ∈ dom 𝑅 ∧ 𝑦 ∈ dom 𝑅 ) → ( 𝑥 = 𝑦 ∨ ( [ 𝑥 ] 𝑅 ∩ [ 𝑦 ] 𝑅 ) = ∅ ) ) )
5 eceq1 ⊢ ( 𝑥 = 𝑦 → [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 )
6 5 a1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ∈ [ 𝑥 ] 𝑅 ∧ 𝐴 ∈ [ 𝑦 ] 𝑅 ) → [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 ) )
7 elin ⊢ ( 𝐴 ∈ ( [ 𝑥 ] 𝑅 ∩ [ 𝑦 ] 𝑅 ) ↔ ( 𝐴 ∈ [ 𝑥 ] 𝑅 ∧ 𝐴 ∈ [ 𝑦 ] 𝑅 ) )
8 nel02 ⊢ ( ( [ 𝑥 ] 𝑅 ∩ [ 𝑦 ] 𝑅 ) = ∅ → ¬ 𝐴 ∈ ( [ 𝑥 ] 𝑅 ∩ [ 𝑦 ] 𝑅 ) )
9 8 pm2.21d ⊢ ( ( [ 𝑥 ] 𝑅 ∩ [ 𝑦 ] 𝑅 ) = ∅ → ( 𝐴 ∈ ( [ 𝑥 ] 𝑅 ∩ [ 𝑦 ] 𝑅 ) → [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 ) )
10 7 9 biimtrrid ⊢ ( ( [ 𝑥 ] 𝑅 ∩ [ 𝑦 ] 𝑅 ) = ∅ → ( ( 𝐴 ∈ [ 𝑥 ] 𝑅 ∧ 𝐴 ∈ [ 𝑦 ] 𝑅 ) → [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 ) )
11 6 10 jaoi ⊢ ( ( 𝑥 = 𝑦 ∨ ( [ 𝑥 ] 𝑅 ∩ [ 𝑦 ] 𝑅 ) = ∅ ) → ( ( 𝐴 ∈ [ 𝑥 ] 𝑅 ∧ 𝐴 ∈ [ 𝑦 ] 𝑅 ) → [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 ) )
12 4 11 syl6 ⊢ ( Disj 𝑅 → ( ( 𝑥 ∈ dom 𝑅 ∧ 𝑦 ∈ dom 𝑅 ) → ( ( 𝐴 ∈ [ 𝑥 ] 𝑅 ∧ 𝐴 ∈ [ 𝑦 ] 𝑅 ) → [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 ) ) )