Metamath Proof Explorer


Theorem hash3tr

Description: A set of size three is an unordered triple. (Contributed by Alexander van der Vekens, 13-Sep-2018)

Ref Expression
Assertion hash3tr VWV=3abcV=abc

Proof

Step Hyp Ref Expression
1 3nn0 30
2 hashvnfin VW30V=3VFin
3 1 2 mpan2 VWV=3VFin
4 3 imp VWV=3VFin
5 hash3 3𝑜=3
6 5 eqcomi 3=3𝑜
7 6 a1i VFin3=3𝑜
8 7 eqeq2d VFinV=3V=3𝑜
9 3onn 3𝑜ω
10 nnfi 3𝑜ω3𝑜Fin
11 9 10 ax-mp 3𝑜Fin
12 hashen VFin3𝑜FinV=3𝑜V3𝑜
13 11 12 mpan2 VFinV=3𝑜V3𝑜
14 13 biimpd VFinV=3𝑜V3𝑜
15 8 14 sylbid VFinV=3V3𝑜
16 15 adantld VFinVWV=3V3𝑜
17 4 16 mpcom VWV=3V3𝑜
18 en3 V3𝑜abcV=abc
19 17 18 syl VWV=3abcV=abc