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 \| (\emptyset \in x \land \forall y \in x suc y \in x)\}$

Proof

Step	Hyp	Ref	Expression
1		0ex	$⊢ \emptyset \in V$
2	1	elintab	$⊢ \emptyset \in ⋂ \{x \| (\emptyset \in x \land \forall y \in x suc y \in x)\} \leftrightarrow \forall x ((\emptyset \in x \land \forall y \in x suc y \in x) \to \emptyset \in x)$
3		simpl	$⊢ (\emptyset \in x \land \forall y \in x suc y \in x) \to \emptyset \in x$
4	2 3	mpgbir	$⊢ \emptyset \in ⋂ \{x \| (\emptyset \in x \land \forall y \in x suc y \in x)\}$
5		suceq	$⊢ y = z \to suc y = suc z$
6	5	eleq1d	$⊢ y = z \to (suc y \in x \leftrightarrow suc z \in x)$
7	6	rspccv	$⊢ \forall y \in x suc y \in x \to (z \in x \to suc z \in x)$
8	7	adantl	$⊢ (\emptyset \in x \land \forall y \in x suc y \in x) \to (z \in x \to suc z \in x)$
9	8	a2i	$⊢ ((\emptyset \in x \land \forall y \in x suc y \in x) \to z \in x) \to ((\emptyset \in x \land \forall y \in x suc y \in x) \to suc z \in x)$
10	9	alimi	$⊢ \forall x ((\emptyset \in x \land \forall y \in x suc y \in x) \to z \in x) \to \forall x ((\emptyset \in x \land \forall y \in x suc y \in x) \to suc z \in x)$
11		vex	$⊢ z \in V$
12	11	elintab	$⊢ z \in ⋂ \{x \| (\emptyset \in x \land \forall y \in x suc y \in x)\} \leftrightarrow \forall x ((\emptyset \in x \land \forall y \in x suc y \in x) \to z \in x)$
13	11	sucex	$⊢ suc z \in V$
14	13	elintab	$⊢ suc z \in ⋂ \{x \| (\emptyset \in x \land \forall y \in x suc y \in x)\} \leftrightarrow \forall x ((\emptyset \in x \land \forall y \in x suc y \in x) \to suc z \in x)$
15	10 12 14	3imtr4i	$⊢ z \in ⋂ \{x \| (\emptyset \in x \land \forall y \in x suc y \in x)\} \to suc z \in ⋂ \{x \| (\emptyset \in x \land \forall y \in x suc y \in x)\}$
16	15	rgenw	$⊢ \forall z \in ω (z \in ⋂ \{x \| (\emptyset \in x \land \forall y \in x suc y \in x)\} \to suc z \in ⋂ \{x \| (\emptyset \in x \land \forall y \in x suc y \in x)\})$
17		peano5	$⊢ (\emptyset \in ⋂ \{x \| (\emptyset \in x \land \forall y \in x suc y \in x)\} \land \forall z \in ω (z \in ⋂ \{x \| (\emptyset \in x \land \forall y \in x suc y \in x)\} \to suc z \in ⋂ \{x \| (\emptyset \in x \land \forall y \in x suc y \in x)\})) \to ω \subseteq ⋂ \{x \| (\emptyset \in x \land \forall y \in x suc y \in x)\}$
18	4 16 17	mp2an	$⊢ ω \subseteq ⋂ \{x \| (\emptyset \in x \land \forall y \in x suc y \in x)\}$
19		peano1	$⊢ \emptyset \in ω$
20		peano2	$⊢ y \in ω \to suc y \in ω$
21	20	rgen	$⊢ \forall y \in ω suc y \in ω$
22		omex	$⊢ ω \in V$
23		eleq2	$⊢ x = ω \to (\emptyset \in x \leftrightarrow \emptyset \in ω)$
24		eleq2	$⊢ x = ω \to (suc y \in x \leftrightarrow suc y \in ω)$
25	24	raleqbi1dv	$⊢ x = ω \to (\forall y \in x suc y \in x \leftrightarrow \forall y \in ω suc y \in ω)$
26	23 25	anbi12d	$⊢ x = ω \to ((\emptyset \in x \land \forall y \in x suc y \in x) \leftrightarrow (\emptyset \in ω \land \forall y \in ω suc y \in ω))$
27		eleq2	$⊢ x = ω \to (z \in x \leftrightarrow z \in ω)$
28	26 27	imbi12d	$⊢ x = ω \to (((\emptyset \in x \land \forall y \in x suc y \in x) \to z \in x) \leftrightarrow ((\emptyset \in ω \land \forall y \in ω suc y \in ω) \to z \in ω))$
29	22 28	spcv	$⊢ \forall x ((\emptyset \in x \land \forall y \in x suc y \in x) \to z \in x) \to ((\emptyset \in ω \land \forall y \in ω suc y \in ω) \to z \in ω)$
30	12 29	sylbi	$⊢ z \in ⋂ \{x \| (\emptyset \in x \land \forall y \in x suc y \in x)\} \to ((\emptyset \in ω \land \forall y \in ω suc y \in ω) \to z \in ω)$
31	19 21 30	mp2ani	$⊢ z \in ⋂ \{x \| (\emptyset \in x \land \forall y \in x suc y \in x)\} \to z \in ω$
32	31	ssriv	$⊢ ⋂ \{x \| (\emptyset \in x \land \forall y \in x suc y \in x)\} \subseteq ω$
33	18 32	eqssi	$⊢ ω = ⋂ \{x \| (\emptyset \in x \land \forall y \in x suc y \in x)\}$

Metamath Proof Explorer

Theorem dfom3

Proof