Metamath Proof Explorer

Theorem hash1snb

Description: The size of a set is 1 if and only if it is a singleton (containing a set). (Contributed by Alexander van der Vekens, 7-Dec-2017)

Ref Expression
Assertion hash1snb ⊢ V ∈ W → V = 1 ↔ ∃ a V = a

Proof

Step Hyp Ref Expression
1 id ⊢ V = 1 → V = 1
2 hash1 ⊢ 1 𝑜 = 1
3 1 2 eqtr4di ⊢ V = 1 → V = 1 𝑜
4 3 adantl ⊢ V ∈ Fin ∧ V = 1 → V = 1 𝑜
5 1onn ⊢ 1 𝑜 ∈ ω
6 nnfi ⊢ 1 𝑜 ∈ ω → 1 𝑜 ∈ Fin
7 5 6 mp1i ⊢ V = 1 → 1 𝑜 ∈ Fin
8 hashen ⊢ V ∈ Fin ∧ 1 𝑜 ∈ Fin → V = 1 𝑜 ↔ V ≈ 1 𝑜
9 7 8 sylan2 ⊢ V ∈ Fin ∧ V = 1 → V = 1 𝑜 ↔ V ≈ 1 𝑜
10 4 9 mpbid ⊢ V ∈ Fin ∧ V = 1 → V ≈ 1 𝑜
11 en1 ⊢ V ≈ 1 𝑜 ↔ ∃ a V = a
12 10 11 sylib ⊢ V ∈ Fin ∧ V = 1 → ∃ a V = a
13 12 ex ⊢ V ∈ Fin → V = 1 → ∃ a V = a
14 13 a1d ⊢ V ∈ Fin → V ∈ W → V = 1 → ∃ a V = a
15 hashinf ⊢ V ∈ W ∧ ¬ V ∈ Fin → V = +∞
16 eqeq1 ⊢ V = +∞ → V = 1 ↔ +∞ = 1
17 1re ⊢ 1 ∈ ℝ
18 renepnf ⊢ 1 ∈ ℝ → 1 ≠ +∞
19 df-ne ⊢ 1 ≠ +∞ ↔ ¬ 1 = +∞
20 pm2.21 ⊢ ¬ 1 = +∞ → 1 = +∞ → ∃ a V = a
21 19 20 sylbi ⊢ 1 ≠ +∞ → 1 = +∞ → ∃ a V = a
22 17 18 21 mp2b ⊢ 1 = +∞ → ∃ a V = a
23 22 eqcoms ⊢ +∞ = 1 → ∃ a V = a
24 16 23 syl6bi ⊢ V = +∞ → V = 1 → ∃ a V = a
25 15 24 syl ⊢ V ∈ W ∧ ¬ V ∈ Fin → V = 1 → ∃ a V = a
26 25 expcom ⊢ ¬ V ∈ Fin → V ∈ W → V = 1 → ∃ a V = a
27 14 26 pm2.61i ⊢ V ∈ W → V = 1 → ∃ a V = a
28 fveq2 ⊢ V = a → V = a
29 hashsng ⊢ a ∈ V → a = 1
30 29 elv ⊢ a = 1
31 28 30 eqtrdi ⊢ V = a → V = 1
32 31 exlimiv ⊢ ∃ a V = a → V = 1
33 27 32 impbid1 ⊢ V ∈ W → V = 1 ↔ ∃ a V = a