Theorem funprg

Description: A set of two pairs is a function if their first members are different. (Contributed by FL, 26-Jun-2011) (Proof shortened by JJ, 14-Jul-2021)

	Ref	Expression
Assertion	funprg	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ∧ 𝐴 ≠ 𝐵 ) → Fun { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		funsng	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋 ) → Fun { ⟨ 𝐴 , 𝐶 ⟩ } )
2		funsng	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐷 ∈ 𝑌 ) → Fun { ⟨ 𝐵 , 𝐷 ⟩ } )
3	1 2	anim12i	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑊 ∧ 𝐷 ∈ 𝑌 ) ) → ( Fun { ⟨ 𝐴 , 𝐶 ⟩ } ∧ Fun { ⟨ 𝐵 , 𝐷 ⟩ } ) )
4	3	an4s	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) → ( Fun { ⟨ 𝐴 , 𝐶 ⟩ } ∧ Fun { ⟨ 𝐵 , 𝐷 ⟩ } ) )
5	4	3adant3	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ∧ 𝐴 ≠ 𝐵 ) → ( Fun { ⟨ 𝐴 , 𝐶 ⟩ } ∧ Fun { ⟨ 𝐵 , 𝐷 ⟩ } ) )
6		dmsnopg	⊢ ( 𝐶 ∈ 𝑋 → dom { ⟨ 𝐴 , 𝐶 ⟩ } = { 𝐴 } )
7		dmsnopg	⊢ ( 𝐷 ∈ 𝑌 → dom { ⟨ 𝐵 , 𝐷 ⟩ } = { 𝐵 } )
8	6 7	ineqan12d	⊢ ( ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) → ( dom { ⟨ 𝐴 , 𝐶 ⟩ } ∩ dom { ⟨ 𝐵 , 𝐷 ⟩ } ) = ( { 𝐴 } ∩ { 𝐵 } ) )
9		disjsn2	⊢ ( 𝐴 ≠ 𝐵 → ( { 𝐴 } ∩ { 𝐵 } ) = ∅ )
10	8 9	sylan9eq	⊢ ( ( ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ∧ 𝐴 ≠ 𝐵 ) → ( dom { ⟨ 𝐴 , 𝐶 ⟩ } ∩ dom { ⟨ 𝐵 , 𝐷 ⟩ } ) = ∅ )
11	10	3adant1	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ∧ 𝐴 ≠ 𝐵 ) → ( dom { ⟨ 𝐴 , 𝐶 ⟩ } ∩ dom { ⟨ 𝐵 , 𝐷 ⟩ } ) = ∅ )
12		funun	⊢ ( ( ( Fun { ⟨ 𝐴 , 𝐶 ⟩ } ∧ Fun { ⟨ 𝐵 , 𝐷 ⟩ } ) ∧ ( dom { ⟨ 𝐴 , 𝐶 ⟩ } ∩ dom { ⟨ 𝐵 , 𝐷 ⟩ } ) = ∅ ) → Fun ( { ⟨ 𝐴 , 𝐶 ⟩ } ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) )
13	5 11 12	syl2anc	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ∧ 𝐴 ≠ 𝐵 ) → Fun ( { ⟨ 𝐴 , 𝐶 ⟩ } ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) )
14		df-pr	⊢ { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = ( { ⟨ 𝐴 , 𝐶 ⟩ } ∪ { ⟨ 𝐵 , 𝐷 ⟩ } )
15	14	funeqi	⊢ ( Fun { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ↔ Fun ( { ⟨ 𝐴 , 𝐶 ⟩ } ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) )
16	13 15	sylibr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ∧ 𝐴 ≠ 𝐵 ) → Fun { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } )