Metamath Proof Explorer


Theorem ssnlim

Description: An ordinal subclass of non-limit ordinals is a class of natural numbers. Exercise 7 of TakeutiZaring p. 42. (Contributed by NM, 2-Nov-2004)

Ref Expression
Assertion ssnlim Ord A A x On | ¬ Lim x A ω

Proof

Step Hyp Ref Expression
1 limom Lim ω
2 ssel A x On | ¬ Lim x ω A ω x On | ¬ Lim x
3 limeq x = ω Lim x Lim ω
4 3 notbid x = ω ¬ Lim x ¬ Lim ω
5 4 elrab ω x On | ¬ Lim x ω On ¬ Lim ω
6 5 simprbi ω x On | ¬ Lim x ¬ Lim ω
7 2 6 syl6 A x On | ¬ Lim x ω A ¬ Lim ω
8 1 7 mt2i A x On | ¬ Lim x ¬ ω A
9 8 adantl Ord A A x On | ¬ Lim x ¬ ω A
10 ordom Ord ω
11 ordtri1 Ord A Ord ω A ω ¬ ω A
12 10 11 mpan2 Ord A A ω ¬ ω A
13 12 adantr Ord A A x On | ¬ Lim x A ω ¬ ω A
14 9 13 mpbird Ord A A x On | ¬ Lim x A ω