Theorem disjtppr

Description: The disjoint intersection of an unordered triple and an unordered pair. (Contributed by Thierry Arnoux, 9-Nov-2026)

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

Proof

Step	Hyp	Ref	Expression
1		df-pr	⊢ { 𝐷 , 𝐸 } = ( { 𝐷 } ∪ { 𝐸 } )
2	1	ineq2i	⊢ ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐷 , 𝐸 } ) = ( { 𝐴 , 𝐵 , 𝐶 } ∩ ( { 𝐷 } ∪ { 𝐸 } ) )
3		disjtpsn	⊢ ( ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) → ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐷 } ) = ∅ )
4		disjtpsn	⊢ ( ( 𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸 ) → ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐸 } ) = ∅ )
5	3 4	anim12i	⊢ ( ( ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸 ) ) → ( ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐷 } ) = ∅ ∧ ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐸 } ) = ∅ ) )
6		undisj2	⊢ ( ( ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐷 } ) = ∅ ∧ ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐸 } ) = ∅ ) ↔ ( { 𝐴 , 𝐵 , 𝐶 } ∩ ( { 𝐷 } ∪ { 𝐸 } ) ) = ∅ )
7	5 6	sylib	⊢ ( ( ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸 ) ) → ( { 𝐴 , 𝐵 , 𝐶 } ∩ ( { 𝐷 } ∪ { 𝐸 } ) ) = ∅ )
8	2 7	eqtrid	⊢ ( ( ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸 ) ) → ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐷 , 𝐸 } ) = ∅ )