Description: A function with a domain of three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | ftpg | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simpa | |
|
2 | 3simpa | |
|
3 | simp1 | |
|
4 | fprg | |
|
5 | 1 2 3 4 | syl3an | |
6 | eqidd | |
|
7 | simp3 | |
|
8 | simp3 | |
|
9 | 7 8 | anim12i | |
10 | 9 | 3adant3 | |
11 | fsng | |
|
12 | 10 11 | syl | |
13 | 6 12 | mpbird | |
14 | elpri | |
|
15 | eqcom | |
|
16 | nne | |
|
17 | 15 16 | bitr4i | |
18 | eqcom | |
|
19 | nne | |
|
20 | 18 19 | bitr4i | |
21 | 17 20 | orbi12i | |
22 | ianor | |
|
23 | 21 22 | sylbb2 | |
24 | 14 23 | syl | |
25 | 24 | con2i | |
26 | 25 | 3adant1 | |
27 | 26 | 3ad2ant3 | |
28 | disjsn | |
|
29 | 27 28 | sylibr | |
30 | fun | |
|
31 | 5 13 29 30 | syl21anc | |
32 | df-tp | |
|
33 | 32 | feq1i | |
34 | df-tp | |
|
35 | df-tp | |
|
36 | 34 35 | feq23i | |
37 | 33 36 | bitri | |
38 | 31 37 | sylibr | |