MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssnlim Structured version   Visualization version   GIF version

Theorem ssnlim 7726
Description: An ordinal subclass of non-limit ordinals is a class of natural numbers. Exercise 7 of [TakeutiZaring] p. 42. (Contributed by NM, 2-Nov-2004.)
Assertion
Ref Expression
ssnlim ((Ord 𝐴𝐴 ⊆ {𝑥 ∈ On ∣ ¬ Lim 𝑥}) → 𝐴 ⊆ ω)
Distinct variable group:   𝑥,𝐴

Proof of Theorem ssnlim
StepHypRef Expression
1 limom 7722 . . . 4 Lim ω
2 ssel 3919 . . . . 5 (𝐴 ⊆ {𝑥 ∈ On ∣ ¬ Lim 𝑥} → (ω ∈ 𝐴 → ω ∈ {𝑥 ∈ On ∣ ¬ Lim 𝑥}))
3 limeq 6277 . . . . . . . 8 (𝑥 = ω → (Lim 𝑥 ↔ Lim ω))
43notbid 318 . . . . . . 7 (𝑥 = ω → (¬ Lim 𝑥 ↔ ¬ Lim ω))
54elrab 3626 . . . . . 6 (ω ∈ {𝑥 ∈ On ∣ ¬ Lim 𝑥} ↔ (ω ∈ On ∧ ¬ Lim ω))
65simprbi 497 . . . . 5 (ω ∈ {𝑥 ∈ On ∣ ¬ Lim 𝑥} → ¬ Lim ω)
72, 6syl6 35 . . . 4 (𝐴 ⊆ {𝑥 ∈ On ∣ ¬ Lim 𝑥} → (ω ∈ 𝐴 → ¬ Lim ω))
81, 7mt2i 137 . . 3 (𝐴 ⊆ {𝑥 ∈ On ∣ ¬ Lim 𝑥} → ¬ ω ∈ 𝐴)
98adantl 482 . 2 ((Ord 𝐴𝐴 ⊆ {𝑥 ∈ On ∣ ¬ Lim 𝑥}) → ¬ ω ∈ 𝐴)
10 ordom 7716 . . . 4 Ord ω
11 ordtri1 6298 . . . 4 ((Ord 𝐴 ∧ Ord ω) → (𝐴 ⊆ ω ↔ ¬ ω ∈ 𝐴))
1210, 11mpan2 688 . . 3 (Ord 𝐴 → (𝐴 ⊆ ω ↔ ¬ ω ∈ 𝐴))
1312adantr 481 . 2 ((Ord 𝐴𝐴 ⊆ {𝑥 ∈ On ∣ ¬ Lim 𝑥}) → (𝐴 ⊆ ω ↔ ¬ ω ∈ 𝐴))
149, 13mpbird 256 1 ((Ord 𝐴𝐴 ⊆ {𝑥 ∈ On ∣ ¬ Lim 𝑥}) → 𝐴 ⊆ ω)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1542  wcel 2110  {crab 3070  wss 3892  Ord word 6264  Oncon0 6265  Lim wlim 6266  ωcom 7706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-11 2158  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356  ax-un 7582
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-ne 2946  df-ral 3071  df-rex 3072  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-opab 5142  df-tr 5197  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-ord 6268  df-on 6269  df-lim 6270  df-suc 6271  df-om 7707
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator