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	|- ( ( A e. V /\ B e. W ) -> ( F Fn { A , B } <-> F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ) )

Proof

Step	Hyp	Ref	Expression
1		preq1	|- ( a = A -> { a , b } = { A , b } )
2	1	fneq2d	|- ( a = A -> ( F Fn { a , b } <-> F Fn { A , b } ) )
3		id	|- ( a = A -> a = A )
4		fveq2	|- ( a = A -> ( F ` a ) = ( F ` A ) )
5	3 4	opeq12d	|- ( a = A -> <. a , ( F ` a ) >. = <. A , ( F ` A ) >. )
6	5	preq1d	|- ( a = A -> { <. a , ( F ` a ) >. , <. b , ( F ` b ) >. } = { <. A , ( F ` A ) >. , <. b , ( F ` b ) >. } )
7	6	eqeq2d	|- ( a = A -> ( F = { <. a , ( F ` a ) >. , <. b , ( F ` b ) >. } <-> F = { <. A , ( F ` A ) >. , <. b , ( F ` b ) >. } ) )
8	2 7	bibi12d	|- ( a = A -> ( ( F Fn { a , b } <-> F = { <. a , ( F ` a ) >. , <. b , ( F ` b ) >. } ) <-> ( F Fn { A , b } <-> F = { <. A , ( F ` A ) >. , <. b , ( F ` b ) >. } ) ) )
9		preq2	|- ( b = B -> { A , b } = { A , B } )
10	9	fneq2d	|- ( b = B -> ( F Fn { A , b } <-> F Fn { A , B } ) )
11		id	|- ( b = B -> b = B )
12		fveq2	|- ( b = B -> ( F ` b ) = ( F ` B ) )
13	11 12	opeq12d	|- ( b = B -> <. b , ( F ` b ) >. = <. B , ( F ` B ) >. )
14	13	preq2d	|- ( b = B -> { <. A , ( F ` A ) >. , <. b , ( F ` b ) >. } = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } )
15	14	eqeq2d	|- ( b = B -> ( F = { <. A , ( F ` A ) >. , <. b , ( F ` b ) >. } <-> F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ) )
16	10 15	bibi12d	|- ( b = B -> ( ( F Fn { A , b } <-> F = { <. A , ( F ` A ) >. , <. b , ( F ` b ) >. } ) <-> ( F Fn { A , B } <-> F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ) ) )
17		vex	|- a e. _V
18		vex	|- b e. _V
19	17 18	fnprb	|- ( F Fn { a , b } <-> F = { <. a , ( F ` a ) >. , <. b , ( F ` b ) >. } )
20	8 16 19	vtocl2g	|- ( ( A e. V /\ B e. W ) -> ( F Fn { A , B } <-> F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ) )