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 ( 𝐴𝑉 → ( ¬ 𝐴 ∈ ( ♯ “ { 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 < ( ♯ ‘ 𝐴 ) ) )