Theorem fnpr2g

Description: A function whose domain has at most two elements can be represented as a set of at most two ordered pairs. (Contributed by Thierry Arnoux, 12-Jul-2020)

	Ref	Expression
Assertion	fnpr2g	$$⊢\left(A\in V\wedge B\in W\right)\to \left(FFn\left\{A,B\right\}\leftrightarrow F=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		preq1	$$⊢a=A\to \left\{a,b\right\}=\left\{A,b\right\}$$
2	1	fneq2d	$$⊢a=A\to \left(FFn\left\{a,b\right\}\leftrightarrow FFn\left\{A,b\right\}\right)$$
3		id	$$⊢a=A\to a=A$$
4		fveq2	$$⊢a=A\to F\left(a\right)=F\left(A\right)$$
5	3 4	opeq12d	$$⊢a=A\to ⟨a,F\left(a\right)⟩=⟨A,F\left(A\right)⟩$$
6	5	preq1d	$$⊢a=A\to \left\{⟨a,F\left(a\right)⟩,⟨b,F\left(b\right)⟩\right\}=\left\{⟨A,F\left(A\right)⟩,⟨b,F\left(b\right)⟩\right\}$$
7	6	eqeq2d	$$⊢a=A\to \left(F=\left\{⟨a,F\left(a\right)⟩,⟨b,F\left(b\right)⟩\right\}\leftrightarrow F=\left\{⟨A,F\left(A\right)⟩,⟨b,F\left(b\right)⟩\right\}\right)$$
8	2 7	bibi12d	$$⊢a=A\to \left(\left(FFn\left\{a,b\right\}\leftrightarrow F=\left\{⟨a,F\left(a\right)⟩,⟨b,F\left(b\right)⟩\right\}\right)\leftrightarrow \left(FFn\left\{A,b\right\}\leftrightarrow F=\left\{⟨A,F\left(A\right)⟩,⟨b,F\left(b\right)⟩\right\}\right)\right)$$
9		preq2	$$⊢b=B\to \left\{A,b\right\}=\left\{A,B\right\}$$
10	9	fneq2d	$$⊢b=B\to \left(FFn\left\{A,b\right\}\leftrightarrow FFn\left\{A,B\right\}\right)$$
11		id	$$⊢b=B\to b=B$$
12		fveq2	$$⊢b=B\to F\left(b\right)=F\left(B\right)$$
13	11 12	opeq12d	$$⊢b=B\to ⟨b,F\left(b\right)⟩=⟨B,F\left(B\right)⟩$$
14	13	preq2d	$$⊢b=B\to \left\{⟨A,F\left(A\right)⟩,⟨b,F\left(b\right)⟩\right\}=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}$$
15	14	eqeq2d	$$⊢b=B\to \left(F=\left\{⟨A,F\left(A\right)⟩,⟨b,F\left(b\right)⟩\right\}\leftrightarrow F=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\right)$$
16	10 15	bibi12d	$$⊢b=B\to \left(\left(FFn\left\{A,b\right\}\leftrightarrow F=\left\{⟨A,F\left(A\right)⟩,⟨b,F\left(b\right)⟩\right\}\right)\leftrightarrow \left(FFn\left\{A,B\right\}\leftrightarrow F=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\right)\right)$$
17		vex	$$⊢a\in \mathrm{V}$$
18		vex	$$⊢b\in \mathrm{V}$$
19	17 18	fnprb	$$⊢FFn\left\{a,b\right\}\leftrightarrow F=\left\{⟨a,F\left(a\right)⟩,⟨b,F\left(b\right)⟩\right\}$$
20	8 16 19	vtocl2g	$$⊢\left(A\in V\wedge B\in W\right)\to \left(FFn\left\{A,B\right\}\leftrightarrow F=\left\{⟨A,F\left(A\right)⟩,⟨B,F\left(B\right)⟩\right\}\right)$$