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

Metamath Proof Explorer

Theorem hashgt1

Description: Restate "set contains at least two elements" in terms of elementhood. (Contributed by Thierry Arnoux, 21-Nov-2023)

Ref Expression
Assertion hashgt1 
|- ( A e. V -> ( -. A e. ( `' # " { 0 , 1 } ) <-> 1 < ( # ` A ) ) )

Proof

Step Hyp Ref Expression
1 hashf 
 |-  # : _V --> ( NN0 u. { +oo } )
2 ffn 
 |-  ( # : _V --> ( NN0 u. { +oo } ) -> # Fn _V )
3 elpreima 
 |-  ( # Fn _V -> ( A e. ( `' # " { 0 , 1 } ) <-> ( A e. _V /\ ( # ` A ) e. { 0 , 1 } ) ) )
4 1 2 3 mp2b 
 |-  ( A e. ( `' # " { 0 , 1 } ) <-> ( A e. _V /\ ( # ` A ) e. { 0 , 1 } ) )
5 elex 
 |-  ( A e. V -> A e. _V )
6 5 biantrurd 
 |-  ( A e. V -> ( ( # ` A ) e. { 0 , 1 } <-> ( A e. _V /\ ( # ` A ) e. { 0 , 1 } ) ) )
7 4 6 bitr4id 
 |-  ( A e. V -> ( A e. ( `' # " { 0 , 1 } ) <-> ( # ` A ) e. { 0 , 1 } ) )
8 7 notbid 
 |-  ( A e. V -> ( -. A e. ( `' # " { 0 , 1 } ) <-> -. ( # ` A ) e. { 0 , 1 } ) )
9 hashxnn0 
 |-  ( A e. V -> ( # ` A ) e. NN0* )
10 xnn01gt 
 |-  ( ( # ` A ) e. NN0* -> ( -. ( # ` A ) e. { 0 , 1 } <-> 1 < ( # ` A ) ) )
11 9 10 syl 
 |-  ( A e. V -> ( -. ( # ` A ) e. { 0 , 1 } <-> 1 < ( # ` A ) ) )
12 8 11 bitrd 
 |-  ( A e. V -> ( -. A e. ( `' # " { 0 , 1 } ) <-> 1 < ( # ` A ) ) )