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