Theorem mptprop

Description: Rewrite pairs of ordered pairs as mapping to functions. (Contributed by Thierry Arnoux, 24-Sep-2023)

	Ref	Expression
Hypotheses	brprop.a	$$⊢\phi \to A\in V$$
	brprop.b	$$⊢\phi \to B\in W$$
	brprop.c	$$⊢\phi \to C\in V$$
	brprop.d	$$⊢\phi \to D\in W$$
	mptprop.1	$$⊢\phi \to A\ne C$$
Assertion	mptprop	$$⊢\phi \to \left\{⟨A,B⟩,⟨C,D⟩\right\}=\left(x\in \left\{A,C\right\}⟼if\left(x=A,B,D\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		brprop.a	$$⊢\phi \to A\in V$$
2		brprop.b	$$⊢\phi \to B\in W$$
3		brprop.c	$$⊢\phi \to C\in V$$
4		brprop.d	$$⊢\phi \to D\in W$$
5		mptprop.1	$$⊢\phi \to A\ne C$$
6		df-pr	$$⊢\left\{⟨A,B⟩,⟨C,D⟩\right\}=\left\{⟨A,B⟩\right\}\cup \left\{⟨C,D⟩\right\}$$
7		fmptsn	$$⊢\left(A\in V\wedge B\in W\right)\to \left\{⟨A,B⟩\right\}=\left(x\in \left\{A\right\}⟼B\right)$$
8	1 2 7	syl2anc	$$⊢\phi \to \left\{⟨A,B⟩\right\}=\left(x\in \left\{A\right\}⟼B\right)$$
9		incom	$$⊢\left\{A\right\}\cap \left\{A,C\right\}=\left\{A,C\right\}\cap \left\{A\right\}$$
10		prid1g	$$⊢A\in V\to A\in \left\{A,C\right\}$$
11		snssi	$$⊢A\in \left\{A,C\right\}\to \left\{A\right\}\subseteq \left\{A,C\right\}$$
12	1 10 11	3syl	$$⊢\phi \to \left\{A\right\}\subseteq \left\{A,C\right\}$$
13		df-ss	$$⊢\left\{A\right\}\subseteq \left\{A,C\right\}\leftrightarrow \left\{A\right\}\cap \left\{A,C\right\}=\left\{A\right\}$$
14	12 13	sylib	$$⊢\phi \to \left\{A\right\}\cap \left\{A,C\right\}=\left\{A\right\}$$
15	9 14	eqtr3id	$$⊢\phi \to \left\{A,C\right\}\cap \left\{A\right\}=\left\{A\right\}$$
16	15	mpteq1d	$$⊢\phi \to \left(x\in \left(\left\{A,C\right\}\cap \left\{A\right\}\right)⟼B\right)=\left(x\in \left\{A\right\}⟼B\right)$$
17	8 16	eqtr4d	$$⊢\phi \to \left\{⟨A,B⟩\right\}=\left(x\in \left(\left\{A,C\right\}\cap \left\{A\right\}\right)⟼B\right)$$
18		fmptsn	$$⊢\left(C\in V\wedge D\in W\right)\to \left\{⟨C,D⟩\right\}=\left(x\in \left\{C\right\}⟼D\right)$$
19	3 4 18	syl2anc	$$⊢\phi \to \left\{⟨C,D⟩\right\}=\left(x\in \left\{C\right\}⟼D\right)$$
20		difprsn1	$$⊢A\ne C\to \left\{A,C\right\}\setminus \left\{A\right\}=\left\{C\right\}$$
21	5 20	syl	$$⊢\phi \to \left\{A,C\right\}\setminus \left\{A\right\}=\left\{C\right\}$$
22	21	mpteq1d	$$⊢\phi \to \left(x\in \left(\left\{A,C\right\}\setminus \left\{A\right\}\right)⟼D\right)=\left(x\in \left\{C\right\}⟼D\right)$$
23	19 22	eqtr4d	$$⊢\phi \to \left\{⟨C,D⟩\right\}=\left(x\in \left(\left\{A,C\right\}\setminus \left\{A\right\}\right)⟼D\right)$$
24	17 23	uneq12d	$$⊢\phi \to \left\{⟨A,B⟩\right\}\cup \left\{⟨C,D⟩\right\}=\left(x\in \left(\left\{A,C\right\}\cap \left\{A\right\}\right)⟼B\right)\cup \left(x\in \left(\left\{A,C\right\}\setminus \left\{A\right\}\right)⟼D\right)$$
25		partfun	$$⊢\left(x\in \left\{A,C\right\}⟼if\left(x\in \left\{A\right\},B,D\right)\right)=\left(x\in \left(\left\{A,C\right\}\cap \left\{A\right\}\right)⟼B\right)\cup \left(x\in \left(\left\{A,C\right\}\setminus \left\{A\right\}\right)⟼D\right)$$
26	24 25	eqtr4di	$$⊢\phi \to \left\{⟨A,B⟩\right\}\cup \left\{⟨C,D⟩\right\}=\left(x\in \left\{A,C\right\}⟼if\left(x\in \left\{A\right\},B,D\right)\right)$$
27		elsn2g	$$⊢A\in V\to \left(x\in \left\{A\right\}\leftrightarrow x=A\right)$$
28	1 27	syl	$$⊢\phi \to \left(x\in \left\{A\right\}\leftrightarrow x=A\right)$$
29	28	ifbid	$$⊢\phi \to if\left(x\in \left\{A\right\},B,D\right)=if\left(x=A,B,D\right)$$
30	29	mpteq2dv	$$⊢\phi \to \left(x\in \left\{A,C\right\}⟼if\left(x\in \left\{A\right\},B,D\right)\right)=\left(x\in \left\{A,C\right\}⟼if\left(x=A,B,D\right)\right)$$
31	26 30	eqtrd	$$⊢\phi \to \left\{⟨A,B⟩\right\}\cup \left\{⟨C,D⟩\right\}=\left(x\in \left\{A,C\right\}⟼if\left(x=A,B,D\right)\right)$$
32	6 31	eqtrid	$$⊢\phi \to \left\{⟨A,B⟩,⟨C,D⟩\right\}=\left(x\in \left\{A,C\right\}⟼if\left(x=A,B,D\right)\right)$$