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	$$⊢\left(A\in U\wedge C\in V\wedge B\ne D\right)\to \mathrm{Fun}{\left\{⟨A,B⟩,⟨C,D⟩\right\}}^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		funcnvsn	$$⊢\mathrm{Fun}{\left\{⟨A,B⟩\right\}}^{-1}$$
2		funcnvsn	$$⊢\mathrm{Fun}{\left\{⟨C,D⟩\right\}}^{-1}$$
3	1 2	pm3.2i	$$⊢\left(\mathrm{Fun}{\left\{⟨A,B⟩\right\}}^{-1}\wedge \mathrm{Fun}{\left\{⟨C,D⟩\right\}}^{-1}\right)$$
4		df-rn	$$⊢\mathrm{ran}\left\{⟨A,B⟩\right\}=\mathrm{dom}{\left\{⟨A,B⟩\right\}}^{-1}$$
5		rnsnopg	$$⊢A\in U\to \mathrm{ran}\left\{⟨A,B⟩\right\}=\left\{B\right\}$$
6	4 5	eqtr3id	$$⊢A\in U\to \mathrm{dom}{\left\{⟨A,B⟩\right\}}^{-1}=\left\{B\right\}$$
7		df-rn	$$⊢\mathrm{ran}\left\{⟨C,D⟩\right\}=\mathrm{dom}{\left\{⟨C,D⟩\right\}}^{-1}$$
8		rnsnopg	$$⊢C\in V\to \mathrm{ran}\left\{⟨C,D⟩\right\}=\left\{D\right\}$$
9	7 8	eqtr3id	$$⊢C\in V\to \mathrm{dom}{\left\{⟨C,D⟩\right\}}^{-1}=\left\{D\right\}$$
10	6 9	ineqan12d	$$⊢\left(A\in U\wedge C\in V\right)\to \mathrm{dom}{\left\{⟨A,B⟩\right\}}^{-1}\cap \mathrm{dom}{\left\{⟨C,D⟩\right\}}^{-1}=\left\{B\right\}\cap \left\{D\right\}$$
11	10	3adant3	$$⊢\left(A\in U\wedge C\in V\wedge B\ne D\right)\to \mathrm{dom}{\left\{⟨A,B⟩\right\}}^{-1}\cap \mathrm{dom}{\left\{⟨C,D⟩\right\}}^{-1}=\left\{B\right\}\cap \left\{D\right\}$$
12		disjsn2	$$⊢B\ne D\to \left\{B\right\}\cap \left\{D\right\}=\varnothing$$
13	12	3ad2ant3	$$⊢\left(A\in U\wedge C\in V\wedge B\ne D\right)\to \left\{B\right\}\cap \left\{D\right\}=\varnothing$$
14	11 13	eqtrd	$$⊢\left(A\in U\wedge C\in V\wedge B\ne D\right)\to \mathrm{dom}{\left\{⟨A,B⟩\right\}}^{-1}\cap \mathrm{dom}{\left\{⟨C,D⟩\right\}}^{-1}=\varnothing$$
15		funun	$$⊢\left(\left(\mathrm{Fun}{\left\{⟨A,B⟩\right\}}^{-1}\wedge \mathrm{Fun}{\left\{⟨C,D⟩\right\}}^{-1}\right)\wedge \mathrm{dom}{\left\{⟨A,B⟩\right\}}^{-1}\cap \mathrm{dom}{\left\{⟨C,D⟩\right\}}^{-1}=\varnothing \right)\to \mathrm{Fun}\left({\left\{⟨A,B⟩\right\}}^{-1}\cup {\left\{⟨C,D⟩\right\}}^{-1}\right)$$
16	3 14 15	sylancr	$$⊢\left(A\in U\wedge C\in V\wedge B\ne D\right)\to \mathrm{Fun}\left({\left\{⟨A,B⟩\right\}}^{-1}\cup {\left\{⟨C,D⟩\right\}}^{-1}\right)$$
17		df-pr	$$⊢\left\{⟨A,B⟩,⟨C,D⟩\right\}=\left\{⟨A,B⟩\right\}\cup \left\{⟨C,D⟩\right\}$$
18	17	cnveqi	$$⊢{\left\{⟨A,B⟩,⟨C,D⟩\right\}}^{-1}={\left(\left\{⟨A,B⟩\right\}\cup \left\{⟨C,D⟩\right\}\right)}^{-1}$$
19		cnvun	$$⊢{\left(\left\{⟨A,B⟩\right\}\cup \left\{⟨C,D⟩\right\}\right)}^{-1}={\left\{⟨A,B⟩\right\}}^{-1}\cup {\left\{⟨C,D⟩\right\}}^{-1}$$
20	18 19	eqtri	$$⊢{\left\{⟨A,B⟩,⟨C,D⟩\right\}}^{-1}={\left\{⟨A,B⟩\right\}}^{-1}\cup {\left\{⟨C,D⟩\right\}}^{-1}$$
21	20	funeqi	$$⊢\mathrm{Fun}{\left\{⟨A,B⟩,⟨C,D⟩\right\}}^{-1}\leftrightarrow \mathrm{Fun}\left({\left\{⟨A,B⟩\right\}}^{-1}\cup {\left\{⟨C,D⟩\right\}}^{-1}\right)$$
22	16 21	sylibr	$$⊢\left(A\in U\wedge C\in V\wedge B\ne D\right)\to \mathrm{Fun}{\left\{⟨A,B⟩,⟨C,D⟩\right\}}^{-1}$$