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 = ( ZZ>= ` N )
Assertion uzct
|- Z ~<_ _om

Proof

Step Hyp Ref Expression
1 uzct.1
 |-  Z = ( ZZ>= ` N )
2 uzssz
 |-  ( ZZ>= ` N ) C_ ZZ
3 1 2 eqsstri
 |-  Z C_ ZZ
4 zex
 |-  ZZ e. _V
5 ssdomg
 |-  ( ZZ e. _V -> ( Z C_ ZZ -> Z ~<_ ZZ ) )
6 4 5 ax-mp
 |-  ( Z C_ ZZ -> Z ~<_ ZZ )
7 3 6 ax-mp
 |-  Z ~<_ ZZ
8 zct
 |-  ZZ ~<_ _om
9 domtr
 |-  ( ( Z ~<_ ZZ /\ ZZ ~<_ _om ) -> Z ~<_ _om )
10 7 8 9 mp2an
 |-  Z ~<_ _om