Metamath Proof Explorer

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 ⊢ ω = x ∈ On | suc ⁡ x ⊆ y ∈ On | ¬ Lim ⁡ y

Proof

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