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

Metamath Proof Explorer

Theorem hash2prde

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

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

Proof

Step Hyp Ref Expression
1 hash2pr 
 |-  ( ( V e. W /\ ( # ` V ) = 2 ) -> E. a E. b V = { a , b } )
2 equid 
 |-  b = b
3 vex 
 |-  a e. _V
4 vex 
 |-  b e. _V
5 3 4 preqsn 
 |-  ( { a , b } = { b } <-> ( a = b /\ b = b ) )
6 eqeq2 
 |-  ( { a , b } = { b } -> ( V = { a , b } <-> V = { b } ) )
7 fveq2 
 |-  ( V = { b } -> ( # ` V ) = ( # ` { b } ) )
8 hashsng 
 |-  ( b e. _V -> ( # ` { b } ) = 1 )
9 8 elv 
 |-  ( # ` { b } ) = 1
10 7 9 eqtrdi 
 |-  ( V = { b } -> ( # ` V ) = 1 )
11 eqeq1 
 |-  ( ( # ` V ) = 2 -> ( ( # ` V ) = 1 <-> 2 = 1 ) )
12 1ne2 
 |-  1 =/= 2
13 df-ne 
 |-  ( 1 =/= 2 <-> -. 1 = 2 )
14 pm2.21 
 |-  ( -. 1 = 2 -> ( 1 = 2 -> a =/= b ) )
15 13 14 sylbi 
 |-  ( 1 =/= 2 -> ( 1 = 2 -> a =/= b ) )
16 12 15 ax-mp 
 |-  ( 1 = 2 -> a =/= b )
17 16 eqcoms 
 |-  ( 2 = 1 -> a =/= b )
18 11 17 biimtrdi 
 |-  ( ( # ` V ) = 2 -> ( ( # ` V ) = 1 -> a =/= b ) )
19 18 adantl 
 |-  ( ( V e. W /\ ( # ` V ) = 2 ) -> ( ( # ` V ) = 1 -> a =/= b ) )
20 10 19 syl5com 
 |-  ( V = { b } -> ( ( V e. W /\ ( # ` V ) = 2 ) -> a =/= b ) )
21 6 20 biimtrdi 
 |-  ( { a , b } = { b } -> ( V = { a , b } -> ( ( V e. W /\ ( # ` V ) = 2 ) -> a =/= b ) ) )
22 21 impcomd 
 |-  ( { a , b } = { b } -> ( ( ( V e. W /\ ( # ` V ) = 2 ) /\ V = { a , b } ) -> a =/= b ) )
23 5 22 sylbir 
 |-  ( ( a = b /\ b = b ) -> ( ( ( V e. W /\ ( # ` V ) = 2 ) /\ V = { a , b } ) -> a =/= b ) )
24 2 23 mpan2 
 |-  ( a = b -> ( ( ( V e. W /\ ( # ` V ) = 2 ) /\ V = { a , b } ) -> a =/= b ) )
25 ax-1 
 |-  ( a =/= b -> ( ( ( V e. W /\ ( # ` V ) = 2 ) /\ V = { a , b } ) -> a =/= b ) )
26 24 25 pm2.61ine 
 |-  ( ( ( V e. W /\ ( # ` V ) = 2 ) /\ V = { a , b } ) -> a =/= b )
27 simpr 
 |-  ( ( ( V e. W /\ ( # ` V ) = 2 ) /\ V = { a , b } ) -> V = { a , b } )
28 26 27 jca 
 |-  ( ( ( V e. W /\ ( # ` V ) = 2 ) /\ V = { a , b } ) -> ( a =/= b /\ V = { a , b } ) )
29 28 ex 
 |-  ( ( V e. W /\ ( # ` V ) = 2 ) -> ( V = { a , b } -> ( a =/= b /\ V = { a , b } ) ) )
30 29 2eximdv 
 |-  ( ( V e. W /\ ( # ` V ) = 2 ) -> ( E. a E. b V = { a , b } -> E. a E. b ( a =/= b /\ V = { a , b } ) ) )
31 1 30 mpd 
 |-  ( ( V e. W /\ ( # ` V ) = 2 ) -> E. a E. b ( a =/= b /\ V = { a , b } ) )