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

Metamath Proof Explorer

Theorem hash2pr

Description: A set of size two is an unordered pair. (Contributed by Alexander van der Vekens, 8-Dec-2017)

Ref Expression
Assertion hash2pr 
|- ( ( V e. W /\ ( # ` V ) = 2 ) -> E. a E. b V = { a , b } )

Proof

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