This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 } )