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 𝑅 ) → ( ( 𝐴 ∈ [ 𝑥 ] 𝑅 ∧ 𝐴 ∈ [ 𝑦 ] 𝑅 ) → [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 ) ) )