Theorem dfom2 7429

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

Assertion

Ref	Expression
dfom2	⊢ ω = {𝑥 ∈ On ∣ suc 𝑥 ⊆ {𝑦 ∈ On ∣ ¬ Lim 𝑦}}

Proof of Theorem dfom2

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-om 7428	. 2 ⊢ ω = {𝑥 ∈ On ∣ ∀𝑧(Lim 𝑧 → 𝑥 ∈ 𝑧)}
2		onsssuc 6145	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ On ∧ 𝑥 ∈ On) → (𝑧 ⊆ 𝑥 ↔ 𝑧 ∈ suc 𝑥))
3		ontri1 6092	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ On ∧ 𝑥 ∈ On) → (𝑧 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝑧))
4	2, 3	bitr3d 282	. . . . . . . . . 10 ⊢ ((𝑧 ∈ On ∧ 𝑥 ∈ On) → (𝑧 ∈ suc 𝑥 ↔ ¬ 𝑥 ∈ 𝑧))
5	4	ancoms 459	. . . . . . . . 9 ⊢ ((𝑥 ∈ On ∧ 𝑧 ∈ On) → (𝑧 ∈ suc 𝑥 ↔ ¬ 𝑥 ∈ 𝑧))
6		limeq 6070	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (Lim 𝑦 ↔ Lim 𝑧))
7	6	notbid 319	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → (¬ Lim 𝑦 ↔ ¬ Lim 𝑧))
8	7	elrab 3613	. . . . . . . . . 10 ⊢ (𝑧 ∈ {𝑦 ∈ On ∣ ¬ Lim 𝑦} ↔ (𝑧 ∈ On ∧ ¬ Lim 𝑧))
9	8	a1i 11	. . . . . . . . 9 ⊢ ((𝑥 ∈ On ∧ 𝑧 ∈ On) → (𝑧 ∈ {𝑦 ∈ On ∣ ¬ Lim 𝑦} ↔ (𝑧 ∈ On ∧ ¬ Lim 𝑧)))
10	5, 9	imbi12d 346	. . . . . . . 8 ⊢ ((𝑥 ∈ On ∧ 𝑧 ∈ On) → ((𝑧 ∈ suc 𝑥 → 𝑧 ∈ {𝑦 ∈ On ∣ ¬ Lim 𝑦}) ↔ (¬ 𝑥 ∈ 𝑧 → (𝑧 ∈ On ∧ ¬ Lim 𝑧))))
11	10	pm5.74da 800	. . . . . . 7 ⊢ (𝑥 ∈ On → ((𝑧 ∈ On → (𝑧 ∈ suc 𝑥 → 𝑧 ∈ {𝑦 ∈ On ∣ ¬ Lim 𝑦})) ↔ (𝑧 ∈ On → (¬ 𝑥 ∈ 𝑧 → (𝑧 ∈ On ∧ ¬ Lim 𝑧)))))
12		vex 3435	. . . . . . . . . . 11 ⊢ 𝑧 ∈ V
13		limelon 6121	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ V ∧ Lim 𝑧) → 𝑧 ∈ On)
14	12, 13	mpan 686	. . . . . . . . . 10 ⊢ (Lim 𝑧 → 𝑧 ∈ On)
15	14	pm4.71ri 561	. . . . . . . . 9 ⊢ (Lim 𝑧 ↔ (𝑧 ∈ On ∧ Lim 𝑧))
16	15	imbi1i 351	. . . . . . . 8 ⊢ ((Lim 𝑧 → 𝑥 ∈ 𝑧) ↔ ((𝑧 ∈ On ∧ Lim 𝑧) → 𝑥 ∈ 𝑧))
17		impexp 451	. . . . . . . 8 ⊢ (((𝑧 ∈ On ∧ Lim 𝑧) → 𝑥 ∈ 𝑧) ↔ (𝑧 ∈ On → (Lim 𝑧 → 𝑥 ∈ 𝑧)))
18		con34b 317	. . . . . . . . . 10 ⊢ ((Lim 𝑧 → 𝑥 ∈ 𝑧) ↔ (¬ 𝑥 ∈ 𝑧 → ¬ Lim 𝑧))
19		ibar 529	. . . . . . . . . . 11 ⊢ (𝑧 ∈ On → (¬ Lim 𝑧 ↔ (𝑧 ∈ On ∧ ¬ Lim 𝑧)))
20	19	imbi2d 342	. . . . . . . . . 10 ⊢ (𝑧 ∈ On → ((¬ 𝑥 ∈ 𝑧 → ¬ Lim 𝑧) ↔ (¬ 𝑥 ∈ 𝑧 → (𝑧 ∈ On ∧ ¬ Lim 𝑧))))
21	18, 20	syl5bb 284	. . . . . . . . 9 ⊢ (𝑧 ∈ On → ((Lim 𝑧 → 𝑥 ∈ 𝑧) ↔ (¬ 𝑥 ∈ 𝑧 → (𝑧 ∈ On ∧ ¬ Lim 𝑧))))
22	21	pm5.74i 272	. . . . . . . 8 ⊢ ((𝑧 ∈ On → (Lim 𝑧 → 𝑥 ∈ 𝑧)) ↔ (𝑧 ∈ On → (¬ 𝑥 ∈ 𝑧 → (𝑧 ∈ On ∧ ¬ Lim 𝑧))))
23	16, 17, 22	3bitri 298	. . . . . . 7 ⊢ ((Lim 𝑧 → 𝑥 ∈ 𝑧) ↔ (𝑧 ∈ On → (¬ 𝑥 ∈ 𝑧 → (𝑧 ∈ On ∧ ¬ Lim 𝑧))))
24	11, 23	syl6rbbr 291	. . . . . 6 ⊢ (𝑥 ∈ On → ((Lim 𝑧 → 𝑥 ∈ 𝑧) ↔ (𝑧 ∈ On → (𝑧 ∈ suc 𝑥 → 𝑧 ∈ {𝑦 ∈ On ∣ ¬ Lim 𝑦}))))
25		impexp 451	. . . . . . 7 ⊢ (((𝑧 ∈ On ∧ 𝑧 ∈ suc 𝑥) → 𝑧 ∈ {𝑦 ∈ On ∣ ¬ Lim 𝑦}) ↔ (𝑧 ∈ On → (𝑧 ∈ suc 𝑥 → 𝑧 ∈ {𝑦 ∈ On ∣ ¬ Lim 𝑦})))
26		simpr 485	. . . . . . . . 9 ⊢ ((𝑧 ∈ On ∧ 𝑧 ∈ suc 𝑥) → 𝑧 ∈ suc 𝑥)
27		suceloni 7375	. . . . . . . . . . 11 ⊢ (𝑥 ∈ On → suc 𝑥 ∈ On)
28		onelon 6083	. . . . . . . . . . . 12 ⊢ ((suc 𝑥 ∈ On ∧ 𝑧 ∈ suc 𝑥) → 𝑧 ∈ On)
29	28	ex 413	. . . . . . . . . . 11 ⊢ (suc 𝑥 ∈ On → (𝑧 ∈ suc 𝑥 → 𝑧 ∈ On))
30	27, 29	syl 17	. . . . . . . . . 10 ⊢ (𝑥 ∈ On → (𝑧 ∈ suc 𝑥 → 𝑧 ∈ On))
31	30	ancrd 552	. . . . . . . . 9 ⊢ (𝑥 ∈ On → (𝑧 ∈ suc 𝑥 → (𝑧 ∈ On ∧ 𝑧 ∈ suc 𝑥)))
32	26, 31	impbid2 227	. . . . . . . 8 ⊢ (𝑥 ∈ On → ((𝑧 ∈ On ∧ 𝑧 ∈ suc 𝑥) ↔ 𝑧 ∈ suc 𝑥))
33	32	imbi1d 343	. . . . . . 7 ⊢ (𝑥 ∈ On → (((𝑧 ∈ On ∧ 𝑧 ∈ suc 𝑥) → 𝑧 ∈ {𝑦 ∈ On ∣ ¬ Lim 𝑦}) ↔ (𝑧 ∈ suc 𝑥 → 𝑧 ∈ {𝑦 ∈ On ∣ ¬ Lim 𝑦})))
34	25, 33	syl5bbr 286	. . . . . 6 ⊢ (𝑥 ∈ On → ((𝑧 ∈ On → (𝑧 ∈ suc 𝑥 → 𝑧 ∈ {𝑦 ∈ On ∣ ¬ Lim 𝑦})) ↔ (𝑧 ∈ suc 𝑥 → 𝑧 ∈ {𝑦 ∈ On ∣ ¬ Lim 𝑦})))
35	24, 34	bitrd 280	. . . . 5 ⊢ (𝑥 ∈ On → ((Lim 𝑧 → 𝑥 ∈ 𝑧) ↔ (𝑧 ∈ suc 𝑥 → 𝑧 ∈ {𝑦 ∈ On ∣ ¬ Lim 𝑦})))
36	35	albidv 1896	. . . 4 ⊢ (𝑥 ∈ On → (∀𝑧(Lim 𝑧 → 𝑥 ∈ 𝑧) ↔ ∀𝑧(𝑧 ∈ suc 𝑥 → 𝑧 ∈ {𝑦 ∈ On ∣ ¬ Lim 𝑦})))
37		dfss2 3872	. . . 4 ⊢ (suc 𝑥 ⊆ {𝑦 ∈ On ∣ ¬ Lim 𝑦} ↔ ∀𝑧(𝑧 ∈ suc 𝑥 → 𝑧 ∈ {𝑦 ∈ On ∣ ¬ Lim 𝑦}))
38	36, 37	syl6bbr 290	. . 3 ⊢ (𝑥 ∈ On → (∀𝑧(Lim 𝑧 → 𝑥 ∈ 𝑧) ↔ suc 𝑥 ⊆ {𝑦 ∈ On ∣ ¬ Lim 𝑦}))
39	38	rabbiia 3415	. 2 ⊢ {𝑥 ∈ On ∣ ∀𝑧(Lim 𝑧 → 𝑥 ∈ 𝑧)} = {𝑥 ∈ On ∣ suc 𝑥 ⊆ {𝑦 ∈ On ∣ ¬ Lim 𝑦}}
40	1, 39	eqtri 2817	1 ⊢ ω = {𝑥 ∈ On ∣ suc 𝑥 ⊆ {𝑦 ∈ On ∣ ¬ Lim 𝑦}}

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396  ∀wal 1518   = wceq 1520   ∈ wcel 2079  {crab 3107  Vcvv 3432   ⊆ wss 3854  Oncon0 6058  Lim wlim 6059  suc csuc 6060  ωcom 7427

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-13 2342  ax-ext 2767  ax-sep 5088  ax-nul 5095  ax-pr 5214  ax-un 7310

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1079  df-3an 1080  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-mo 2574  df-eu 2610  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-ne 2983  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3434  df-sbc 3702  df-dif 3857  df-un 3859  df-in 3861  df-ss 3869  df-pss 3871  df-nul 4207  df-if 4376  df-sn 4467  df-pr 4469  df-tp 4471  df-op 4473  df-uni 4740  df-br 4957  df-opab 5019  df-tr 5058  df-eprel 5345  df-po 5354  df-so 5355  df-fr 5394  df-we 5396  df-ord 6061  df-on 6062  df-lim 6063  df-suc 6064  df-om 7428

This theorem is referenced by:  omsson  7431