This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) >. } ) )