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

Metamath Proof Explorer

Theorem hashen1

Description: A set has size 1 if and only if it is equinumerous to the ordinal 1. (Contributed by AV, 14-Apr-2019)

Ref Expression
Assertion hashen1 
|- ( A e. V -> ( ( # ` A ) = 1 <-> A ~~ 1o ) )

Proof

Step Hyp Ref Expression
1 0ex 
 |-  (/) e. _V
2 hashsng 
 |-  ( (/) e. _V -> ( # ` { (/) } ) = 1 )
3 1 2 ax-mp 
 |-  ( # ` { (/) } ) = 1
4 3 eqcomi 
 |-  1 = ( # ` { (/) } )
5 4 a1i 
 |-  ( A e. V -> 1 = ( # ` { (/) } ) )
6 5 eqeq2d 
 |-  ( A e. V -> ( ( # ` A ) = 1 <-> ( # ` A ) = ( # ` { (/) } ) ) )
7 simpr 
 |-  ( ( A e. V /\ ( # ` A ) = ( # ` { (/) } ) ) -> ( # ` A ) = ( # ` { (/) } ) )
8 1nn0 
 |-  1 e. NN0
9 3 8 eqeltri 
 |-  ( # ` { (/) } ) e. NN0
10 hashvnfin 
 |-  ( ( A e. V /\ ( # ` { (/) } ) e. NN0 ) -> ( ( # ` A ) = ( # ` { (/) } ) -> A e. Fin ) )
11 9 10 mpan2 
 |-  ( A e. V -> ( ( # ` A ) = ( # ` { (/) } ) -> A e. Fin ) )
12 11 imp 
 |-  ( ( A e. V /\ ( # ` A ) = ( # ` { (/) } ) ) -> A e. Fin )
13 snfi 
 |-  { (/) } e. Fin
14 hashen 
 |-  ( ( A e. Fin /\ { (/) } e. Fin ) -> ( ( # ` A ) = ( # ` { (/) } ) <-> A ~~ { (/) } ) )
15 12 13 14 sylancl 
 |-  ( ( A e. V /\ ( # ` A ) = ( # ` { (/) } ) ) -> ( ( # ` A ) = ( # ` { (/) } ) <-> A ~~ { (/) } ) )
16 7 15 mpbid 
 |-  ( ( A e. V /\ ( # ` A ) = ( # ` { (/) } ) ) -> A ~~ { (/) } )
17 16 ex 
 |-  ( A e. V -> ( ( # ` A ) = ( # ` { (/) } ) -> A ~~ { (/) } ) )
18 hasheni 
 |-  ( A ~~ { (/) } -> ( # ` A ) = ( # ` { (/) } ) )
19 17 18 impbid1 
 |-  ( A e. V -> ( ( # ` A ) = ( # ` { (/) } ) <-> A ~~ { (/) } ) )
20 df1o2 
 |-  1o = { (/) }
21 20 eqcomi 
 |-  { (/) } = 1o
22 21 breq2i 
 |-  ( A ~~ { (/) } <-> A ~~ 1o )
23 22 a1i 
 |-  ( A e. V -> ( A ~~ { (/) } <-> A ~~ 1o ) )
24 6 19 23 3bitrd 
 |-  ( A e. V -> ( ( # ` A ) = 1 <-> A ~~ 1o ) )