Metamath Proof Explorer

Theorem fntpb

Description: A function whose domain has at most three elements can be represented as a set of at most three ordered pairs. (Contributed by AV, 26-Jan-2021)

Ref Expression
Hypotheses fnprb.a 
|- A e. _V
fnprb.b 
|- B e. _V
fntpb.c 
|- C e. _V
Assertion fntpb 
|- ( F Fn { A , B , C } <-> F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } )

Proof

Step Hyp Ref Expression
1 fnprb.a 
 |-  A e. _V
2 fnprb.b 
 |-  B e. _V
3 fntpb.c 
 |-  C e. _V
4 1 2 fnprb 
 |-  ( F Fn { A , B } <-> F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } )
5 tpidm23 
 |-  { A , B , B } = { A , B }
6 5 eqcomi 
 |-  { A , B } = { A , B , B }
7 6 fneq2i 
 |-  ( F Fn { A , B } <-> F Fn { A , B , B } )
8 tpidm23 
 |-  { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. B , ( F ` B ) >. } = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. }
9 8 eqcomi 
 |-  { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. B , ( F ` B ) >. }
10 9 eqeq2i 
 |-  ( F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } <-> F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. B , ( F ` B ) >. } )
11 4 7 10 3bitr3i 
 |-  ( F Fn { A , B , B } <-> F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. B , ( F ` B ) >. } )
12 11 a1i 
 |-  ( B = C -> ( F Fn { A , B , B } <-> F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. B , ( F ` B ) >. } ) )
13 tpeq3 
 |-  ( B = C -> { A , B , B } = { A , B , C } )
14 13 fneq2d 
 |-  ( B = C -> ( F Fn { A , B , B } <-> F Fn { A , B , C } ) )
15 id 
 |-  ( B = C -> B = C )
16 fveq2 
 |-  ( B = C -> ( F ` B ) = ( F ` C ) )
17 15 16 opeq12d 
 |-  ( B = C -> <. B , ( F ` B ) >. = <. C , ( F ` C ) >. )
18 17 tpeq3d 
 |-  ( B = C -> { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. B , ( F ` B ) >. } = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } )
19 18 eqeq2d 
 |-  ( B = C -> ( F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. B , ( F ` B ) >. } <-> F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ) )
20 12 14 19 3bitr3d 
 |-  ( B = C -> ( F Fn { A , B , C } <-> F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ) )
21 20 a1d 
 |-  ( B = C -> ( ( A =/= B /\ A =/= C ) -> ( F Fn { A , B , C } <-> F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ) ) )
22 fndm 
 |-  ( F Fn { A , B , C } -> dom F = { A , B , C } )
23 fvex 
 |-  ( F ` A ) e. _V
24 fvex 
 |-  ( F ` B ) e. _V
25 fvex 
 |-  ( F ` C ) e. _V
26 23 24 25 dmtpop 
 |-  dom { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } = { A , B , C }
27 22 26 eqtr4di 
 |-  ( F Fn { A , B , C } -> dom F = dom { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } )
28 27 adantl 
 |-  ( ( ( ( A =/= B /\ A =/= C ) /\ B =/= C ) /\ F Fn { A , B , C } ) -> dom F = dom { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } )
29 22 adantl 
 |-  ( ( ( ( A =/= B /\ A =/= C ) /\ B =/= C ) /\ F Fn { A , B , C } ) -> dom F = { A , B , C } )
30 29 eleq2d 
 |-  ( ( ( ( A =/= B /\ A =/= C ) /\ B =/= C ) /\ F Fn { A , B , C } ) -> ( x e. dom F <-> x e. { A , B , C } ) )
31 vex 
 |-  x e. _V
32 31 eltp 
 |-  ( x e. { A , B , C } <-> ( x = A \/ x = B \/ x = C ) )
33 1 23 fvtp1 
 |-  ( ( A =/= B /\ A =/= C ) -> ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ` A ) = ( F ` A ) )
34 33 ad2antrr 
 |-  ( ( ( ( A =/= B /\ A =/= C ) /\ B =/= C ) /\ F Fn { A , B , C } ) -> ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ` A ) = ( F ` A ) )
35 34 eqcomd 
 |-  ( ( ( ( A =/= B /\ A =/= C ) /\ B =/= C ) /\ F Fn { A , B , C } ) -> ( F ` A ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ` A ) )
36 fveq2 
 |-  ( x = A -> ( F ` x ) = ( F ` A ) )
37 fveq2 
 |-  ( x = A -> ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ` x ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ` A ) )
38 36 37 eqeq12d 
 |-  ( x = A -> ( ( F ` x ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ` x ) <-> ( F ` A ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ` A ) ) )
39 35 38 syl5ibrcom 
 |-  ( ( ( ( A =/= B /\ A =/= C ) /\ B =/= C ) /\ F Fn { A , B , C } ) -> ( x = A -> ( F ` x ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ` x ) ) )
