Metamath Proof Explorer


Theorem dfnn2

Description: Alternate definition of the set of positive integers. This was our original definition, before the current df-nn replaced it. This definition requires the axiom of infinity to ensure it has the properties we expect. (Contributed by Jeff Hankins, 12-Sep-2013) (Revised by Mario Carneiro, 3-May-2014)

Ref Expression
Assertion dfnn2 = x | 1 x y x y + 1 x

Proof

Step Hyp Ref Expression
1 1ex 1 V
2 1 elintab 1 x | 1 x y x y + 1 x x 1 x y x y + 1 x 1 x
3 simpl 1 x y x y + 1 x 1 x
4 2 3 mpgbir 1 x | 1 x y x y + 1 x
5 oveq1 y = z y + 1 = z + 1
6 5 eleq1d y = z y + 1 x z + 1 x
7 6 rspccv y x y + 1 x z x z + 1 x
8 7 adantl 1 x y x y + 1 x z x z + 1 x
9 8 a2i 1 x y x y + 1 x z x 1 x y x y + 1 x z + 1 x
10 9 alimi x 1 x y x y + 1 x z x x 1 x y x y + 1 x z + 1 x
11 vex z V
12 11 elintab z x | 1 x y x y + 1 x x 1 x y x y + 1 x z x
13 ovex z + 1 V
14 13 elintab z + 1 x | 1 x y x y + 1 x x 1 x y x y + 1 x z + 1 x
15 10 12 14 3imtr4i z x | 1 x y x y + 1 x z + 1 x | 1 x y x y + 1 x
16 15 rgen z x | 1 x y x y + 1 x z + 1 x | 1 x y x y + 1 x
17 peano5nni 1 x | 1 x y x y + 1 x z x | 1 x y x y + 1 x z + 1 x | 1 x y x y + 1 x x | 1 x y x y + 1 x
18 4 16 17 mp2an x | 1 x y x y + 1 x
19 1nn 1
20 peano2nn y y + 1
21 20 rgen y y + 1
22 nnex V
23 eleq2 x = 1 x 1
24 eleq2 x = y + 1 x y + 1
25 24 raleqbi1dv x = y x y + 1 x y y + 1
26 23 25 anbi12d x = 1 x y x y + 1 x 1 y y + 1
27 22 26 elab x | 1 x y x y + 1 x 1 y y + 1
28 19 21 27 mpbir2an x | 1 x y x y + 1 x
29 intss1 x | 1 x y x y + 1 x x | 1 x y x y + 1 x
30 28 29 ax-mp x | 1 x y x y + 1 x
31 18 30 eqssi = x | 1 x y x y + 1 x