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 biimtrid ⊢ 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