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

Metamath Proof Explorer

Theorem uzct

Description: An upper integer set is countable. (Contributed by Glauco Siliprandi, 17-Aug-2020)

		Ref	Expression
	Hypothesis	uzct.1	$⊢ Z = ℤ_{\geq N}$
	Assertion	uzct	$⊢ Z ≼ ω$

Step	Hyp	Ref	Expression
1		uzct.1	$⊢ Z = ℤ_{\geq N}$
2		uzssz	$⊢ ℤ_{\geq N} \subseteq ℤ$
3	1 2	eqsstri	$⊢ Z \subseteq ℤ$
4		zex	$⊢ ℤ \in V$
5		ssdomg	$⊢ ℤ \in V \to (Z \subseteq ℤ \to Z ≼ ℤ)$
6	4 5	ax-mp	$⊢ Z \subseteq ℤ \to Z ≼ ℤ$
7	3 6	ax-mp	$⊢ Z ≼ ℤ$
8		zct	$⊢ ℤ ≼ ω$
9		domtr	$⊢ (Z ≼ ℤ \land ℤ ≼ ω) \to Z ≼ ω$
10	7 8 9	mp2an	$⊢ Z ≼ ω$