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. Definition 1.20 of Schloeder p. 3. (Contributed by NM, 6-Aug-1994)

Ref Expression
Assertion dfom3 ⊢ω=⋂x|∅∈x∧∀y∈xsuc⁡y∈x

Proof

Step Hyp Ref Expression
1 0ex ⊢∅∈V
2 1 elintab ⊢∅∈⋂x|∅∈x∧∀y∈xsuc⁡y∈x↔∀x∅∈x∧∀y∈xsuc⁡y∈x→∅∈x
3 simpl ⊢∅∈x∧∀y∈xsuc⁡y∈x→∅∈x
4 2 3 mpgbir ⊢∅∈⋂x|∅∈x∧∀y∈xsuc⁡y∈x
5 suceq ⊢y=z→suc⁡y=suc⁡z
6 5 eleq1d ⊢y=z→suc⁡y∈x↔suc⁡z∈x
7 6 rspccv ⊢∀y∈xsuc⁡y∈x→z∈x→suc⁡z∈x
8 7 adantl ⊢∅∈x∧∀y∈xsuc⁡y∈x→z∈x→suc⁡z∈x
9 8 a2i ⊢∅∈x∧∀y∈xsuc⁡y∈x→z∈x→∅∈x∧∀y∈xsuc⁡y∈x→suc⁡z∈x
10 9 alimi ⊢∀x∅∈x∧∀y∈xsuc⁡y∈x→z∈x→∀x∅∈x∧∀y∈xsuc⁡y∈x→suc⁡z∈x
11 vex ⊢z∈V
12 11 elintab ⊢z∈⋂x|∅∈x∧∀y∈xsuc⁡y∈x↔∀x∅∈x∧∀y∈xsuc⁡y∈x→z∈x
13 11 sucex ⊢suc⁡z∈V
14 13 elintab ⊢suc⁡z∈⋂x|∅∈x∧∀y∈xsuc⁡y∈x↔∀x∅∈x∧∀y∈xsuc⁡y∈x→suc⁡z∈x
15 10 12 14 3imtr4i ⊢z∈⋂x|∅∈x∧∀y∈xsuc⁡y∈x→suc⁡z∈⋂x|∅∈x∧∀y∈xsuc⁡y∈x
16 15 rgenw ⊢∀z∈ωz∈⋂x|∅∈x∧∀y∈xsuc⁡y∈x→suc⁡z∈⋂x|∅∈x∧∀y∈xsuc⁡y∈x
17 peano5 ⊢∅∈⋂x|∅∈x∧∀y∈xsuc⁡y∈x∧∀z∈ωz∈⋂x|∅∈x∧∀y∈xsuc⁡y∈x→suc⁡z∈⋂x|∅∈x∧∀y∈xsuc⁡y∈x→ω⊆⋂x|∅∈x∧∀y∈xsuc⁡y∈x
18 4 16 17 mp2an ⊢ω⊆⋂x|∅∈x∧∀y∈xsuc⁡y∈x
19 peano1 ⊢∅∈ω
20 peano2 ⊢y∈ω→suc⁡y∈ω
21 20 rgen ⊢∀y∈ωsuc⁡y∈ω
22 omex ⊢ω∈V
23 eleq2 ⊢x=ω→∅∈x↔∅∈ω
24 eleq2 ⊢x=ω→suc⁡y∈x↔suc⁡y∈ω
25 24 raleqbi1dv ⊢x=ω→∀y∈xsuc⁡y∈x↔∀y∈ωsuc⁡y∈ω
26 23 25 anbi12d ⊢x=ω→∅∈x∧∀y∈xsuc⁡y∈x↔∅∈ω∧∀y∈ωsuc⁡y∈ω
27 eleq2 ⊢x=ω→z∈x↔z∈ω
28 26 27 imbi12d ⊢x=ω→∅∈x∧∀y∈xsuc⁡y∈x→z∈x↔∅∈ω∧∀y∈ωsuc⁡y∈ω→z∈ω
29 22 28 spcv ⊢∀x∅∈x∧∀y∈xsuc⁡y∈x→z∈x→∅∈ω∧∀y∈ωsuc⁡y∈ω→z∈ω
30 12 29 sylbi ⊢z∈⋂x|∅∈x∧∀y∈xsuc⁡y∈x→∅∈ω∧∀y∈ωsuc⁡y∈ω→z∈ω
31 19 21 30 mp2ani ⊢z∈⋂x|∅∈x∧∀y∈xsuc⁡y∈x→z∈ω
32 31 ssriv ⊢⋂x|∅∈x∧∀y∈xsuc⁡y∈x⊆ω
33 18 32 eqssi ⊢ω=⋂x|∅∈x∧∀y∈xsuc⁡y∈x