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 
|- _om = { x e. On | suc x C_ { y e. On | -. Lim y } }

Proof

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