Description: A set of size three is an unordered triple. (Contributed by Alexander van der Vekens, 13-Sep-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | hash3tr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3nn0 | |
|
2 | hashvnfin | |
|
3 | 1 2 | mpan2 | |
4 | 3 | imp | |
5 | hash3 | |
|
6 | 5 | eqcomi | |
7 | 6 | a1i | |
8 | 7 | eqeq2d | |
9 | 3onn | |
|
10 | nnfi | |
|
11 | 9 10 | ax-mp | |
12 | hashen | |
|
13 | 11 12 | mpan2 | |
14 | 13 | biimpd | |
15 | 8 14 | sylbid | |
16 | 15 | adantld | |
17 | 4 16 | mpcom | |
18 | en3 | |
|
19 | 17 18 | syl | |