Theorem funtpg

Description: A set of three pairs is a function if their first members are different. (Contributed by Alexander van der Vekens, 5-Dec-2017) (Proof shortened by JJ, 14-Jul-2021)

	Ref	Expression
Assertion	funtpg	⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → Fun { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ , ⟨ 𝑍 , 𝐶 ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		3simpa	⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) )
2		3simpa	⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻 ) → ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ) )
3		simp1	⊢ ( ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) → 𝑋 ≠ 𝑌 )
4		funprg	⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ) ∧ 𝑋 ≠ 𝑌 ) → Fun { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } )
5	1 2 3 4	syl3an	⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → Fun { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } )
6		simp3	⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → 𝑍 ∈ 𝑊 )
7		simp3	⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻 ) → 𝐶 ∈ 𝐻 )
8		funsng	⊢ ( ( 𝑍 ∈ 𝑊 ∧ 𝐶 ∈ 𝐻 ) → Fun { ⟨ 𝑍 , 𝐶 ⟩ } )
9	6 7 8	syl2an	⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻 ) ) → Fun { ⟨ 𝑍 , 𝐶 ⟩ } )
10	9	3adant3	⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → Fun { ⟨ 𝑍 , 𝐶 ⟩ } )
11		dmpropg	⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ) → dom { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } = { 𝑋 , 𝑌 } )
12		dmsnopg	⊢ ( 𝐶 ∈ 𝐻 → dom { ⟨ 𝑍 , 𝐶 ⟩ } = { 𝑍 } )
13	11 12	ineqan12d	⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ) ∧ 𝐶 ∈ 𝐻 ) → ( dom { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } ∩ dom { ⟨ 𝑍 , 𝐶 ⟩ } ) = ( { 𝑋 , 𝑌 } ∩ { 𝑍 } ) )
14	13	3impa	⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻 ) → ( dom { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } ∩ dom { ⟨ 𝑍 , 𝐶 ⟩ } ) = ( { 𝑋 , 𝑌 } ∩ { 𝑍 } ) )
15		disjprsn	⊢ ( ( 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) → ( { 𝑋 , 𝑌 } ∩ { 𝑍 } ) = ∅ )
16	15	3adant1	⊢ ( ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) → ( { 𝑋 , 𝑌 } ∩ { 𝑍 } ) = ∅ )
17	14 16	sylan9eq	⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( dom { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } ∩ dom { ⟨ 𝑍 , 𝐶 ⟩ } ) = ∅ )
18	17	3adant1	⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( dom { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } ∩ dom { ⟨ 𝑍 , 𝐶 ⟩ } ) = ∅ )
19		funun	⊢ ( ( ( Fun { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } ∧ Fun { ⟨ 𝑍 , 𝐶 ⟩ } ) ∧ ( dom { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } ∩ dom { ⟨ 𝑍 , 𝐶 ⟩ } ) = ∅ ) → Fun ( { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } ∪ { ⟨ 𝑍 , 𝐶 ⟩ } ) )
20	5 10 18 19	syl21anc	⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → Fun ( { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } ∪ { ⟨ 𝑍 , 𝐶 ⟩ } ) )
21		df-tp	⊢ { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ , ⟨ 𝑍 , 𝐶 ⟩ } = ( { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } ∪ { ⟨ 𝑍 , 𝐶 ⟩ } )
22	21	funeqi	⊢ ( Fun { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ , ⟨ 𝑍 , 𝐶 ⟩ } ↔ Fun ( { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } ∪ { ⟨ 𝑍 , 𝐶 ⟩ } ) )
23	20 22	sylibr	⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → Fun { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ , ⟨ 𝑍 , 𝐶 ⟩ } )