Theorem snct

Description: A singleton is countable. (Contributed by Thierry Arnoux, 16-Sep-2016)

	Ref	Expression
Assertion	snct	⊢ ( 𝐴 ∈ 𝑉 → { 𝐴 } ≼ ω )

Proof

Step	Hyp	Ref	Expression
1		ensn1g	⊢ ( 𝐴 ∈ 𝑉 → { 𝐴 } ≈ 1o )
2		peano1	⊢ ∅ ∈ ω
3	2	ne0ii	⊢ ω ≠ ∅
4		omex	⊢ ω ∈ V
5	4	0sdom	⊢ ( ∅ ≺ ω ↔ ω ≠ ∅ )
6	3 5	mpbir	⊢ ∅ ≺ ω
7		0sdom1dom	⊢ ( ∅ ≺ ω ↔ 1o ≼ ω )
8	6 7	mpbi	⊢ 1o ≼ ω
9		endomtr	⊢ ( ( { 𝐴 } ≈ 1o ∧ 1o ≼ ω ) → { 𝐴 } ≼ ω )
10	1 8 9	sylancl	⊢ ( 𝐴 ∈ 𝑉 → { 𝐴 } ≼ ω )