Metamath Proof Explorer

Theorem hash1snb

Description: The size of a set is 1 if and only if it is a singleton (containing a set). (Contributed by Alexander van der Vekens, 7-Dec-2017)

Ref Expression
Assertion hash1snb 
|- ( V e. W -> ( ( # ` V ) = 1 <-> E. a V = { a } ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( ( # ` V ) = 1 -> ( # ` V ) = 1 )
2 hash1 
 |-  ( # ` 1o ) = 1
3 1 2 eqtr4di 
 |-  ( ( # ` V ) = 1 -> ( # ` V ) = ( # ` 1o ) )
4 3 adantl 
 |-  ( ( V e. Fin /\ ( # ` V ) = 1 ) -> ( # ` V ) = ( # ` 1o ) )
5 1onn 
 |-  1o e. _om
6 nnfi 
 |-  ( 1o e. _om -> 1o e. Fin )
7 5 6 mp1i 
 |-  ( ( # ` V ) = 1 -> 1o e. Fin )
8 hashen 
 |-  ( ( V e. Fin /\ 1o e. Fin ) -> ( ( # ` V ) = ( # ` 1o ) <-> V ~~ 1o ) )
9 7 8 sylan2 
 |-  ( ( V e. Fin /\ ( # ` V ) = 1 ) -> ( ( # ` V ) = ( # ` 1o ) <-> V ~~ 1o ) )
10 4 9 mpbid 
 |-  ( ( V e. Fin /\ ( # ` V ) = 1 ) -> V ~~ 1o )
11 en1 
 |-  ( V ~~ 1o <-> E. a V = { a } )
12 10 11 sylib 
 |-  ( ( V e. Fin /\ ( # ` V ) = 1 ) -> E. a V = { a } )
13 12 ex 
 |-  ( V e. Fin -> ( ( # ` V ) = 1 -> E. a V = { a } ) )
14 13 a1d 
 |-  ( V e. Fin -> ( V e. W -> ( ( # ` V ) = 1 -> E. a V = { a } ) ) )
15 hashinf 
 |-  ( ( V e. W /\ -. V e. Fin ) -> ( # ` V ) = +oo )
16 eqeq1 
 |-  ( ( # ` V ) = +oo -> ( ( # ` V ) = 1 <-> +oo = 1 ) )
17 1re 
 |-  1 e. RR
18 renepnf 
 |-  ( 1 e. RR -> 1 =/= +oo )
19 df-ne 
 |-  ( 1 =/= +oo <-> -. 1 = +oo )
20 pm2.21 
 |-  ( -. 1 = +oo -> ( 1 = +oo -> E. a V = { a } ) )
21 19 20 sylbi 
 |-  ( 1 =/= +oo -> ( 1 = +oo -> E. a V = { a } ) )
22 17 18 21 mp2b 
 |-  ( 1 = +oo -> E. a V = { a } )
23 22 eqcoms 
 |-  ( +oo = 1 -> E. a V = { a } )
24 16 23 syl6bi 
 |-  ( ( # ` V ) = +oo -> ( ( # ` V ) = 1 -> E. a V = { a } ) )
25 15 24 syl 
 |-  ( ( V e. W /\ -. V e. Fin ) -> ( ( # ` V ) = 1 -> E. a V = { a } ) )
26 25 expcom 
 |-  ( -. V e. Fin -> ( V e. W -> ( ( # ` V ) = 1 -> E. a V = { a } ) ) )
27 14 26 pm2.61i 
 |-  ( V e. W -> ( ( # ` V ) = 1 -> E. a V = { a } ) )
28 fveq2 
 |-  ( V = { a } -> ( # ` V ) = ( # ` { a } ) )
29 hashsng 
 |-  ( a e. _V -> ( # ` { a } ) = 1 )
30 29 elv 
 |-  ( # ` { a } ) = 1
31 28 30 eqtrdi 
 |-  ( V = { a } -> ( # ` V ) = 1 )
32 31 exlimiv 
 |-  ( E. a V = { a } -> ( # ` V ) = 1 )
33 27 32 impbid1 
 |-  ( V e. W -> ( ( # ` V ) = 1 <-> E. a V = { a } ) )