Theorem hashen1

Description: A set has size 1 if and only if it is equinumerous to the ordinal 1. (Contributed by AV, 14-Apr-2019)

	Ref	Expression
Assertion	hashen1	⊢ ( 𝐴 ∈ 𝑉 → ( ( ♯ ‘ 𝐴 ) = 1 ↔ 𝐴 ≈ 1o ) )

Proof

Step	Hyp	Ref	Expression
1		0ex	⊢ ∅ ∈ V
2		hashsng	⊢ ( ∅ ∈ V → ( ♯ ‘ { ∅ } ) = 1 )
3	1 2	ax-mp	⊢ ( ♯ ‘ { ∅ } ) = 1
4	3	eqcomi	⊢ 1 = ( ♯ ‘ { ∅ } )
5	4	a1i	⊢ ( 𝐴 ∈ 𝑉 → 1 = ( ♯ ‘ { ∅ } ) )
6	5	eqeq2d	⊢ ( 𝐴 ∈ 𝑉 → ( ( ♯ ‘ 𝐴 ) = 1 ↔ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ { ∅ } ) ) )
7		simpr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ { ∅ } ) ) → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ { ∅ } ) )
8		1nn0	⊢ 1 ∈ ℕ0
9	3 8	eqeltri	⊢ ( ♯ ‘ { ∅ } ) ∈ ℕ0
10		hashvnfin	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ♯ ‘ { ∅ } ) ∈ ℕ0 ) → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ { ∅ } ) → 𝐴 ∈ Fin ) )
11	9 10	mpan2	⊢ ( 𝐴 ∈ 𝑉 → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ { ∅ } ) → 𝐴 ∈ Fin ) )
12	11	imp	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ { ∅ } ) ) → 𝐴 ∈ Fin )
13		snfi	⊢ { ∅ } ∈ Fin
14		hashen	⊢ ( ( 𝐴 ∈ Fin ∧ { ∅ } ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ { ∅ } ) ↔ 𝐴 ≈ { ∅ } ) )
15	12 13 14	sylancl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ { ∅ } ) ) → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ { ∅ } ) ↔ 𝐴 ≈ { ∅ } ) )
16	7 15	mpbid	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ { ∅ } ) ) → 𝐴 ≈ { ∅ } )
17	16	ex	⊢ ( 𝐴 ∈ 𝑉 → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ { ∅ } ) → 𝐴 ≈ { ∅ } ) )
18		hasheni	⊢ ( 𝐴 ≈ { ∅ } → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ { ∅ } ) )
19	17 18	impbid1	⊢ ( 𝐴 ∈ 𝑉 → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ { ∅ } ) ↔ 𝐴 ≈ { ∅ } ) )
20		df1o2	⊢ 1o = { ∅ }
21	20	eqcomi	⊢ { ∅ } = 1o
22	21	breq2i	⊢ ( 𝐴 ≈ { ∅ } ↔ 𝐴 ≈ 1o )
23	22	a1i	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ≈ { ∅ } ↔ 𝐴 ≈ 1o ) )
24	6 19 23	3bitrd	⊢ ( 𝐴 ∈ 𝑉 → ( ( ♯ ‘ 𝐴 ) = 1 ↔ 𝐴 ≈ 1o ) )