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

Metamath Proof Explorer

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 { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } )