Theorem fprb

Description: A condition for functionhood over a pair. (Contributed by Scott Fenton, 16-Sep-2013)

	Ref	Expression
Hypotheses	fprb.1	$$⊢A\in \mathrm{V}$$
	fprb.2	$$⊢B\in \mathrm{V}$$
Assertion	fprb	$$⊢A\ne B\to \left(F:\left\{A,B\right\}⟶R\leftrightarrow \exists x\in R\exists y\in RF=\left\{⟨A,x⟩,⟨B,y⟩\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		fprb.1	$$⊢A\in \mathrm{V}$$
2		fprb.2	$$⊢B\in \mathrm{V}$$
3	1	prid1	$$⊢A\in \left\{A,B\right\}$$
4		ffvelcdm	$$⊢\left(F:\left\{A,B\right\}⟶R\wedge A\in \left\{A,B\right\}\right)\to F\left(A\right)\in R$$
5	3 4	mpan2	$$⊢F:\left\{A,B\right\}⟶R\to F\left(A\right)\in R$$
6	5	adantr	$$⊢\left(F:\left\{A,B\right\}⟶R\wedge A\ne B\right)\to F\left(A\right)\in R$$
7	2	prid2	$$⊢B\in \left\{A,B\right\}$$
8		ffvelcdm	$$⊢\left(F:\left\{A,B\right\}⟶R\wedge B\in \left\{A,B\right\}\right)\to F\left(B\right)\in R$$
9	7 8	mpan2	$$⊢F:\left\{A,B\right\}⟶R\to F\left(B\right)\in R$$
10	9	adantr	$$⊢\left(F:\left\{A,B\right\}⟶R\wedge A\ne B\right)\to F\left(B\right)\in R$$
11		fvex	$$⊢F\left(A\right)\in \mathrm{V}$$
12	1 11	fvpr1	$$⊢A\ne B\to \left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(A\right)=F\left(A\right)$$
13		fvex	$$⊢F\left(B\right)\in \mathrm{V}$$
14	2 13	fvpr2	$$⊢A\ne B\to \left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(B\right)=F\left(B\right)$$
15		fveq2	$$⊢x=A\to F\left(x\right)=F\left(A\right)$$
16		fveq2	$$⊢x=A\to \left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(x\right)=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(A\right)$$
17	15 16	eqeq12d	$$⊢x=A\to \left(F\left(x\right)=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(x\right)\leftrightarrow F\left(A\right)=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(A\right)\right)$$
18		eqcom	$$⊢F\left(A\right)=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(A\right)\leftrightarrow \left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(A\right)=F\left(A\right)$$
19	17 18	bitrdi	$$⊢x=A\to \left(F\left(x\right)=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(x\right)\leftrightarrow \left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(A\right)=F\left(A\right)\right)$$
20		fveq2	$$⊢x=B\to F\left(x\right)=F\left(B\right)$$
21		fveq2	$$⊢x=B\to \left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(x\right)=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(B\right)$$
22	20 21	eqeq12d	$$⊢x=B\to \left(F\left(x\right)=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(x\right)\leftrightarrow F\left(B\right)=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(B\right)\right)$$
23		eqcom	$$⊢F\left(B\right)=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(B\right)\leftrightarrow \left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(B\right)=F\left(B\right)$$
24	22 23	bitrdi	$$⊢x=B\to \left(F\left(x\right)=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(x\right)\leftrightarrow \left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(B\right)=F\left(B\right)\right)$$
25	1 2 19 24	ralpr	$$⊢\forall x\in \left\{A,B\right\}F\left(x\right)=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(x\right)\leftrightarrow \left(\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(A\right)=F\left(A\right)\wedge \left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(B\right)=F\left(B\right)\right)$$
26	12 14 25	sylanbrc	$$⊢A\ne B\to \forall x\in \left\{A,B\right\}F\left(x\right)=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(x\right)$$
27	26	adantl	$$⊢\left(F:\left\{A,B\right\}⟶R\wedge A\ne B\right)\to \forall x\in \left\{A,B\right\}F\left(x\right)=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(x\right)$$
28		ffn	$$⊢F:\left\{A,B\right\}⟶R\to FFn\left\{A,B\right\}$$
29	1 2 11 13	fpr	$$⊢A\ne B\to \left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}:\left\{A,B\right\}⟶\left\{F\left(A\right),F\left(B\right)\right\}$$
30	29	ffnd	$$⊢A\ne B\to \left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}Fn\left\{A,B\right\}$$
31		eqfnfv	$$⊢\left(FFn\left\{A,B\right\}\wedge \left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}Fn\left\{A,B\right\}\right)\to \left(F=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\leftrightarrow \forall x\in \left\{A,B\right\}F\left(x\right)=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(x\right)\right)$$
32	28 30 31	syl2an	$$⊢\left(F:\left\{A,B\right\}⟶R\wedge A\ne B\right)\to \left(F=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\leftrightarrow \forall x\in \left\{A,B\right\}F\left(x\right)=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(x\right)\right)$$
33	27 32	mpbird	$$⊢\left(F:\left\{A,B\right\}⟶R\wedge A\ne B\right)\to F=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}$$
34		opeq2	$$⊢x=F\left(A\right)\to ⟨A,x⟩=⟨A,F\left(A\right)⟩$$
35	34	preq1d	$$⊢x=F\left(A\right)\to \left\{⟨A,x⟩,⟨B,y⟩\right\}=\left\{⟨A,F\left(A\right)⟩,⟨B,y⟩\right\}$$
36	35	eqeq2d	$$⊢x=F\left(A\right)\to \left(F=\left\{⟨A,x⟩,⟨B,y⟩\right\}\leftrightarrow F=\left\{⟨A,F\left(A\right)⟩,⟨B,y⟩\right\}\right)$$
37		opeq2	$$⊢y=F\left(B\right)\to ⟨B,y⟩=⟨B,F\left(B\right)⟩$$
38	37	preq2d	$$⊢y=F\left(B\right)\to \left\{⟨A,F\left(A\right)⟩,⟨B,y⟩\right\}=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}$$
39	38	eqeq2d	$$⊢y=F\left(B\right)\to \left(F=\left\{⟨A,F\left(A\right)⟩,⟨B,y⟩\right\}\leftrightarrow F=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\right)$$
40	36 39	rspc2ev	$$⊢\left(F\left(A\right)\in R\wedge F\left(B\right)\in R\wedge F=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\right)\to \exists x\in R\exists y\in RF=\left\{⟨A,x⟩,⟨B,y⟩\right\}$$
41	6 10 33 40	syl3anc	$$⊢\left(F:\left\{A,B\right\}⟶R\wedge A\ne B\right)\to \exists x\in R\exists y\in RF=\left\{⟨A,x⟩,⟨B,y⟩\right\}$$
42	41	expcom	$$⊢A\ne B\to \left(F:\left\{A,B\right\}⟶R\to \exists x\in R\exists y\in RF=\left\{⟨A,x⟩,⟨B,y⟩\right\}\right)$$
43		vex	$$⊢x\in \mathrm{V}$$
44		vex	$$⊢y\in \mathrm{V}$$
45	1 2 43 44	fpr	$$⊢A\ne B\to \left\{⟨A,x⟩,⟨B,y⟩\right\}:\left\{A,B\right\}⟶\left\{x,y\right\}$$
46		prssi	$$⊢\left(x\in R\wedge y\in R\right)\to \left\{x,y\right\}\subseteq R$$
47		fss	$$⊢\left(\left\{⟨A,x⟩,⟨B,y⟩\right\}:\left\{A,B\right\}⟶\left\{x,y\right\}\wedge \left\{x,y\right\}\subseteq R\right)\to \left\{⟨A,x⟩,⟨B,y⟩\right\}:\left\{A,B\right\}⟶R$$
48	45 46 47	syl2an	$$⊢\left(A\ne B\wedge \left(x\in R\wedge y\in R\right)\right)\to \left\{⟨A,x⟩,⟨B,y⟩\right\}:\left\{A,B\right\}⟶R$$
49	48	ex	$$⊢A\ne B\to \left(\left(x\in R\wedge y\in R\right)\to \left\{⟨A,x⟩,⟨B,y⟩\right\}:\left\{A,B\right\}⟶R\right)$$
50		feq1	$$⊢F=\left\{⟨A,x⟩,⟨B,y⟩\right\}\to \left(F:\left\{A,B\right\}⟶R\leftrightarrow \left\{⟨A,x⟩,⟨B,y⟩\right\}:\left\{A,B\right\}⟶R\right)$$
51	50	biimprcd	$$⊢\left\{⟨A,x⟩,⟨B,y⟩\right\}:\left\{A,B\right\}⟶R\to \left(F=\left\{⟨A,x⟩,⟨B,y⟩\right\}\to F:\left\{A,B\right\}⟶R\right)$$
52	49 51	syl6	$$⊢A\ne B\to \left(\left(x\in R\wedge y\in R\right)\to \left(F=\left\{⟨A,x⟩,⟨B,y⟩\right\}\to F:\left\{A,B\right\}⟶R\right)\right)$$
53	52	rexlimdvv	$$⊢A\ne B\to \left(\exists x\in R\exists y\in RF=\left\{⟨A,x⟩,⟨B,y⟩\right\}\to F:\left\{A,B\right\}⟶R\right)$$
54	42 53	impbid	$$⊢A\ne B\to \left(F:\left\{A,B\right\}⟶R\leftrightarrow \exists x\in R\exists y\in RF=\left\{⟨A,x⟩,⟨B,y⟩\right\}\right)$$