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		onsssuc	⊢ ( ( 𝑧 ∈ On ∧ 𝑥 ∈ On ) → ( 𝑧 ⊆ 𝑥 ↔ 𝑧 ∈ suc 𝑥 ) )
3		ontri1	⊢ ( ( 𝑧 ∈ On ∧ 𝑥 ∈ On ) → ( 𝑧 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝑧 ) )
4	2 3	bitr3d	⊢ ( ( 𝑧 ∈ On ∧ 𝑥 ∈ On ) → ( 𝑧 ∈ suc 𝑥 ↔ ¬ 𝑥 ∈ 𝑧 ) )
5	4	ancoms	⊢ ( ( 𝑥 ∈ On ∧ 𝑧 ∈ On ) → ( 𝑧 ∈ suc 𝑥 ↔ ¬ 𝑥 ∈ 𝑧 ) )
6		limeq	⊢ ( 𝑦 = 𝑧 → ( Lim 𝑦 ↔ Lim 𝑧 ) )
7	6	notbid	⊢ ( 𝑦 = 𝑧 → ( ¬ Lim 𝑦 ↔ ¬ Lim 𝑧 ) )
8	7	elrab	⊢ ( 𝑧 ∈ { 𝑦 ∈ On ∣ ¬ Lim 𝑦 } ↔ ( 𝑧 ∈ On ∧ ¬ Lim 𝑧 ) )
9	8	a1i	⊢ ( ( 𝑥 ∈ On ∧ 𝑧 ∈ On ) → ( 𝑧 ∈ { 𝑦 ∈ On ∣ ¬ Lim 𝑦 } ↔ ( 𝑧 ∈ On ∧ ¬ Lim 𝑧 ) ) )
10	5 9	imbi12d	⊢ ( ( 𝑥 ∈ On ∧ 𝑧 ∈ On ) → ( ( 𝑧 ∈ suc 𝑥 → 𝑧 ∈ { 𝑦 ∈ On ∣ ¬ Lim 𝑦 } ) ↔ ( ¬ 𝑥 ∈ 𝑧 → ( 𝑧 ∈ On ∧ ¬ Lim 𝑧 ) ) ) )
11	10	pm5.74da	⊢ ( 𝑥 ∈ On → ( ( 𝑧 ∈ On → ( 𝑧 ∈ suc 𝑥 → 𝑧 ∈ { 𝑦 ∈ On ∣ ¬ Lim 𝑦 } ) ) ↔ ( 𝑧 ∈ On → ( ¬ 𝑥 ∈ 𝑧 → ( 𝑧 ∈ On ∧ ¬ Lim 𝑧 ) ) ) ) )
12		vex	⊢ 𝑧 ∈ V
13		limelon	⊢ ( ( 𝑧 ∈ V ∧ Lim 𝑧 ) → 𝑧 ∈ On )
14	12 13	mpan	⊢ ( Lim 𝑧 → 𝑧 ∈ On )
15	14	pm4.71ri	⊢ ( Lim 𝑧 ↔ ( 𝑧 ∈ On ∧ Lim 𝑧 ) )
16	15	imbi1i	⊢ ( ( Lim 𝑧 → 𝑥 ∈ 𝑧 ) ↔ ( ( 𝑧 ∈ On ∧ Lim 𝑧 ) → 𝑥 ∈ 𝑧 ) )
17		impexp	⊢ ( ( ( 𝑧 ∈ On ∧ Lim 𝑧 ) → 𝑥 ∈ 𝑧 ) ↔ ( 𝑧 ∈ On → ( Lim 𝑧 → 𝑥 ∈ 𝑧 ) ) )
18		con34b	⊢ ( ( Lim 𝑧 → 𝑥 ∈ 𝑧 ) ↔ ( ¬ 𝑥 ∈ 𝑧 → ¬ Lim 𝑧 ) )
19		ibar	⊢ ( 𝑧 ∈ On → ( ¬ Lim 𝑧 ↔ ( 𝑧 ∈ On ∧ ¬ Lim 𝑧 ) ) )
20	19	imbi2d	⊢ ( 𝑧 ∈ On → ( ( ¬ 𝑥 ∈ 𝑧 → ¬ Lim 𝑧 ) ↔ ( ¬ 𝑥 ∈ 𝑧 → ( 𝑧 ∈ On ∧ ¬ Lim 𝑧 ) ) ) )
21	18 20	syl5bb	⊢ ( 𝑧 ∈ On → ( ( Lim 𝑧 → 𝑥 ∈ 𝑧 ) ↔ ( ¬ 𝑥 ∈ 𝑧 → ( 𝑧 ∈ On ∧ ¬ Lim 𝑧 ) ) ) )
22	21	pm5.74i	⊢ ( ( 𝑧 ∈ On → ( Lim 𝑧 → 𝑥 ∈ 𝑧 ) ) ↔ ( 𝑧 ∈ On → ( ¬ 𝑥 ∈ 𝑧 → ( 𝑧 ∈ On ∧ ¬ Lim 𝑧 ) ) ) )
23	16 17 22	3bitri	⊢ ( ( Lim 𝑧 → 𝑥 ∈ 𝑧 ) ↔ ( 𝑧 ∈ On → ( ¬ 𝑥 ∈ 𝑧 → ( 𝑧 ∈ On ∧ ¬ Lim 𝑧 ) ) ) )
24	11 23	syl6rbbr	⊢ ( 𝑥 ∈ 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	syl6bbr	⊢ ( 𝑥 ∈ On → ( ∀ 𝑧 ( Lim 𝑧 → 𝑥 ∈ 𝑧 ) ↔ suc 𝑥 ⊆ { 𝑦 ∈ On ∣ ¬ Lim 𝑦 } ) )
39	38	rabbiia	⊢ { 𝑥 ∈ On ∣ ∀ 𝑧 ( Lim 𝑧 → 𝑥 ∈ 𝑧 ) } = { 𝑥 ∈ On ∣ suc 𝑥 ⊆ { 𝑦 ∈ On ∣ ¬ Lim 𝑦 } }
40	1 39	eqtri	⊢ ω = { 𝑥 ∈ On ∣ suc 𝑥 ⊆ { 𝑦 ∈ On ∣ ¬ Lim 𝑦 } }