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 ⊢FFnABC↔F=AF⁡ABF⁡BCF⁡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 ⊢FFnAB↔F=AF⁡ABF⁡B
5 tpidm23 ⊢ABB=AB
6 5 eqcomi ⊢AB=ABB
7 6 fneq2i ⊢FFnAB↔FFnABB
8 tpidm23 ⊢AF⁡ABF⁡BBF⁡B=AF⁡ABF⁡B
9 8 eqcomi ⊢AF⁡ABF⁡B=AF⁡ABF⁡BBF⁡B
10 9 eqeq2i ⊢F=AF⁡ABF⁡B↔F=AF⁡ABF⁡BBF⁡B
11 4 7 10 3bitr3i ⊢FFnABB↔F=AF⁡ABF⁡BBF⁡B
12 11 a1i ⊢B=C→FFnABB↔F=AF⁡ABF⁡BBF⁡B
13 tpeq3 ⊢B=C→ABB=ABC
14 13 fneq2d ⊢B=C→FFnABB↔FFnABC
15 id ⊢B=C→B=C
16 fveq2 ⊢B=C→F⁡B=F⁡C
17 15 16 opeq12d ⊢B=C→BF⁡B=CF⁡C
18 17 tpeq3d ⊢B=C→AF⁡ABF⁡BBF⁡B=AF⁡ABF⁡BCF⁡C
19 18 eqeq2d ⊢B=C→F=AF⁡ABF⁡BBF⁡B↔F=AF⁡ABF⁡BCF⁡C
20 12 14 19 3bitr3d ⊢B=C→FFnABC↔F=AF⁡ABF⁡BCF⁡C
21 20 a1d ⊢B=C→A≠B∧A≠C→FFnABC↔F=AF⁡ABF⁡BCF⁡C
22 fndm ⊢FFnABC→dom⁡F=ABC
23 fvex ⊢F⁡A∈V
24 fvex ⊢F⁡B∈V
25 fvex ⊢F⁡C∈V
26 23 24 25 dmtpop ⊢dom⁡AF⁡ABF⁡BCF⁡C=ABC
27 22 26 eqtr4di ⊢FFnABC→dom⁡F=dom⁡AF⁡ABF⁡BCF⁡C
28 27 adantl ⊢A≠B∧A≠C∧B≠C∧FFnABC→dom⁡F=dom⁡AF⁡ABF⁡BCF⁡C
29 22 adantl ⊢A≠B∧A≠C∧B≠C∧FFnABC→dom⁡F=ABC
30 29 eleq2d ⊢A≠B∧A≠C∧B≠C∧FFnABC→x∈dom⁡F↔x∈ABC
31 vex ⊢x∈V
32 31 eltp ⊢x∈ABC↔x=A∨x=B∨x=C
33 1 23 fvtp1 ⊢A≠B∧A≠C→AF⁡ABF⁡BCF⁡C⁡A=F⁡A
34 33 ad2antrr ⊢A≠B∧A≠C∧B≠C∧FFnABC→AF⁡ABF⁡BCF⁡C⁡A=F⁡A
35 34 eqcomd ⊢A≠B∧A≠C∧B≠C∧FFnABC→F⁡A=AF⁡ABF⁡BCF⁡C⁡A
36 fveq2 ⊢x=A→F⁡x=F⁡A
37 fveq2 ⊢x=A→AF⁡ABF⁡BCF⁡C⁡x=AF⁡ABF⁡BCF⁡C⁡A
38 36 37 eqeq12d ⊢x=A→F⁡x=AF⁡ABF⁡BCF⁡C⁡x↔F⁡A=AF⁡ABF⁡BCF⁡C⁡A
39 35 38 syl5ibrcom ⊢A≠B∧A≠C∧B≠C∧FFnABC→x=A→F⁡x=AF⁡ABF⁡BCF⁡C⁡x
40 2 24 fvtp2 ⊢A≠B∧B≠C→AF⁡ABF⁡BCF⁡C⁡B=F⁡B
41 40 ad4ant13 ⊢A≠B∧A≠C∧B≠C∧FFnABC→AF⁡ABF⁡BCF⁡C⁡B=F⁡B
42 41 eqcomd ⊢A≠B∧A≠C∧B≠C∧FFnABC→F⁡B=AF⁡ABF⁡BCF⁡C⁡B
43 fveq2 ⊢x=B→F⁡x=F⁡B
44 fveq2 ⊢x=B→AF⁡ABF⁡BCF⁡C⁡x=AF⁡ABF⁡BCF⁡C⁡B
45 43 44 eqeq12d ⊢x=B→F⁡x=AF⁡ABF⁡BCF⁡C⁡x↔F⁡B=AF⁡ABF⁡BCF⁡C⁡B
46 42 45 syl5ibrcom ⊢A≠B∧A≠C∧B≠C∧FFnABC→x=B→F⁡x=AF⁡ABF⁡BCF⁡C⁡x
47 3 25 fvtp3 ⊢A≠C∧B≠C→AF⁡ABF⁡BCF⁡C⁡C=F⁡C
48 47 ad4ant23 ⊢A≠B∧A≠C∧B≠C∧FFnABC→AF⁡ABF⁡BCF⁡C⁡C=F⁡C
49 48 eqcomd ⊢A≠B∧A≠C∧B≠C∧FFnABC→F⁡C=AF⁡ABF⁡BCF⁡C⁡C
50 fveq2 ⊢x=C→F⁡x=F⁡C
51 fveq2 ⊢x=C→AF⁡ABF⁡BCF⁡C⁡x=AF⁡ABF⁡BCF⁡C⁡C
52 50 51 eqeq12d ⊢x=C→F⁡x=AF⁡ABF⁡BCF⁡C⁡x↔F⁡C=AF⁡ABF⁡BCF⁡C⁡C
53 49 52 syl5ibrcom ⊢A≠B∧A≠C∧B≠C∧FFnABC→x=C→F⁡x=AF⁡ABF⁡BCF⁡C⁡x
54 39 46 53 3jaod ⊢A≠B∧A≠C∧B≠C∧FFnABC→x=A∨x=B∨x=C→F⁡x=AF⁡ABF⁡BCF⁡C⁡x
55 32 54 biimtrid ⊢A≠B∧A≠C∧B≠C∧FFnABC→x∈ABC→F⁡x=AF⁡ABF⁡BCF⁡C⁡x
56 30 55 sylbid ⊢A≠B∧A≠C∧B≠C∧FFnABC→x∈dom⁡F→F⁡x=AF⁡ABF⁡BCF⁡C⁡x
57 56 ralrimiv ⊢A≠B∧A≠C∧B≠C∧FFnABC→∀x∈dom⁡FF⁡x=AF⁡ABF⁡BCF⁡C⁡x
58 fnfun ⊢FFnABC→Fun⁡F
59 1 2 3 23 24 25 funtp ⊢A≠B∧A≠C∧B≠C→Fun⁡AF⁡ABF⁡BCF⁡C
60 59 3expa ⊢A≠B∧A≠C∧B≠C→Fun⁡AF⁡ABF⁡BCF⁡C
61 eqfunfv ⊢Fun⁡F∧Fun⁡AF⁡ABF⁡BCF⁡C→F=AF⁡ABF⁡BCF⁡C↔dom⁡F=dom⁡AF⁡ABF⁡BCF⁡C∧∀x∈dom⁡FF⁡x=AF⁡ABF⁡BCF⁡C⁡x
62 58 60 61 syl2anr ⊢A≠B∧A≠C∧B≠C∧FFnABC→F=AF⁡ABF⁡BCF⁡C↔dom⁡F=dom⁡AF⁡ABF⁡BCF⁡C∧∀x∈dom⁡FF⁡x=AF⁡ABF⁡BCF⁡C⁡x
63 28 57 62 mpbir2and ⊢A≠B∧A≠C∧B≠C∧FFnABC→F=AF⁡ABF⁡BCF⁡C
64 1 2 3 23 24 25 fntp ⊢A≠B∧A≠C∧B≠C→AF⁡ABF⁡BCF⁡CFnABC
65 64 3expa ⊢A≠B∧A≠C∧B≠C→AF⁡ABF⁡BCF⁡CFnABC
66 fneq1 ⊢F=AF⁡ABF⁡BCF⁡C→FFnABC↔AF⁡ABF⁡BCF⁡CFnABC
67 66 biimprd ⊢F=AF⁡ABF⁡BCF⁡C→AF⁡ABF⁡BCF⁡CFnABC→FFnABC
68 65 67 mpan9 ⊢A≠B∧A≠C∧B≠C∧F=AF⁡ABF⁡BCF⁡C→FFnABC
69 63 68 impbida ⊢A≠B∧A≠C∧B≠C→FFnABC↔F=AF⁡ABF⁡BCF⁡C
70 69 expcom ⊢B≠C→A≠B∧A≠C→FFnABC↔F=AF⁡ABF⁡BCF⁡C
71 21 70 pm2.61ine ⊢A≠B∧A≠C→FFnABC↔F=AF⁡ABF⁡BCF⁡C
72 1 3 fnprb ⊢FFnAC↔F=AF⁡ACF⁡C
73 tpidm12 ⊢AAC=AC
74 73 eqcomi ⊢AC=AAC
75 74 fneq2i ⊢FFnAC↔FFnAAC
76 tpidm12 ⊢AF⁡AAF⁡ACF⁡C=AF⁡ACF⁡C
77 76 eqcomi ⊢AF⁡ACF⁡C=AF⁡AAF⁡ACF⁡C
78 77 eqeq2i ⊢F=AF⁡ACF⁡C↔F=AF⁡AAF⁡ACF⁡C
79 72 75 78 3bitr3i ⊢FFnAAC↔F=AF⁡AAF⁡ACF⁡C
80 79 a1i ⊢A=B→FFnAAC↔F=AF⁡AAF⁡ACF⁡C
81 tpeq2 ⊢A=B→AAC=ABC
82 81 fneq2d ⊢A=B→FFnAAC↔FFnABC
83 id ⊢A=B→A=B
84 fveq2 ⊢A=B→F⁡A=F⁡B
85 83 84 opeq12d ⊢A=B→AF⁡A=BF⁡B
86 85 tpeq2d ⊢A=B→AF⁡AAF⁡ACF⁡C=AF⁡ABF⁡BCF⁡C
87 86 eqeq2d ⊢A=B→F=AF⁡AAF⁡ACF⁡C↔F=AF⁡ABF⁡BCF⁡C
88 80 82 87 3bitr3d ⊢A=B→FFnABC↔F=AF⁡ABF⁡BCF⁡C
89 tpidm13 ⊢ABA=AB
90 89 eqcomi ⊢AB=ABA
91 90 fneq2i ⊢FFnAB↔FFnABA
92 tpidm13 ⊢AF⁡ABF⁡BAF⁡A=AF⁡ABF⁡B
93 92 eqcomi ⊢AF⁡ABF⁡B=AF⁡ABF⁡BAF⁡A
94 93 eqeq2i ⊢F=AF⁡ABF⁡B↔F=AF⁡ABF⁡BAF⁡A
95 4 91 94 3bitr3i ⊢FFnABA↔F=AF⁡ABF⁡BAF⁡A
96 95 a1i ⊢A=C→FFnABA↔F=AF⁡ABF⁡BAF⁡A
97 tpeq3 ⊢A=C→ABA=ABC
98 97 fneq2d ⊢A=C→FFnABA↔FFnABC
99 id ⊢A=C→A=C
100 fveq2 ⊢A=C→F⁡A=F⁡C
101 99 100 opeq12d ⊢A=C→AF⁡A=CF⁡C
102 101 tpeq3d ⊢A=C→AF⁡ABF⁡BAF⁡A=AF⁡ABF⁡BCF⁡C
103 102 eqeq2d ⊢A=C→F=AF⁡ABF⁡BAF⁡A↔F=AF⁡ABF⁡BCF⁡C
104 96 98 103 3bitr3d ⊢A=C→FFnABC↔F=AF⁡ABF⁡BCF⁡C
105 71 88 104 pm2.61iine ⊢FFnABC↔F=AF⁡ABF⁡BCF⁡C