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 ) ) )