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	⊢ ( 𝐴 ∈ 𝑉 → ( ¬ 𝐴 ∈ ( ◡ ♯ “ { 0 , 1 } ) ↔ 1 < ( ♯ ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		hashf	⊢ ♯ : V ⟶ ( ℕ0 ∪ { +∞ } )
2		ffn	⊢ ( ♯ : V ⟶ ( ℕ0 ∪ { +∞ } ) → ♯ Fn V )
3		elpreima	⊢ ( ♯ Fn V → ( 𝐴 ∈ ( ◡ ♯ “ { 0 , 1 } ) ↔ ( 𝐴 ∈ V ∧ ( ♯ ‘ 𝐴 ) ∈ { 0 , 1 } ) ) )
4	1 2 3	mp2b	⊢ ( 𝐴 ∈ ( ◡ ♯ “ { 0 , 1 } ) ↔ ( 𝐴 ∈ V ∧ ( ♯ ‘ 𝐴 ) ∈ { 0 , 1 } ) )
5		elex	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
6	5	biantrurd	⊢ ( 𝐴 ∈ 𝑉 → ( ( ♯ ‘ 𝐴 ) ∈ { 0 , 1 } ↔ ( 𝐴 ∈ V ∧ ( ♯ ‘ 𝐴 ) ∈ { 0 , 1 } ) ) )
7	4 6	bitr4id	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ( ◡ ♯ “ { 0 , 1 } ) ↔ ( ♯ ‘ 𝐴 ) ∈ { 0 , 1 } ) )
8	7	notbid	⊢ ( 𝐴 ∈ 𝑉 → ( ¬ 𝐴 ∈ ( ◡ ♯ “ { 0 , 1 } ) ↔ ¬ ( ♯ ‘ 𝐴 ) ∈ { 0 , 1 } ) )
9		hashxnn0	⊢ ( 𝐴 ∈ 𝑉 → ( ♯ ‘ 𝐴 ) ∈ ℕ0* )
10		xnn01gt	⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0* → ( ¬ ( ♯ ‘ 𝐴 ) ∈ { 0 , 1 } ↔ 1 < ( ♯ ‘ 𝐴 ) ) )
11	9 10	syl	⊢ ( 𝐴 ∈ 𝑉 → ( ¬ ( ♯ ‘ 𝐴 ) ∈ { 0 , 1 } ↔ 1 < ( ♯ ‘ 𝐴 ) ) )
12	8 11	bitrd	⊢ ( 𝐴 ∈ 𝑉 → ( ¬ 𝐴 ∈ ( ◡ ♯ “ { 0 , 1 } ) ↔ 1 < ( ♯ ‘ 𝐴 ) ) )