Metamath Proof Explorer


Theorem dfom2

Description: An alternate definition of the set of natural numbers _om . Definition 7.28 of TakeutiZaring p. 42, who use the symbol K_I for the restricted class abstraction of non-limit ordinal numbers (see nlimon ). (Contributed by NM, 1-Nov-2004)

Ref Expression
Assertion dfom2 ω = x On | suc x y On | ¬ Lim y

Proof

Step Hyp Ref Expression
1 df-om ω = x On | z Lim z x z
2 vex z V
3 limelon z V Lim z z On
4 2 3 mpan Lim z z On
5 4 pm4.71ri Lim z z On Lim z
6 5 imbi1i Lim z x z z On Lim z x z
7 impexp z On Lim z x z z On Lim z x z
8 con34b Lim z x z ¬ x z ¬ Lim z
9 ibar z On ¬ Lim z z On ¬ Lim z
10 9 imbi2d z On ¬ x z ¬ Lim z ¬ x z z On ¬ Lim z
11 8 10 syl5bb z On Lim z x z ¬ x z z On ¬ Lim z
12 11 pm5.74i z On Lim z x z z On ¬ x z z On ¬ Lim z
13 6 7 12 3bitri Lim z x z z On ¬ x z z On ¬ Lim z
14 onsssuc z On x On z x z suc x
15 ontri1 z On x On z x ¬ x z
16 14 15 bitr3d z On x On z suc x ¬ x z
17 16 ancoms x On z On z suc x ¬ x z
18 limeq y = z Lim y Lim z
19 18 notbid y = z ¬ Lim y ¬ Lim z
20 19 elrab z y On | ¬ Lim y z On ¬ Lim z
21 20 a1i x On z On z y On | ¬ Lim y z On ¬ Lim z
22 17 21 imbi12d x On z On z suc x z y On | ¬ Lim y ¬ x z z On ¬ Lim z
23 22 pm5.74da x On z On z suc x z y On | ¬ Lim y z On ¬ x z z On ¬ Lim z
24 13 23 bitr4id x On Lim z x z z On z suc x z y On | ¬ Lim y
25 impexp z On z suc x z y On | ¬ Lim y z On z suc x z y On | ¬ Lim y
26 simpr z On z suc x z suc x
27 suceloni x On suc x On
28 onelon suc x On z suc x z On
29 28 ex suc x On z suc x z On
30 27 29 syl x On z suc x z On
31 30 ancrd x On z suc x z On z suc x
32 26 31 impbid2 x On z On z suc x z suc x
33 32 imbi1d x On z On z suc x z y On | ¬ Lim y z suc x z y On | ¬ Lim y
34 25 33 bitr3id x On z On z suc x z y On | ¬ Lim y z suc x z y On | ¬ Lim y
35 24 34 bitrd x On Lim z x z z suc x z y On | ¬ Lim y
36 35 albidv x On z Lim z x z z z suc x z y On | ¬ Lim y
37 dfss2 suc x y On | ¬ Lim y z z suc x z y On | ¬ Lim y
38 36 37 bitr4di x On z Lim z x z suc x y On | ¬ Lim y
39 38 rabbiia x On | z Lim z x z = x On | suc x y On | ¬ Lim y
40 1 39 eqtri ω = x On | suc x y On | ¬ Lim y