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

Metamath Proof Explorer

Theorem disjtp2

Description: Two completely distinct unordered triples are disjoint. (Contributed by AV, 14-Nov-2021)

Ref Expression
Assertion disjtp2 ( ( ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸 ) ∧ ( 𝐴 ≠ 𝐹 ∧ 𝐵 ≠ 𝐹 ∧ 𝐶 ≠ 𝐹 ) ) → ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐷 , 𝐸 , 𝐹 } ) = ∅ )

Proof

Step Hyp Ref Expression
1 df-tp ⊢ { 𝐷 , 𝐸 , 𝐹 } = ( { 𝐷 , 𝐸 } ∪ { 𝐹 } )
2 1 ineq2i ⊢ ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐷 , 𝐸 , 𝐹 } ) = ( { 𝐴 , 𝐵 , 𝐶 } ∩ ( { 𝐷 , 𝐸 } ∪ { 𝐹 } ) )
3 df-tp ⊢ { 𝐴 , 𝐵 , 𝐶 } = ( { 𝐴 , 𝐵 } ∪ { 𝐶 } )
4 3 ineq1i ⊢ ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐷 , 𝐸 } ) = ( ( { 𝐴 , 𝐵 } ∪ { 𝐶 } ) ∩ { 𝐷 , 𝐸 } )
5 3simpa ⊢ ( ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) → ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ) )
6 3simpa ⊢ ( ( 𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸 ) → ( 𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ) )
7 disjpr2 ⊢ ( ( ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ) ) → ( { 𝐴 , 𝐵 } ∩ { 𝐷 , 𝐸 } ) = ∅ )
8 5 6 7 syl2an ⊢ ( ( ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸 ) ) → ( { 𝐴 , 𝐵 } ∩ { 𝐷 , 𝐸 } ) = ∅ )
9 8 3adant3 ⊢ ( ( ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸 ) ∧ ( 𝐴 ≠ 𝐹 ∧ 𝐵 ≠ 𝐹 ∧ 𝐶 ≠ 𝐹 ) ) → ( { 𝐴 , 𝐵 } ∩ { 𝐷 , 𝐸 } ) = ∅ )
10 incom ⊢ ( { 𝐶 } ∩ { 𝐷 , 𝐸 } ) = ( { 𝐷 , 𝐸 } ∩ { 𝐶 } )
11 necom ⊢ ( 𝐶 ≠ 𝐷 ↔ 𝐷 ≠ 𝐶 )
12 11 biimpi ⊢ ( 𝐶 ≠ 𝐷 → 𝐷 ≠ 𝐶 )
13 12 3ad2ant3 ⊢ ( ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) → 𝐷 ≠ 𝐶 )
14 necom ⊢ ( 𝐶 ≠ 𝐸 ↔ 𝐸 ≠ 𝐶 )
15 14 biimpi ⊢ ( 𝐶 ≠ 𝐸 → 𝐸 ≠ 𝐶 )
16 15 3ad2ant3 ⊢ ( ( 𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸 ) → 𝐸 ≠ 𝐶 )
17 disjprsn ⊢ ( ( 𝐷 ≠ 𝐶 ∧ 𝐸 ≠ 𝐶 ) → ( { 𝐷 , 𝐸 } ∩ { 𝐶 } ) = ∅ )
18 13 16 17 syl2an ⊢ ( ( ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸 ) ) → ( { 𝐷 , 𝐸 } ∩ { 𝐶 } ) = ∅ )
19 18 3adant3 ⊢ ( ( ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸 ) ∧ ( 𝐴 ≠ 𝐹 ∧ 𝐵 ≠ 𝐹 ∧ 𝐶 ≠ 𝐹 ) ) → ( { 𝐷 , 𝐸 } ∩ { 𝐶 } ) = ∅ )
20 10 19 eqtrid ⊢ ( ( ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸 ) ∧ ( 𝐴 ≠ 𝐹 ∧ 𝐵 ≠ 𝐹 ∧ 𝐶 ≠ 𝐹 ) ) → ( { 𝐶 } ∩ { 𝐷 , 𝐸 } ) = ∅ )
21 9 20 jca ⊢ ( ( ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸 ) ∧ ( 𝐴 ≠ 𝐹 ∧ 𝐵 ≠ 𝐹 ∧ 𝐶 ≠ 𝐹 ) ) → ( ( { 𝐴 , 𝐵 } ∩ { 𝐷 , 𝐸 } ) = ∅ ∧ ( { 𝐶 } ∩ { 𝐷 , 𝐸 } ) = ∅ ) )
22 undisj1 ⊢ ( ( ( { 𝐴 , 𝐵 } ∩ { 𝐷 , 𝐸 } ) = ∅ ∧ ( { 𝐶 } ∩ { 𝐷 , 𝐸 } ) = ∅ ) ↔ ( ( { 𝐴 , 𝐵 } ∪ { 𝐶 } ) ∩ { 𝐷 , 𝐸 } ) = ∅ )
23 21 22 sylib ⊢ ( ( ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸 ) ∧ ( 𝐴 ≠ 𝐹 ∧ 𝐵 ≠ 𝐹 ∧ 𝐶 ≠ 𝐹 ) ) → ( ( { 𝐴 , 𝐵 } ∪ { 𝐶 } ) ∩ { 𝐷 , 𝐸 } ) = ∅ )
24 4 23 eqtrid ⊢ ( ( ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸 ) ∧ ( 𝐴 ≠ 𝐹 ∧ 𝐵 ≠ 𝐹 ∧ 𝐶 ≠ 𝐹 ) ) → ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐷 , 𝐸 } ) = ∅ )
25 disjtpsn ⊢ ( ( 𝐴 ≠ 𝐹 ∧ 𝐵 ≠ 𝐹 ∧ 𝐶 ≠ 𝐹 ) → ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐹 } ) = ∅ )
26 25 3ad2ant3 ⊢ ( ( ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸 ) ∧ ( 𝐴 ≠ 𝐹 ∧ 𝐵 ≠ 𝐹 ∧ 𝐶 ≠ 𝐹 ) ) → ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐹 } ) = ∅ )
27 24 26 jca ⊢ ( ( ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸 ) ∧ ( 𝐴 ≠ 𝐹 ∧ 𝐵 ≠ 𝐹 ∧ 𝐶 ≠ 𝐹 ) ) → ( ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐷 , 𝐸 } ) = ∅ ∧ ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐹 } ) = ∅ ) )
28 undisj2 ⊢ ( ( ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐷 , 𝐸 } ) = ∅ ∧ ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐹 } ) = ∅ ) ↔ ( { 𝐴 , 𝐵 , 𝐶 } ∩ ( { 𝐷 , 𝐸 } ∪ { 𝐹 } ) ) = ∅ )
29 27 28 sylib ⊢ ( ( ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸 ) ∧ ( 𝐴 ≠ 𝐹 ∧ 𝐵 ≠ 𝐹 ∧ 𝐶 ≠ 𝐹 ) ) → ( { 𝐴 , 𝐵 , 𝐶 } ∩ ( { 𝐷 , 𝐸 } ∪ { 𝐹 } ) ) = ∅ )
30 2 29 eqtrid ⊢ ( ( ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸 ) ∧ ( 𝐴 ≠ 𝐹 ∧ 𝐵 ≠ 𝐹 ∧ 𝐶 ≠ 𝐹 ) ) → ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐷 , 𝐸 , 𝐹 } ) = ∅ )