40 2 24 fvtp2 
 |-  ( ( A =/= B /\ B =/= C ) -> ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ` B ) = ( F ` B ) )
41 40 ad4ant13 
 |-  ( ( ( ( A =/= B /\ A =/= C ) /\ B =/= C ) /\ F Fn { A , B , C } ) -> ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ` B ) = ( F ` B ) )
42 41 eqcomd 
 |-  ( ( ( ( A =/= B /\ A =/= C ) /\ B =/= C ) /\ F Fn { A , B , C } ) -> ( F ` B ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ` B ) )
43 fveq2 
 |-  ( x = B -> ( F ` x ) = ( F ` B ) )
44 fveq2 
 |-  ( x = B -> ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ` x ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ` B ) )
45 43 44 eqeq12d 
 |-  ( x = B -> ( ( F ` x ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ` x ) <-> ( F ` B ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ` B ) ) )
46 42 45 syl5ibrcom 
 |-  ( ( ( ( A =/= B /\ A =/= C ) /\ B =/= C ) /\ F Fn { A , B , C } ) -> ( x = B -> ( F ` x ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ` x ) ) )
47 3 25 fvtp3 
 |-  ( ( A =/= C /\ B =/= C ) -> ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ` C ) = ( F ` C ) )
48 47 ad4ant23 
 |-  ( ( ( ( A =/= B /\ A =/= C ) /\ B =/= C ) /\ F Fn { A , B , C } ) -> ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ` C ) = ( F ` C ) )
49 48 eqcomd 
 |-  ( ( ( ( A =/= B /\ A =/= C ) /\ B =/= C ) /\ F Fn { A , B , C } ) -> ( F ` C ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ` C ) )
50 fveq2 
 |-  ( x = C -> ( F ` x ) = ( F ` C ) )
51 fveq2 
 |-  ( x = C -> ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ` x ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ` C ) )
52 50 51 eqeq12d 
 |-  ( x = C -> ( ( F ` x ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ` x ) <-> ( F ` C ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ` C ) ) )
53 49 52 syl5ibrcom 
 |-  ( ( ( ( A =/= B /\ A =/= C ) /\ B =/= C ) /\ F Fn { A , B , C } ) -> ( x = C -> ( F ` x ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ` x ) ) )
54 39 46 53 3jaod 
 |-  ( ( ( ( A =/= B /\ A =/= C ) /\ B =/= C ) /\ F Fn { A , B , C } ) -> ( ( x = A \/ x = B \/ x = C ) -> ( F ` x ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ` x ) ) )
55 32 54 biimtrid 
 |-  ( ( ( ( A =/= B /\ A =/= C ) /\ B =/= C ) /\ F Fn { A , B , C } ) -> ( x e. { A , B , C } -> ( F ` x ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ` x ) ) )
56 30 55 sylbid 
 |-  ( ( ( ( A =/= B /\ A =/= C ) /\ B =/= C ) /\ F Fn { A , B , C } ) -> ( x e. dom F -> ( F ` x ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ` x ) ) )
57 56 ralrimiv 
 |-  ( ( ( ( A =/= B /\ A =/= C ) /\ B =/= C ) /\ F Fn { A , B , C } ) -> A. x e. dom F ( F ` x ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ` x ) )
58 fnfun 
 |-  ( F Fn { A , B , C } -> Fun F )
59 1 2 3 23 24 25 funtp 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> Fun { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } )
60 59 3expa 
 |-  ( ( ( A =/= B /\ A =/= C ) /\ B =/= C ) -> Fun { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } )
61 eqfunfv 
 |-  ( ( Fun F /\ Fun { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ) -> ( F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } <-> ( dom F = dom { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } /\ A. x e. dom F ( F ` x ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ` x ) ) ) )
62 58 60 61 syl2anr 
 |-  ( ( ( ( A =/= B /\ A =/= C ) /\ B =/= C ) /\ F Fn { A , B , C } ) -> ( F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } <-> ( dom F = dom { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } /\ A. x e. dom F ( F ` x ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ` x ) ) ) )
63 28 57 62 mpbir2and 
 |-  ( ( ( ( A =/= B /\ A =/= C ) /\ B =/= C ) /\ F Fn { A , B , C } ) -> F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } )
64 1 2 3 23 24 25 fntp 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } Fn { A , B , C } )
65 64 3expa 
 |-  ( ( ( A =/= B /\ A =/= C ) /\ B =/= C ) -> { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } Fn { A , B , C } )
66 fneq1 
 |-  ( F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } -> ( F Fn { A , B , C } <-> { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } Fn { A , B , C } ) )
67 66 biimprd 
 |-  ( F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } -> ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } Fn { A , B , C } -> F Fn { A , B , C } ) )
68 65 67 mpan9 
 |-  ( ( ( ( A =/= B /\ A =/= C ) /\ B =/= C ) /\ F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ) -> F Fn { A , B , C } )
