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

Metamath Proof Explorer

Theorem snnen2o

Description: A singleton { A } is never equinumerous with the ordinal number 2. This holds for proper singletons ( A e.V ) as well as for singletons being the empty set ( A e/ V ). (Contributed by AV, 6-Aug-2019) Avoid ax-pow , ax-un . (Revised by BTernaryTau, 1-Dec-2024)

Ref Expression
Assertion snnen2o ⊢ ¬ A ≈ 2 𝑜

Proof

Step Hyp Ref Expression
1 df2o3 ⊢ 2 𝑜 = ∅ 1 𝑜
2 0ex ⊢ ∅ ∈ V
3 1oex ⊢ 1 𝑜 ∈ V
4 1n0 ⊢ 1 𝑜 ≠ ∅
5 4 necomi ⊢ ∅ ≠ 1 𝑜
6 prnesn ⊢ ∅ ∈ V ∧ 1 𝑜 ∈ V ∧ ∅ ≠ 1 𝑜 → ∅ 1 𝑜 ≠ x
7 2 3 5 6 mp3an ⊢ ∅ 1 𝑜 ≠ x
8 1 7 eqnetri ⊢ 2 𝑜 ≠ x
9 8 neii ⊢ ¬ 2 𝑜 = x
10 9 nex ⊢ ¬ ∃ x 2 𝑜 = x
11 2on0 ⊢ 2 𝑜 ≠ ∅
12 f1cdmsn ⊢ f -1 : 2 𝑜 ⟶ 1-1 A ∧ 2 𝑜 ≠ ∅ → ∃ x 2 𝑜 = x
13 11 12 mpan2 ⊢ f -1 : 2 𝑜 ⟶ 1-1 A → ∃ x 2 𝑜 = x
14 10 13 mto ⊢ ¬ f -1 : 2 𝑜 ⟶ 1-1 A
15 f1ocnv ⊢ f : A ⟶ 1-1 onto 2 𝑜 → f -1 : 2 𝑜 ⟶ 1-1 onto A
16 f1of1 ⊢ f -1 : 2 𝑜 ⟶ 1-1 onto A → f -1 : 2 𝑜 ⟶ 1-1 A
17 15 16 syl ⊢ f : A ⟶ 1-1 onto 2 𝑜 → f -1 : 2 𝑜 ⟶ 1-1 A
18 14 17 mto ⊢ ¬ f : A ⟶ 1-1 onto 2 𝑜
19 18 nex ⊢ ¬ ∃ f f : A ⟶ 1-1 onto 2 𝑜
20 snex ⊢ A ∈ V
21 2oex ⊢ 2 𝑜 ∈ V
22 breng ⊢ A ∈ V ∧ 2 𝑜 ∈ V → A ≈ 2 𝑜 ↔ ∃ f f : A ⟶ 1-1 onto 2 𝑜
23 20 21 22 mp2an ⊢ A ≈ 2 𝑜 ↔ ∃ f f : A ⟶ 1-1 onto 2 𝑜
24 19 23 mtbir ⊢ ¬ A ≈ 2 𝑜