MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfom3 Structured version   Visualization version   GIF version

Theorem dfom3 8708
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. (Contributed by NM, 6-Aug-1994.)
Assertion
Ref Expression
dfom3 ω = {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)}
Distinct variable group:   𝑥,𝑦

Proof of Theorem dfom3
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 0ex 4924 . . . . 5 ∅ ∈ V
21elintab 4622 . . . 4 (∅ ∈ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)} ↔ ∀𝑥((∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥) → ∅ ∈ 𝑥))
3 simpl 468 . . . 4 ((∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥) → ∅ ∈ 𝑥)
42, 3mpgbir 1874 . . 3 ∅ ∈ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)}
5 suceq 5933 . . . . . . . . . 10 (𝑦 = 𝑧 → suc 𝑦 = suc 𝑧)
65eleq1d 2835 . . . . . . . . 9 (𝑦 = 𝑧 → (suc 𝑦𝑥 ↔ suc 𝑧𝑥))
76rspccv 3457 . . . . . . . 8 (∀𝑦𝑥 suc 𝑦𝑥 → (𝑧𝑥 → suc 𝑧𝑥))
87adantl 467 . . . . . . 7 ((∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥) → (𝑧𝑥 → suc 𝑧𝑥))
98a2i 14 . . . . . 6 (((∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥) → 𝑧𝑥) → ((∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥) → suc 𝑧𝑥))
109alimi 1887 . . . . 5 (∀𝑥((∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥) → 𝑧𝑥) → ∀𝑥((∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥) → suc 𝑧𝑥))
11 vex 3354 . . . . . 6 𝑧 ∈ V
1211elintab 4622 . . . . 5 (𝑧 {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)} ↔ ∀𝑥((∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥) → 𝑧𝑥))
1311sucex 7158 . . . . . 6 suc 𝑧 ∈ V
1413elintab 4622 . . . . 5 (suc 𝑧 {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)} ↔ ∀𝑥((∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥) → suc 𝑧𝑥))
1510, 12, 143imtr4i 281 . . . 4 (𝑧 {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)} → suc 𝑧 {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)})
1615rgenw 3073 . . 3 𝑧 ∈ ω (𝑧 {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)} → suc 𝑧 {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)})
17 peano5 7236 . . 3 ((∅ ∈ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)} ∧ ∀𝑧 ∈ ω (𝑧 {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)} → suc 𝑧 {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)})) → ω ⊆ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)})
184, 16, 17mp2an 672 . 2 ω ⊆ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)}
19 peano1 7232 . . . 4 ∅ ∈ ω
20 peano2 7233 . . . . 5 (𝑦 ∈ ω → suc 𝑦 ∈ ω)
2120rgen 3071 . . . 4 𝑦 ∈ ω suc 𝑦 ∈ ω
22 omex 8704 . . . . . 6 ω ∈ V
23 eleq2 2839 . . . . . . . 8 (𝑥 = ω → (∅ ∈ 𝑥 ↔ ∅ ∈ ω))
24 eleq2 2839 . . . . . . . . 9 (𝑥 = ω → (suc 𝑦𝑥 ↔ suc 𝑦 ∈ ω))
2524raleqbi1dv 3295 . . . . . . . 8 (𝑥 = ω → (∀𝑦𝑥 suc 𝑦𝑥 ↔ ∀𝑦 ∈ ω suc 𝑦 ∈ ω))
2623, 25anbi12d 616 . . . . . . 7 (𝑥 = ω → ((∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥) ↔ (∅ ∈ ω ∧ ∀𝑦 ∈ ω suc 𝑦 ∈ ω)))
27 eleq2 2839 . . . . . . 7 (𝑥 = ω → (𝑧𝑥𝑧 ∈ ω))
2826, 27imbi12d 333 . . . . . 6 (𝑥 = ω → (((∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥) → 𝑧𝑥) ↔ ((∅ ∈ ω ∧ ∀𝑦 ∈ ω suc 𝑦 ∈ ω) → 𝑧 ∈ ω)))
2922, 28spcv 3450 . . . . 5 (∀𝑥((∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥) → 𝑧𝑥) → ((∅ ∈ ω ∧ ∀𝑦 ∈ ω suc 𝑦 ∈ ω) → 𝑧 ∈ ω))
3012, 29sylbi 207 . . . 4 (𝑧 {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)} → ((∅ ∈ ω ∧ ∀𝑦 ∈ ω suc 𝑦 ∈ ω) → 𝑧 ∈ ω))
3119, 21, 30mp2ani 678 . . 3 (𝑧 {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)} → 𝑧 ∈ ω)
3231ssriv 3756 . 2 {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)} ⊆ ω
3318, 32eqssi 3768 1 ω = {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)}
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wal 1629   = wceq 1631  wcel 2145  {cab 2757  wral 3061  wss 3723  c0 4063   cint 4611  suc csuc 5868  ωcom 7212
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pr 5034  ax-un 7096  ax-inf2 8702
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-br 4787  df-opab 4847  df-tr 4887  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-om 7213
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator