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=N
Assertion uzct Zω

Proof

Step Hyp Ref Expression
1 uzct.1 Z=N
2 uzssz N
3 1 2 eqsstri Z
4 zex V
5 ssdomg VZZ
6 4 5 ax-mp ZZ
7 3 6 ax-mp Z
8 zct ω
9 domtr ZωZω
10 7 8 9 mp2an Zω