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
|- ( ( V e. W /\ ( # ` V ) = 3 ) -> E. a E. b E. c V = { a , b , c } )

Proof

Step Hyp Ref Expression
1 3nn0
 |-  3 e. NN0
2 hashvnfin
 |-  ( ( V e. W /\ 3 e. NN0 ) -> ( ( # ` V ) = 3 -> V e. Fin ) )
3 1 2 mpan2
 |-  ( V e. W -> ( ( # ` V ) = 3 -> V e. Fin ) )
4 3 imp
 |-  ( ( V e. W /\ ( # ` V ) = 3 ) -> V e. Fin )
5 hash3
 |-  ( # ` 3o ) = 3
6 5 eqcomi
 |-  3 = ( # ` 3o )
7 6 a1i
 |-  ( V e. Fin -> 3 = ( # ` 3o ) )
8 7 eqeq2d
 |-  ( V e. Fin -> ( ( # ` V ) = 3 <-> ( # ` V ) = ( # ` 3o ) ) )
9 3onn
 |-  3o e. _om
10 nnfi
 |-  ( 3o e. _om -> 3o e. Fin )
11 9 10 ax-mp
 |-  3o e. Fin
12 hashen
 |-  ( ( V e. Fin /\ 3o e. Fin ) -> ( ( # ` V ) = ( # ` 3o ) <-> V ~~ 3o ) )
13 11 12 mpan2
 |-  ( V e. Fin -> ( ( # ` V ) = ( # ` 3o ) <-> V ~~ 3o ) )
14 13 biimpd
 |-  ( V e. Fin -> ( ( # ` V ) = ( # ` 3o ) -> V ~~ 3o ) )
15 8 14 sylbid
 |-  ( V e. Fin -> ( ( # ` V ) = 3 -> V ~~ 3o ) )
16 15 adantld
 |-  ( V e. Fin -> ( ( V e. W /\ ( # ` V ) = 3 ) -> V ~~ 3o ) )
17 4 16 mpcom
 |-  ( ( V e. W /\ ( # ` V ) = 3 ) -> V ~~ 3o )
18 en3
 |-  ( V ~~ 3o -> E. a E. b E. c V = { a , b , c } )
19 17 18 syl
 |-  ( ( V e. W /\ ( # ` V ) = 3 ) -> E. a E. b E. c V = { a , b , c } )