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

Metamath Proof Explorer

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 eqtrid ⊢ ( ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) → ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐷 } ) = ∅ )