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 vex ⊢ z ∈ V
3 limelon ⊢ z ∈ V ∧ Lim ⁡ z → z ∈ On
4 2 3 mpan ⊢ Lim ⁡ z → z ∈ On
5 4 pm4.71ri ⊢ Lim ⁡ z ↔ z ∈ On ∧ Lim ⁡ z
6 5 imbi1i ⊢ Lim ⁡ z → x ∈ z ↔ z ∈ On ∧ Lim ⁡ z → x ∈ z
7 impexp ⊢ z ∈ On ∧ Lim ⁡ z → x ∈ z ↔ z ∈ On → Lim ⁡ z → x ∈ z
8 con34b ⊢ Lim ⁡ z → x ∈ z ↔ ¬ x ∈ z → ¬ Lim ⁡ z
9 ibar ⊢ z ∈ On → ¬ Lim ⁡ z ↔ z ∈ On ∧ ¬ Lim ⁡ z
10 9 imbi2d ⊢ z ∈ On → ¬ x ∈ z → ¬ Lim ⁡ z ↔ ¬ x ∈ z → z ∈ On ∧ ¬ Lim ⁡ z
11 8 10 bitrid ⊢ z ∈ On → Lim ⁡ z → x ∈ z ↔ ¬ x ∈ z → z ∈ On ∧ ¬ Lim ⁡ z
12 11 pm5.74i ⊢ z ∈ On → Lim ⁡ z → x ∈ z ↔ z ∈ On → ¬ x ∈ z → z ∈ On ∧ ¬ Lim ⁡ z
13 6 7 12 3bitri ⊢ Lim ⁡ z → x ∈ z ↔ z ∈ On → ¬ x ∈ z → z ∈ On ∧ ¬ Lim ⁡ z
14 onsssuc ⊢ z ∈ On ∧ x ∈ On → z ⊆ x ↔ z ∈ suc ⁡ x
15 ontri1 ⊢ z ∈ On ∧ x ∈ On → z ⊆ x ↔ ¬ x ∈ z
16 14 15 bitr3d ⊢ z ∈ On ∧ x ∈ On → z ∈ suc ⁡ x ↔ ¬ x ∈ z
17 16 ancoms ⊢ x ∈ On ∧ z ∈ On → z ∈ suc ⁡ x ↔ ¬ x ∈ z
18 limeq ⊢ y = z → Lim ⁡ y ↔ Lim ⁡ z
19 18 notbid ⊢ y = z → ¬ Lim ⁡ y ↔ ¬ Lim ⁡ z
20 19 elrab ⊢ z ∈ y ∈ On | ¬ Lim ⁡ y ↔ z ∈ On ∧ ¬ Lim ⁡ z
21 20 a1i ⊢ x ∈ On ∧ z ∈ On → z ∈ y ∈ On | ¬ Lim ⁡ y ↔ z ∈ On ∧ ¬ Lim ⁡ z
22 17 21 imbi12d ⊢ x ∈ On ∧ z ∈ On → z ∈ suc ⁡ x → z ∈ y ∈ On | ¬ Lim ⁡ y ↔ ¬ x ∈ z → z ∈ On ∧ ¬ Lim ⁡ z
23 22 pm5.74da ⊢ x ∈ On → z ∈ On → z ∈ suc ⁡ x → z ∈ y ∈ On | ¬ Lim ⁡ y ↔ z ∈ On → ¬ x ∈ z → z ∈ On ∧ ¬ Lim ⁡ z
24 13 23 bitr4id ⊢ 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 bitr4di ⊢ 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