Metamath Proof Explorer

Theorem dfom3

Description: The class of natural numbers _om can be defined as the intersection of all inductive sets (which is the smallest inductive set, since inductive sets are closed under intersection), which is valid provided we assume the Axiom of Infinity. Definition 6.3 of Eisenberg p. 82. (Contributed by NM, 6-Aug-1994)

Ref Expression
Assertion dfom3 
|- _om = |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) }

Proof

Step Hyp Ref Expression
1 0ex 
 |-  (/) e. _V
2 1 elintab 
 |-  ( (/) e. |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) } <-> A. x ( ( (/) e. x /\ A. y e. x suc y e. x ) -> (/) e. x ) )
3 simpl 
 |-  ( ( (/) e. x /\ A. y e. x suc y e. x ) -> (/) e. x )
4 2 3 mpgbir 
 |-  (/) e. |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) }
5 suceq 
 |-  ( y = z -> suc y = suc z )
6 5 eleq1d 
 |-  ( y = z -> ( suc y e. x <-> suc z e. x ) )
7 6 rspccv 
 |-  ( A. y e. x suc y e. x -> ( z e. x -> suc z e. x ) )
8 7 adantl 
 |-  ( ( (/) e. x /\ A. y e. x suc y e. x ) -> ( z e. x -> suc z e. x ) )
9 8 a2i 
 |-  ( ( ( (/) e. x /\ A. y e. x suc y e. x ) -> z e. x ) -> ( ( (/) e. x /\ A. y e. x suc y e. x ) -> suc z e. x ) )
10 9 alimi 
 |-  ( A. x ( ( (/) e. x /\ A. y e. x suc y e. x ) -> z e. x ) -> A. x ( ( (/) e. x /\ A. y e. x suc y e. x ) -> suc z e. x ) )
11 vex 
 |-  z e. _V
12 11 elintab 
 |-  ( z e. |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) } <-> A. x ( ( (/) e. x /\ A. y e. x suc y e. x ) -> z e. x ) )
13 11 sucex 
 |-  suc z e. _V
14 13 elintab 
 |-  ( suc z e. |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) } <-> A. x ( ( (/) e. x /\ A. y e. x suc y e. x ) -> suc z e. x ) )
15 10 12 14 3imtr4i 
 |-  ( z e. |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) } -> suc z e. |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) } )
16 15 rgenw 
 |-  A. z e. _om ( z e. |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) } -> suc z e. |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) } )
17 peano5 
 |-  ( ( (/) e. |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) } /\ A. z e. _om ( z e. |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) } -> suc z e. |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) } ) ) -> _om C_ |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) } )
18 4 16 17 mp2an 
 |-  _om C_ |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) }
19 peano1 
 |-  (/) e. _om
20 peano2 
 |-  ( y e. _om -> suc y e. _om )
21 20 rgen 
 |-  A. y e. _om suc y e. _om
22 omex 
 |-  _om e. _V
23 eleq2 
 |-  ( x = _om -> ( (/) e. x <-> (/) e. _om ) )
24 eleq2 
 |-  ( x = _om -> ( suc y e. x <-> suc y e. _om ) )
25 24 raleqbi1dv 
 |-  ( x = _om -> ( A. y e. x suc y e. x <-> A. y e. _om suc y e. _om ) )
26 23 25 anbi12d 
 |-  ( x = _om -> ( ( (/) e. x /\ A. y e. x suc y e. x ) <-> ( (/) e. _om /\ A. y e. _om suc y e. _om ) ) )
27 eleq2 
 |-  ( x = _om -> ( z e. x <-> z e. _om ) )
28 26 27 imbi12d 
 |-  ( x = _om -> ( ( ( (/) e. x /\ A. y e. x suc y e. x ) -> z e. x ) <-> ( ( (/) e. _om /\ A. y e. _om suc y e. _om ) -> z e. _om ) ) )
29 22 28 spcv 
 |-  ( A. x ( ( (/) e. x /\ A. y e. x suc y e. x ) -> z e. x ) -> ( ( (/) e. _om /\ A. y e. _om suc y e. _om ) -> z e. _om ) )
30 12 29 sylbi 
 |-  ( z e. |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) } -> ( ( (/) e. _om /\ A. y e. _om suc y e. _om ) -> z e. _om ) )
31 19 21 30 mp2ani 
 |-  ( z e. |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) } -> z e. _om )
32 31 ssriv 
 |-  |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) } C_ _om
33 18 32 eqssi 
 |-  _om = |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) }