Metamath Proof Explorer

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 e. _V
fnprb.b 
|- B e. _V
Assertion fnprb 
|- ( F Fn { A , B } <-> F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } )

Proof

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