HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem dfom3 4602
Description: The class of natural numbers omega can be defined as the smallest "inductive set," which is valid provided we assume the Axiom of Infinity. Definition 6.3 of [Eisenberg] p. 82.
Assertion
Ref Expression
dfom3 |- om = |^|{x | ((/) e. x /\ A.y e. x suc y e. x)}
Distinct variable group:   x,y
Proof of Theorem dfom3
StepHypRef Expression
1 0ex 2701 . . . . 5 |- (/) e. V
21elintab 2534 . . . 4 |- ((/) 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 pm3.26 319 . . . 4 |- (((/) e. x /\ A.y e. x suc y e. x) -> (/) e. x)
42, 3mpgbir 985 . . 3 |- (/) e. |^|{x | ((/) e. x /\ A.y e. x suc y e. x)}
5 suceq 3024 . . . . . . . . . . 11 |- (y = z -> suc y = suc z)
65eleq1d 1532 . . . . . . . . . 10 |- (y = z -> (suc y e. x <-> suc z e. x))
76rcla4cv 1865 . . . . . . . . 9 |- (A.y e. x suc y e. x -> (z e. x -> suc z e. x))
87adantl 388 . . . . . . . 8 |- (((/) e. x /\ A.y e. x suc y e. x) -> (z e. x -> suc z e. x))
98a2i 9 . . . . . . 7 |- ((((/) 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))
10919.20i 989 . . . . . 6 |- (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 visset 1804 . . . . . . 7 |- z e. V
1211elintab 2534 . . . . . 6 |- (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))
1311sucex 3040 . . . . . . 7 |- suc z e. V
1413elintab 2534 . . . . . 6 |- (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))
1510, 12, 143imtr4 219 . . . . 5 |- (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)})
1615a1i 8 . . . 4 |- (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)}))
1716rgen 1690 . . 3 |- 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)})
18 peano5 3143 . . 3 |- (((/) 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 (_ |^|{x | ((/) e. x /\ A.y e. x suc y e. x)})
194, 17, 18mp2an 695 . 2 |- om (_ |^|{x | ((/) e. x /\ A.y e. x suc y e. x)}
20 peano1 3139 . . . 4 |- (/) e. om
21 peano2 3140 . . . . 5 |- (y e. om -> suc y e. om)
2221rgen 1690 . . . 4 |- A.y e. om suc y e. om
23 omex 4599 . . . . . 6 |- om e. V
24 eleq2 1527 . . . . . . . 8 |- (x = om -> ((/) e. x <-> (/) e. om))
25 eleq2 1527 . . . . . . . . 9 |- (x = om -> (suc y e. x <-> suc y e. om))
2625raleqd 1783 . . . . . . . 8 |- (x = om -> (A.y e. x suc y e. x <-> A.y e. om suc y e. om))
2724, 26anbi12d 626 . . . . . . 7 |- (x = om -> (((/) e. x /\ A.y e. x suc y e. x) <-> ((/) e. om /\ A.y e. om suc y e. om)))
28 eleq2 1527 . . . . . . 7 |- (x = om -> (z e. x <-> z e. om))
2927, 28imbi12d 624 . . . . . 6 |- (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)))
3023, 29cla4v 1859 . . . . 5 |- (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))
3112, 30sylbi 199 . . . 4 |- (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))
3220, 22, 31mp2ani 698 . . 3 |- (z e. |^|{x | ((/) e. x /\ A.y e. x suc y e. x)} -> z e. om)
3332ssriv 2059 . 2 |- |^|{x | ((/) e. x /\ A.y e. x suc y e. x)} (_ om
3419, 33eqssi 2068 1 |- om = |^|{x | ((/) e. x /\ A.y e. x suc y e. x)}
Colors of variables: wff set class
Syntax hints:   -> wi 3   /\ wa 223  A.wal 951   = wceq 953   e. wcel 955  {cab 1456  A.wral 1637   (_ wss 2037  (/)c0 2270  |^|cint 2523  suc csuc 2940  omcom 3121
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-nul 2700  ax-pow 2732  ax-pr 2769  ax-un 2857  ax-inf2 4597
This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 774  df-3an 775  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-ral 1641  df-rex 1642  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-if 2352  df-pw 2392  df-sn 2402  df-pr 2403  df-tp 2405  df-op 2406  df-uni 2494  df-int 2524  df-br 2610  df-opab 2657  df-tr 2671  df-eprel 2821  df-po 2831  df-so 2841  df-fr 2907  df-we 2924  df-ord 2941  df-on 2942  df-lim 2943  df-suc 2944  df-om 3122
Copyright terms: Public domain