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

Metamath Proof Explorer

Theorem pr0hash2ex

Description: There is (at least) one set with two different elements: the unordered pair containing the empty set and the singleton containing the empty set. (Contributed by AV, 29-Jan-2020)

Ref Expression
Assertion pr0hash2ex ( ♯ ‘ { ∅ , { ∅ } } ) = 2

Proof

Step Hyp Ref Expression
1 df2o2 ⊢ 2o = { ∅ , { ∅ } }
2 1 eqcomi ⊢ { ∅ , { ∅ } } = 2o
3 2 fveq2i ⊢ ( ♯ ‘ { ∅ , { ∅ } } ) = ( ♯ ‘ 2o )
4 hash2 ⊢ ( ♯ ‘ 2o ) = 2
5 3 4 eqtri ⊢ ( ♯ ‘ { ∅ , { ∅ } } ) = 2