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