This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ω = { 𝑥 ∈ 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 bitrid ⊢ ( 𝑧 ∈ 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 onsuc ⊢ ( 𝑥 ∈ 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 df-ss ⊢ ( 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 𝑦 } }