dfom2

Description: An alternate definition of the set of natural numbers _om . Definition 7.28 of TakeutiZaring p. 42, who use the symbol K_I for the restricted class abstraction of non-limit ordinal numbers (see nlimon ). (Contributed by NM, 1-Nov-2004)

		Ref	Expression
	Assertion	dfom2	$⊢ ω = \{x \in On \| suc x \subseteq \{y \in On \| \neg Lim y\}\}$

Proof

Step	Hyp	Ref	Expression
1		df-om	$⊢ ω = \{x \in On \| \forall z (Lim z \to x \in z)\}$
2		vex	$⊢ z \in V$
3		limelon	$⊢ (z \in V \land Lim z) \to z \in On$
4	2 3	mpan	$⊢ Lim z \to z \in On$
5	4	pm4.71ri	$⊢ Lim z \leftrightarrow (z \in On \land Lim z)$
6	5	imbi1i	$⊢ (Lim z \to x \in z) \leftrightarrow ((z \in On \land Lim z) \to x \in z)$
7		impexp	$⊢ ((z \in On \land Lim z) \to x \in z) \leftrightarrow (z \in On \to (Lim z \to x \in z))$
8		con34b	$⊢ (Lim z \to x \in z) \leftrightarrow (\neg x \in z \to \neg Lim z)$
9		ibar	$⊢ z \in On \to (\neg Lim z \leftrightarrow (z \in On \land \neg Lim z))$
10	9	imbi2d	$⊢ z \in On \to ((\neg x \in z \to \neg Lim z) \leftrightarrow (\neg x \in z \to (z \in On \land \neg Lim z)))$
11	8 10	bitrid	$⊢ z \in On \to ((Lim z \to x \in z) \leftrightarrow (\neg x \in z \to (z \in On \land \neg Lim z)))$
12	11	pm5.74i	$⊢ (z \in On \to (Lim z \to x \in z)) \leftrightarrow (z \in On \to (\neg x \in z \to (z \in On \land \neg Lim z)))$
13	6 7 12	3bitri	$⊢ (Lim z \to x \in z) \leftrightarrow (z \in On \to (\neg x \in z \to (z \in On \land \neg Lim z)))$
14		onsssuc	$⊢ (z \in On \land x \in On) \to (z \subseteq x \leftrightarrow z \in suc x)$
15		ontri1	$⊢ (z \in On \land x \in On) \to (z \subseteq x \leftrightarrow \neg x \in z)$
16	14 15	bitr3d	$⊢ (z \in On \land x \in On) \to (z \in suc x \leftrightarrow \neg x \in z)$
17	16	ancoms	$⊢ (x \in On \land z \in On) \to (z \in suc x \leftrightarrow \neg x \in z)$
18		limeq	$⊢ y = z \to (Lim y \leftrightarrow Lim z)$
19	18	notbid	$⊢ y = z \to (\neg Lim y \leftrightarrow \neg Lim z)$
20	19	elrab	$⊢ z \in \{y \in On \| \neg Lim y\} \leftrightarrow (z \in On \land \neg Lim z)$
21	20	a1i	$⊢ (x \in On \land z \in On) \to (z \in \{y \in On \| \neg Lim y\} \leftrightarrow (z \in On \land \neg Lim z))$
22	17 21	imbi12d	$⊢ (x \in On \land z \in On) \to ((z \in suc x \to z \in \{y \in On \| \neg Lim y\}) \leftrightarrow (\neg x \in z \to (z \in On \land \neg Lim z)))$
23	22	pm5.74da	$⊢ x \in On \to ((z \in On \to (z \in suc x \to z \in \{y \in On \| \neg Lim y\})) \leftrightarrow (z \in On \to (\neg x \in z \to (z \in On \land \neg Lim z))))$
24	13 23	bitr4id	$⊢ x \in On \to ((Lim z \to x \in z) \leftrightarrow (z \in On \to (z \in suc x \to z \in \{y \in On \| \neg Lim y\})))$
25		impexp	$⊢ ((z \in On \land z \in suc x) \to z \in \{y \in On \| \neg Lim y\}) \leftrightarrow (z \in On \to (z \in suc x \to z \in \{y \in On \| \neg Lim y\}))$
26		simpr	$⊢ (z \in On \land z \in suc x) \to z \in suc x$
27		onsuc	$⊢ x \in On \to suc x \in On$
28		onelon	$⊢ (suc x \in On \land z \in suc x) \to z \in On$
29	28	ex	$⊢ suc x \in On \to (z \in suc x \to z \in On)$
30	27 29	syl	$⊢ x \in On \to (z \in suc x \to z \in On)$
31	30	ancrd	$⊢ x \in On \to (z \in suc x \to (z \in On \land z \in suc x))$
32	26 31	impbid2	$⊢ x \in On \to ((z \in On \land z \in suc x) \leftrightarrow z \in suc x)$
33	32	imbi1d	$⊢ x \in On \to (((z \in On \land z \in suc x) \to z \in \{y \in On \| \neg Lim y\}) \leftrightarrow (z \in suc x \to z \in \{y \in On \| \neg Lim y\}))$
34	25 33	bitr3id	$⊢ x \in On \to ((z \in On \to (z \in suc x \to z \in \{y \in On \| \neg Lim y\})) \leftrightarrow (z \in suc x \to z \in \{y \in On \| \neg Lim y\}))$
35	24 34	bitrd	$⊢ x \in On \to ((Lim z \to x \in z) \leftrightarrow (z \in suc x \to z \in \{y \in On \| \neg Lim y\}))$
36	35	albidv	$⊢ x \in On \to (\forall z (Lim z \to x \in z) \leftrightarrow \forall z (z \in suc x \to z \in \{y \in On \| \neg Lim y\}))$
37		dfss2	$⊢ suc x \subseteq \{y \in On \| \neg Lim y\} \leftrightarrow \forall z (z \in suc x \to z \in \{y \in On \| \neg Lim y\})$
38	36 37	bitr4di	$⊢ x \in On \to (\forall z (Lim z \to x \in z) \leftrightarrow suc x \subseteq \{y \in On \| \neg Lim y\})$
39	38	rabbiia	$⊢ \{x \in On \| \forall z (Lim z \to x \in z)\} = \{x \in On \| suc x \subseteq \{y \in On \| \neg Lim y\}\}$
40	1 39	eqtri	$⊢ ω = \{x \in On \| suc x \subseteq \{y \in On \| \neg Lim y\}\}$

Metamath Proof Explorer

Theorem dfom2

Proof