69 63 68 impbida 
 |-  ( ( ( A =/= B /\ A =/= C ) /\ B =/= C ) -> ( F Fn { A , B , C } <-> F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ) )
70 69 expcom 
 |-  ( B =/= C -> ( ( A =/= B /\ A =/= C ) -> ( F Fn { A , B , C } <-> F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ) ) )
71 21 70 pm2.61ine 
 |-  ( ( A =/= B /\ A =/= C ) -> ( F Fn { A , B , C } <-> F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ) )
72 1 3 fnprb 
 |-  ( F Fn { A , C } <-> F = { <. A , ( F ` A ) >. , <. C , ( F ` C ) >. } )
73 tpidm12 
 |-  { A , A , C } = { A , C }
74 73 eqcomi 
 |-  { A , C } = { A , A , C }
75 74 fneq2i 
 |-  ( F Fn { A , C } <-> F Fn { A , A , C } )
76 tpidm12 
 |-  { <. A , ( F ` A ) >. , <. A , ( F ` A ) >. , <. C , ( F ` C ) >. } = { <. A , ( F ` A ) >. , <. C , ( F ` C ) >. }
77 76 eqcomi 
 |-  { <. A , ( F ` A ) >. , <. C , ( F ` C ) >. } = { <. A , ( F ` A ) >. , <. A , ( F ` A ) >. , <. C , ( F ` C ) >. }
78 77 eqeq2i 
 |-  ( F = { <. A , ( F ` A ) >. , <. C , ( F ` C ) >. } <-> F = { <. A , ( F ` A ) >. , <. A , ( F ` A ) >. , <. C , ( F ` C ) >. } )
79 72 75 78 3bitr3i 
 |-  ( F Fn { A , A , C } <-> F = { <. A , ( F ` A ) >. , <. A , ( F ` A ) >. , <. C , ( F ` C ) >. } )
80 79 a1i 
 |-  ( A = B -> ( F Fn { A , A , C } <-> F = { <. A , ( F ` A ) >. , <. A , ( F ` A ) >. , <. C , ( F ` C ) >. } ) )
81 tpeq2 
 |-  ( A = B -> { A , A , C } = { A , B , C } )
82 81 fneq2d 
 |-  ( A = B -> ( F Fn { A , A , C } <-> F Fn { A , B , C } ) )
83 id 
 |-  ( A = B -> A = B )
84 fveq2 
 |-  ( A = B -> ( F ` A ) = ( F ` B ) )
85 83 84 opeq12d 
 |-  ( A = B -> <. A , ( F ` A ) >. = <. B , ( F ` B ) >. )
86 85 tpeq2d 
 |-  ( A = B -> { <. A , ( F ` A ) >. , <. A , ( F ` A ) >. , <. C , ( F ` C ) >. } = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } )
87 86 eqeq2d 
 |-  ( A = B -> ( F = { <. A , ( F ` A ) >. , <. A , ( F ` A ) >. , <. C , ( F ` C ) >. } <-> F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ) )
88 80 82 87 3bitr3d 
 |-  ( A = B -> ( F Fn { A , B , C } <-> F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ) )
89 tpidm13 
 |-  { A , B , A } = { A , B }
90 89 eqcomi 
 |-  { A , B } = { A , B , A }
91 90 fneq2i 
 |-  ( F Fn { A , B } <-> F Fn { A , B , A } )
92 tpidm13 
 |-  { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. A , ( F ` A ) >. } = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. }
93 92 eqcomi 
 |-  { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. A , ( F ` A ) >. }
94 93 eqeq2i 
 |-  ( F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } <-> F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. A , ( F ` A ) >. } )
95 4 91 94 3bitr3i 
 |-  ( F Fn { A , B , A } <-> F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. A , ( F ` A ) >. } )
96 95 a1i 
 |-  ( A = C -> ( F Fn { A , B , A } <-> F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. A , ( F ` A ) >. } ) )
97 tpeq3 
 |-  ( A = C -> { A , B , A } = { A , B , C } )
98 97 fneq2d 
 |-  ( A = C -> ( F Fn { A , B , A } <-> F Fn { A , B , C } ) )
99 id 
 |-  ( A = C -> A = C )
100 fveq2 
 |-  ( A = C -> ( F ` A ) = ( F ` C ) )
101 99 100 opeq12d 
 |-  ( A = C -> <. A , ( F ` A ) >. = <. C , ( F ` C ) >. )
102 101 tpeq3d 
 |-  ( A = C -> { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. A , ( F ` A ) >. } = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } )
103 102 eqeq2d 
 |-  ( A = C -> ( F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. A , ( F ` A ) >. } <-> F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ) )
104 96 98 103 3bitr3d 
 |-  ( A = C -> ( F Fn { A , B , C } <-> F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } ) )
105 71 88 104 pm2.61iine 
 |-  ( F Fn { A , B , C } <-> F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. , <. C , ( F ` C ) >. } )