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 V
fnprb.b B V
fntpb.c C 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 V
2 fnprb.b B V
3 fntpb.c C 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 V
24 fvex F B V
25 fvex F C 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 dom F x A B C
31 vex x V
32 31 eltp x 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 syl5bi A B A C B C F Fn A B C x 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 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 x 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 x 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 x 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