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 ↔ ∃ 𝑎 𝑉 = { 𝑎 } ) )