Theorem disjtpsn

Description: The disjoint intersection of an unordered triple and a singleton. (Contributed by AV, 14-Nov-2021)

	Ref	Expression
Assertion	disjtpsn	⊢ ( ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) → ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐷 } ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		df-tp	⊢ { 𝐴 , 𝐵 , 𝐶 } = ( { 𝐴 , 𝐵 } ∪ { 𝐶 } )
2	1	ineq1i	⊢ ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐷 } ) = ( ( { 𝐴 , 𝐵 } ∪ { 𝐶 } ) ∩ { 𝐷 } )
3		disjprsn	⊢ ( ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ) → ( { 𝐴 , 𝐵 } ∩ { 𝐷 } ) = ∅ )
4	3	3adant3	⊢ ( ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) → ( { 𝐴 , 𝐵 } ∩ { 𝐷 } ) = ∅ )
5		disjsn2	⊢ ( 𝐶 ≠ 𝐷 → ( { 𝐶 } ∩ { 𝐷 } ) = ∅ )
6	5	3ad2ant3	⊢ ( ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) → ( { 𝐶 } ∩ { 𝐷 } ) = ∅ )
7	4 6	jca	⊢ ( ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) → ( ( { 𝐴 , 𝐵 } ∩ { 𝐷 } ) = ∅ ∧ ( { 𝐶 } ∩ { 𝐷 } ) = ∅ ) )
8		undisj1	⊢ ( ( ( { 𝐴 , 𝐵 } ∩ { 𝐷 } ) = ∅ ∧ ( { 𝐶 } ∩ { 𝐷 } ) = ∅ ) ↔ ( ( { 𝐴 , 𝐵 } ∪ { 𝐶 } ) ∩ { 𝐷 } ) = ∅ )
9	7 8	sylib	⊢ ( ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) → ( ( { 𝐴 , 𝐵 } ∪ { 𝐶 } ) ∩ { 𝐷 } ) = ∅ )
10	2 9	syl5eq	⊢ ( ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) → ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐷 } ) = ∅ )