Theorem fnprb

Description: A function whose domain has at most two elements can be represented as a set of at most two ordered pairs. (Contributed by FL, 26-Jun-2011) (Proof shortened by Scott Fenton, 12-Oct-2017) Eliminate unnecessary antecedent A =/= B . (Revised by NM, 29-Dec-2018)

	Ref	Expression
Hypotheses	fnprb.a	$$⊢A\in \mathrm{V}$$
	fnprb.b	$$⊢B\in \mathrm{V}$$
Assertion	fnprb	$$⊢FFn\left\{A,B\right\}\leftrightarrow F=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		fnprb.a	$$⊢A\in \mathrm{V}$$
2		fnprb.b	$$⊢B\in \mathrm{V}$$
3	1	fnsnb	$$⊢FFn\left\{A\right\}\leftrightarrow F=\left\{⟨A,F\left(A\right)⟩\right\}$$
4		dfsn2	$$⊢\left\{A\right\}=\left\{A,A\right\}$$
5	4	fneq2i	$$⊢FFn\left\{A\right\}\leftrightarrow FFn\left\{A,A\right\}$$
6		dfsn2	$$⊢\left\{⟨A,F\left(A\right)⟩\right\}=\left\{⟨A,F\left(A\right)⟩,⟨A,F\left(A\right)⟩\right\}$$
7	6	eqeq2i	$$⊢F=\left\{⟨A,F\left(A\right)⟩\right\}\leftrightarrow F=\left\{⟨A,F\left(A\right)⟩,⟨A,F\left(A\right)⟩\right\}$$
8	3 5 7	3bitr3i	$$⊢FFn\left\{A,A\right\}\leftrightarrow F=\left\{⟨A,F\left(A\right)⟩,⟨A,F\left(A\right)⟩\right\}$$
9	8	a1i	$$⊢A=B\to \left(FFn\left\{A,A\right\}\leftrightarrow F=\left\{⟨A,F\left(A\right)⟩,⟨A,F\left(A\right)⟩\right\}\right)$$
10		preq2	$$⊢A=B\to \left\{A,A\right\}=\left\{A,B\right\}$$
11	10	fneq2d	$$⊢A=B\to \left(FFn\left\{A,A\right\}\leftrightarrow FFn\left\{A,B\right\}\right)$$
12		id	$$⊢A=B\to A=B$$
13		fveq2	$$⊢A=B\to F\left(A\right)=F\left(B\right)$$
14	12 13	opeq12d	$$⊢A=B\to ⟨A,F\left(A\right)⟩=⟨B,F\left(B\right)⟩$$
15	14	preq2d	$$⊢A=B\to \left\{⟨A,F\left(A\right)⟩,⟨A,F\left(A\right)⟩\right\}=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}$$
16	15	eqeq2d	$$⊢A=B\to \left(F=\left\{⟨A,F\left(A\right)⟩,⟨A,F\left(A\right)⟩\right\}\leftrightarrow F=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\right)$$
17	9 11 16	3bitr3d	$$⊢A=B\to \left(FFn\left\{A,B\right\}\leftrightarrow F=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\right)$$
18		fndm	$$⊢FFn\left\{A,B\right\}\to \mathrm{dom}F=\left\{A,B\right\}$$
19		fvex	$$⊢F\left(A\right)\in \mathrm{V}$$
20		fvex	$$⊢F\left(B\right)\in \mathrm{V}$$
21	19 20	dmprop	$$⊢\mathrm{dom}\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}=\left\{A,B\right\}$$
22	18 21	eqtr4di	$$⊢FFn\left\{A,B\right\}\to \mathrm{dom}F=\mathrm{dom}\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}$$
23	22	adantl	$$⊢\left(A\ne B\wedge FFn\left\{A,B\right\}\right)\to \mathrm{dom}F=\mathrm{dom}\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}$$
24	18	adantl	$$⊢\left(A\ne B\wedge FFn\left\{A,B\right\}\right)\to \mathrm{dom}F=\left\{A,B\right\}$$
25	24	eleq2d	$$⊢\left(A\ne B\wedge FFn\left\{A,B\right\}\right)\to \left(x\in \mathrm{dom}F\leftrightarrow x\in \left\{A,B\right\}\right)$$
26		vex	$$⊢x\in \mathrm{V}$$
27	26	elpr	$$⊢x\in \left\{A,B\right\}\leftrightarrow \left(x=A\vee x=B\right)$$
28	1 19	fvpr1	$$⊢A\ne B\to \left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(A\right)=F\left(A\right)$$
29	28	adantr	$$⊢\left(A\ne B\wedge FFn\left\{A,B\right\}\right)\to \left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(A\right)=F\left(A\right)$$
30	29	eqcomd	$$⊢\left(A\ne B\wedge FFn\left\{A,B\right\}\right)\to F\left(A\right)=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(A\right)$$
31		fveq2	$$⊢x=A\to F\left(x\right)=F\left(A\right)$$
32		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)$$
33	31 32	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)$$
34	30 33	syl5ibrcom	$$⊢\left(A\ne B\wedge FFn\left\{A,B\right\}\right)\to \left(x=A\to F\left(x\right)=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(x\right)\right)$$
35	2 20	fvpr2	$$⊢A\ne B\to \left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(B\right)=F\left(B\right)$$
36	35	adantr	$$⊢\left(A\ne B\wedge FFn\left\{A,B\right\}\right)\to \left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(B\right)=F\left(B\right)$$
37	36	eqcomd	$$⊢\left(A\ne B\wedge FFn\left\{A,B\right\}\right)\to F\left(B\right)=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(B\right)$$
38		fveq2	$$⊢x=B\to F\left(x\right)=F\left(B\right)$$
39		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)$$
40	38 39	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)$$
41	37 40	syl5ibrcom	$$⊢\left(A\ne B\wedge FFn\left\{A,B\right\}\right)\to \left(x=B\to F\left(x\right)=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(x\right)\right)$$
42	34 41	jaod	$$⊢\left(A\ne B\wedge FFn\left\{A,B\right\}\right)\to \left(\left(x=A\vee x=B\right)\to F\left(x\right)=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(x\right)\right)$$
43	27 42	syl5bi	$$⊢\left(A\ne B\wedge FFn\left\{A,B\right\}\right)\to \left(x\in \left\{A,B\right\}\to F\left(x\right)=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(x\right)\right)$$
44	25 43	sylbid	$$⊢\left(A\ne B\wedge FFn\left\{A,B\right\}\right)\to \left(x\in \mathrm{dom}F\to F\left(x\right)=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(x\right)\right)$$
45	44	ralrimiv	$$⊢\left(A\ne B\wedge FFn\left\{A,B\right\}\right)\to \forall x\in \mathrm{dom}FF\left(x\right)=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(x\right)$$
46		fnfun	$$⊢FFn\left\{A,B\right\}\to \mathrm{Fun}F$$
47	1 2 19 20	funpr	$$⊢A\ne B\to \mathrm{Fun}\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}$$
48		eqfunfv	$$⊢\left(\mathrm{Fun}F\wedge \mathrm{Fun}\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\right)\to \left(F=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\leftrightarrow \left(\mathrm{dom}F=\mathrm{dom}\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\wedge \forall x\in \mathrm{dom}FF\left(x\right)=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(x\right)\right)\right)$$
49	46 47 48	syl2anr	$$⊢\left(A\ne B\wedge FFn\left\{A,B\right\}\right)\to \left(F=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\leftrightarrow \left(\mathrm{dom}F=\mathrm{dom}\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\wedge \forall x\in \mathrm{dom}FF\left(x\right)=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\left(x\right)\right)\right)$$
50	23 45 49	mpbir2and	$$⊢\left(A\ne B\wedge FFn\left\{A,B\right\}\right)\to F=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}$$
51		df-fn	$$⊢\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}Fn\left\{A,B\right\}\leftrightarrow \left(\mathrm{Fun}\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\wedge \mathrm{dom}\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}=\left\{A,B\right\}\right)$$
52	47 21 51	sylanblrc	$$⊢A\ne B\to \left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}Fn\left\{A,B\right\}$$
53		fneq1	$$⊢F=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\to \left(FFn\left\{A,B\right\}\leftrightarrow \left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}Fn\left\{A,B\right\}\right)$$
54	53	biimprd	$$⊢F=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\to \left(\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}Fn\left\{A,B\right\}\to FFn\left\{A,B\right\}\right)$$
55	52 54	mpan9	$$⊢\left(A\ne B\wedge F=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\right)\to FFn\left\{A,B\right\}$$
56	50 55	impbida	$$⊢A\ne B\to \left(FFn\left\{A,B\right\}\leftrightarrow F=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\right)$$
57	17 56	pm2.61ine	$$⊢FFn\left\{A,B\right\}\leftrightarrow F=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}$$