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 onsssuc 
 |-  ( ( z e. On /\ x e. On ) -> ( z C_ x <-> z e. suc x ) )
3 ontri1 
 |-  ( ( z e. On /\ x e. On ) -> ( z C_ x <-> -. x e. z ) )
4 2 3 bitr3d 
 |-  ( ( z e. On /\ x e. On ) -> ( z e. suc x <-> -. x e. z ) )
5 4 ancoms 
 |-  ( ( x e. On /\ z e. On ) -> ( z e. suc x <-> -. x e. z ) )
6 limeq 
 |-  ( y = z -> ( Lim y <-> Lim z ) )
7 6 notbid 
 |-  ( y = z -> ( -. Lim y <-> -. Lim z ) )
8 7 elrab 
 |-  ( z e. { y e. On | -. Lim y } <-> ( z e. On /\ -. Lim z ) )
9 8 a1i 
 |-  ( ( x e. On /\ z e. On ) -> ( z e. { y e. On | -. Lim y } <-> ( z e. On /\ -. Lim z ) ) )
10 5 9 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 ) ) ) )
11 10 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 ) ) ) ) )
12 vex 
 |-  z e. _V
13 limelon 
 |-  ( ( z e. _V /\ Lim z ) -> z e. On )
14 12 13 mpan 
 |-  ( Lim z -> z e. On )
15 14 pm4.71ri 
 |-  ( Lim z <-> ( z e. On /\ Lim z ) )
16 15 imbi1i 
 |-  ( ( Lim z -> x e. z ) <-> ( ( z e. On /\ Lim z ) -> x e. z ) )
17 impexp 
 |-  ( ( ( z e. On /\ Lim z ) -> x e. z ) <-> ( z e. On -> ( Lim z -> x e. z ) ) )
18 con34b 
 |-  ( ( Lim z -> x e. z ) <-> ( -. x e. z -> -. Lim z ) )
19 ibar 
 |-  ( z e. On -> ( -. Lim z <-> ( z e. On /\ -. Lim z ) ) )
20 19 imbi2d 
 |-  ( z e. On -> ( ( -. x e. z -> -. Lim z ) <-> ( -. x e. z -> ( z e. On /\ -. Lim z ) ) ) )
21 18 20 syl5bb 
 |-  ( z e. On -> ( ( Lim z -> x e. z ) <-> ( -. x e. z -> ( z e. On /\ -. Lim z ) ) ) )
22 21 pm5.74i 
 |-  ( ( z e. On -> ( Lim z -> x e. z ) ) <-> ( z e. On -> ( -. x e. z -> ( z e. On /\ -. Lim z ) ) ) )
23 16 17 22 3bitri 
 |-  ( ( Lim z -> x e. z ) <-> ( z e. On -> ( -. x e. z -> ( z e. On /\ -. Lim z ) ) ) )
24 11 23 syl6rbbr 
 |-  ( 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 syl6bbr 
 |-  ( 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 } }