Theorem 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	⊢ ω = { 𝑥 ∈ On ∣ suc 𝑥 ⊆ { 𝑦 ∈ On ∣ ¬ Lim 𝑦 } }

Proof

Step	Hyp	Ref	Expression
1		df-om	⊢ ω = { 𝑥 ∈ On ∣ ∀ 𝑧 ( Lim 𝑧 → 𝑥 ∈ 𝑧 ) }
2		vex	⊢ 𝑧 ∈ V
3		limelon	⊢ ( ( 𝑧 ∈ V ∧ Lim 𝑧 ) → 𝑧 ∈ On )
4	2 3	mpan	⊢ ( Lim 𝑧 → 𝑧 ∈ On )
5	4	pm4.71ri	⊢ ( Lim 𝑧 ↔ ( 𝑧 ∈ On ∧ Lim 𝑧 ) )
6	5	imbi1i	⊢ ( ( Lim 𝑧 → 𝑥 ∈ 𝑧 ) ↔ ( ( 𝑧 ∈ On ∧ Lim 𝑧 ) → 𝑥 ∈ 𝑧 ) )
7		impexp	⊢ ( ( ( 𝑧 ∈ On ∧ Lim 𝑧 ) → 𝑥 ∈ 𝑧 ) ↔ ( 𝑧 ∈ On → ( Lim 𝑧 → 𝑥 ∈ 𝑧 ) ) )
8		con34b	⊢ ( ( Lim 𝑧 → 𝑥 ∈ 𝑧 ) ↔ ( ¬ 𝑥 ∈ 𝑧 → ¬ Lim 𝑧 ) )
9		ibar	⊢ ( 𝑧 ∈ On → ( ¬ Lim 𝑧 ↔ ( 𝑧 ∈ On ∧ ¬ Lim 𝑧 ) ) )
10	9	imbi2d	⊢ ( 𝑧 ∈ On → ( ( ¬ 𝑥 ∈ 𝑧 → ¬ Lim 𝑧 ) ↔ ( ¬ 𝑥 ∈ 𝑧 → ( 𝑧 ∈ On ∧ ¬ Lim 𝑧 ) ) ) )
11	8 10	syl5bb	⊢ ( 𝑧 ∈ On → ( ( Lim 𝑧 → 𝑥 ∈ 𝑧 ) ↔ ( ¬ 𝑥 ∈ 𝑧 → ( 𝑧 ∈ On ∧ ¬ Lim 𝑧 ) ) ) )
12	11	pm5.74i	⊢ ( ( 𝑧 ∈ On → ( Lim 𝑧 → 𝑥 ∈ 𝑧 ) ) ↔ ( 𝑧 ∈ On → ( ¬ 𝑥 ∈ 𝑧 → ( 𝑧 ∈ On ∧ ¬ Lim 𝑧 ) ) ) )
13	6 7 12	3bitri	⊢ ( ( Lim 𝑧 → 𝑥 ∈ 𝑧 ) ↔ ( 𝑧 ∈ On → ( ¬ 𝑥 ∈ 𝑧 → ( 𝑧 ∈ On ∧ ¬ Lim 𝑧 ) ) ) )
14		onsssuc	⊢ ( ( 𝑧 ∈ On ∧ 𝑥 ∈ On ) → ( 𝑧 ⊆ 𝑥 ↔ 𝑧 ∈ suc 𝑥 ) )
15		ontri1	⊢ ( ( 𝑧 ∈ On ∧ 𝑥 ∈ On ) → ( 𝑧 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝑧 ) )
16	14 15	bitr3d	⊢ ( ( 𝑧 ∈ On ∧ 𝑥 ∈ On ) → ( 𝑧 ∈ suc 𝑥 ↔ ¬ 𝑥 ∈ 𝑧 ) )
17	16	ancoms	⊢ ( ( 𝑥 ∈ On ∧ 𝑧 ∈ On ) → ( 𝑧 ∈ suc 𝑥 ↔ ¬ 𝑥 ∈ 𝑧 ) )
18		limeq	⊢ ( 𝑦 = 𝑧 → ( Lim 𝑦 ↔ Lim 𝑧 ) )
19	18	notbid	⊢ ( 𝑦 = 𝑧 → ( ¬ Lim 𝑦 ↔ ¬ Lim 𝑧 ) )
20	19	elrab	⊢ ( 𝑧 ∈ { 𝑦 ∈ On ∣ ¬ Lim 𝑦 } ↔ ( 𝑧 ∈ On ∧ ¬ Lim 𝑧 ) )
21	20	a1i	⊢ ( ( 𝑥 ∈ On ∧ 𝑧 ∈ On ) → ( 𝑧 ∈ { 𝑦 ∈ On ∣ ¬ Lim 𝑦 } ↔ ( 𝑧 ∈ On ∧ ¬ Lim 𝑧 ) ) )
22	17 21	imbi12d	⊢ ( ( 𝑥 ∈ On ∧ 𝑧 ∈ On ) → ( ( 𝑧 ∈ suc 𝑥 → 𝑧 ∈ { 𝑦 ∈ On ∣ ¬ Lim 𝑦 } ) ↔ ( ¬ 𝑥 ∈ 𝑧 → ( 𝑧 ∈ On ∧ ¬ Lim 𝑧 ) ) ) )
23	22	pm5.74da	⊢ ( 𝑥 ∈ On → ( ( 𝑧 ∈ On → ( 𝑧 ∈ suc 𝑥 → 𝑧 ∈ { 𝑦 ∈ On ∣ ¬ Lim 𝑦 } ) ) ↔ ( 𝑧 ∈ On → ( ¬ 𝑥 ∈ 𝑧 → ( 𝑧 ∈ On ∧ ¬ Lim 𝑧 ) ) ) ) )
24	13 23	bitr4id	⊢ ( 𝑥 ∈ On → ( ( Lim 𝑧 → 𝑥 ∈ 𝑧 ) ↔ ( 𝑧 ∈ On → ( 𝑧 ∈ suc 𝑥 → 𝑧 ∈ { 𝑦 ∈ On ∣ ¬ Lim 𝑦 } ) ) ) )
25		impexp	⊢ ( ( ( 𝑧 ∈ On ∧ 𝑧 ∈ suc 𝑥 ) → 𝑧 ∈ { 𝑦 ∈ On ∣ ¬ Lim 𝑦 } ) ↔ ( 𝑧 ∈ On → ( 𝑧 ∈ suc 𝑥 → 𝑧 ∈ { 𝑦 ∈ On ∣ ¬ Lim 𝑦 } ) ) )
26		simpr	⊢ ( ( 𝑧 ∈ On ∧ 𝑧 ∈ suc 𝑥 ) → 𝑧 ∈ suc 𝑥 )
27		suceloni	⊢ ( 𝑥 ∈ On → suc 𝑥 ∈ On )
28		onelon	⊢ ( ( suc 𝑥 ∈ On ∧ 𝑧 ∈ suc 𝑥 ) → 𝑧 ∈ On )
29	28	ex	⊢ ( suc 𝑥 ∈ On → ( 𝑧 ∈ suc 𝑥 → 𝑧 ∈ On ) )
30	27 29	syl	⊢ ( 𝑥 ∈ On → ( 𝑧 ∈ suc 𝑥 → 𝑧 ∈ On ) )
31	30	ancrd	⊢ ( 𝑥 ∈ On → ( 𝑧 ∈ suc 𝑥 → ( 𝑧 ∈ On ∧ 𝑧 ∈ suc 𝑥 ) ) )
32	26 31	impbid2	⊢ ( 𝑥 ∈ On → ( ( 𝑧 ∈ On ∧ 𝑧 ∈ suc 𝑥 ) ↔ 𝑧 ∈ suc 𝑥 ) )
33	32	imbi1d	⊢ ( 𝑥 ∈ On → ( ( ( 𝑧 ∈ On ∧ 𝑧 ∈ suc 𝑥 ) → 𝑧 ∈ { 𝑦 ∈ On ∣ ¬ Lim 𝑦 } ) ↔ ( 𝑧 ∈ suc 𝑥 → 𝑧 ∈ { 𝑦 ∈ On ∣ ¬ Lim 𝑦 } ) ) )
34	25 33	bitr3id	⊢ ( 𝑥 ∈ On → ( ( 𝑧 ∈ On → ( 𝑧 ∈ suc 𝑥 → 𝑧 ∈ { 𝑦 ∈ On ∣ ¬ Lim 𝑦 } ) ) ↔ ( 𝑧 ∈ suc 𝑥 → 𝑧 ∈ { 𝑦 ∈ On ∣ ¬ Lim 𝑦 } ) ) )
35	24 34	bitrd	⊢ ( 𝑥 ∈ On → ( ( Lim 𝑧 → 𝑥 ∈ 𝑧 ) ↔ ( 𝑧 ∈ suc 𝑥 → 𝑧 ∈ { 𝑦 ∈ On ∣ ¬ Lim 𝑦 } ) ) )
36	35	albidv	⊢ ( 𝑥 ∈ On → ( ∀ 𝑧 ( Lim 𝑧 → 𝑥 ∈ 𝑧 ) ↔ ∀ 𝑧 ( 𝑧 ∈ suc 𝑥 → 𝑧 ∈ { 𝑦 ∈ On ∣ ¬ Lim 𝑦 } ) ) )
37		dfss2	⊢ ( suc 𝑥 ⊆ { 𝑦 ∈ On ∣ ¬ Lim 𝑦 } ↔ ∀ 𝑧 ( 𝑧 ∈ suc 𝑥 → 𝑧 ∈ { 𝑦 ∈ On ∣ ¬ Lim 𝑦 } ) )
38	36 37	bitr4di	⊢ ( 𝑥 ∈ On → ( ∀ 𝑧 ( Lim 𝑧 → 𝑥 ∈ 𝑧 ) ↔ suc 𝑥 ⊆ { 𝑦 ∈ On ∣ ¬ Lim 𝑦 } ) )
39	38	rabbiia	⊢ { 𝑥 ∈ On ∣ ∀ 𝑧 ( Lim 𝑧 → 𝑥 ∈ 𝑧 ) } = { 𝑥 ∈ On ∣ suc 𝑥 ⊆ { 𝑦 ∈ On ∣ ¬ Lim 𝑦 } }
40	1 39	eqtri	⊢ ω = { 𝑥 ∈ On ∣ suc 𝑥 ⊆ { 𝑦 ∈ On ∣ ¬ Lim 𝑦 } }