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

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 biimtrdi ⊢ ( ( ♯ ‘ 𝑉 ) = +∞ → ( ( ♯ ‘ 𝑉 ) = 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 ↔ ∃ 𝑎 𝑉 = { 𝑎 } ) )