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

Metamath Proof Explorer

Theorem funcnvpr

Description: The converse pair of ordered pairs is a function if the second members are different. Note that the second members need not be sets. (Contributed by AV, 23-Jan-2021)

Ref Expression
Assertion funcnvpr ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷 ) → Fun ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } )

Proof

Step Hyp Ref Expression
1 funcnvsn ⊢ Fun ◡ { ⟨ 𝐴 , 𝐵 ⟩ }
2 funcnvsn ⊢ Fun ◡ { ⟨ 𝐶 , 𝐷 ⟩ }
3 1 2 pm3.2i ⊢ ( Fun ◡ { ⟨ 𝐴 , 𝐵 ⟩ } ∧ Fun ◡ { ⟨ 𝐶 , 𝐷 ⟩ } )
4 df-rn ⊢ ran { ⟨ 𝐴 , 𝐵 ⟩ } = dom ◡ { ⟨ 𝐴 , 𝐵 ⟩ }
5 rnsnopg ⊢ ( 𝐴 ∈ 𝑈 → ran { ⟨ 𝐴 , 𝐵 ⟩ } = { 𝐵 } )
6 4 5 eqtr3id ⊢ ( 𝐴 ∈ 𝑈 → dom ◡ { ⟨ 𝐴 , 𝐵 ⟩ } = { 𝐵 } )
7 df-rn ⊢ ran { ⟨ 𝐶 , 𝐷 ⟩ } = dom ◡ { ⟨ 𝐶 , 𝐷 ⟩ }
8 rnsnopg ⊢ ( 𝐶 ∈ 𝑉 → ran { ⟨ 𝐶 , 𝐷 ⟩ } = { 𝐷 } )
9 7 8 eqtr3id ⊢ ( 𝐶 ∈ 𝑉 → dom ◡ { ⟨ 𝐶 , 𝐷 ⟩ } = { 𝐷 } )
10 6 9 ineqan12d ⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ) → ( dom ◡ { ⟨ 𝐴 , 𝐵 ⟩ } ∩ dom ◡ { ⟨ 𝐶 , 𝐷 ⟩ } ) = ( { 𝐵 } ∩ { 𝐷 } ) )
11 10 3adant3 ⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷 ) → ( dom ◡ { ⟨ 𝐴 , 𝐵 ⟩ } ∩ dom ◡ { ⟨ 𝐶 , 𝐷 ⟩ } ) = ( { 𝐵 } ∩ { 𝐷 } ) )
12 disjsn2 ⊢ ( 𝐵 ≠ 𝐷 → ( { 𝐵 } ∩ { 𝐷 } ) = ∅ )
13 12 3ad2ant3 ⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷 ) → ( { 𝐵 } ∩ { 𝐷 } ) = ∅ )
14 11 13 eqtrd ⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷 ) → ( dom ◡ { ⟨ 𝐴 , 𝐵 ⟩ } ∩ dom ◡ { ⟨ 𝐶 , 𝐷 ⟩ } ) = ∅ )
15 funun ⊢ ( ( ( Fun ◡ { ⟨ 𝐴 , 𝐵 ⟩ } ∧ Fun ◡ { ⟨ 𝐶 , 𝐷 ⟩ } ) ∧ ( dom ◡ { ⟨ 𝐴 , 𝐵 ⟩ } ∩ dom ◡ { ⟨ 𝐶 , 𝐷 ⟩ } ) = ∅ ) → Fun ( ◡ { ⟨ 𝐴 , 𝐵 ⟩ } ∪ ◡ { ⟨ 𝐶 , 𝐷 ⟩ } ) )
16 3 14 15 sylancr ⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷 ) → Fun ( ◡ { ⟨ 𝐴 , 𝐵 ⟩ } ∪ ◡ { ⟨ 𝐶 , 𝐷 ⟩ } ) )
17 df-pr ⊢ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } )
18 17 cnveqi ⊢ ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = ◡ ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } )
19 cnvun ⊢ ◡ ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } ) = ( ◡ { ⟨ 𝐴 , 𝐵 ⟩ } ∪ ◡ { ⟨ 𝐶 , 𝐷 ⟩ } )
20 18 19 eqtri ⊢ ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = ( ◡ { ⟨ 𝐴 , 𝐵 ⟩ } ∪ ◡ { ⟨ 𝐶 , 𝐷 ⟩ } )
21 20 funeqi ⊢ ( Fun ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ↔ Fun ( ◡ { ⟨ 𝐴 , 𝐵 ⟩ } ∪ ◡ { ⟨ 𝐶 , 𝐷 ⟩ } ) )
22 16 21 sylibr ⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷 ) → Fun ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } )