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 ( 𝑉𝑊 → ( ( ♯ ‘ 𝑉 ) = 1 ↔ ∃ 𝑎 𝑉 = { 𝑎 } ) )

Proof

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