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

Theorem noreson 27723
Description: The restriction of a surreal to an ordinal is still a surreal. (Contributed by Scott Fenton, 4-Sep-2011.)
Assertion
Ref Expression
noreson ((𝐴 No 𝐵 ∈ On) → (𝐴𝐵) ∈ No )

Proof of Theorem noreson
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elno 27708 . . 3 (𝐴 No ↔ ∃𝑥 ∈ On 𝐴:𝑥⟶{1o, 2o})
2 onin 6426 . . . . . . . 8 ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑥𝐵) ∈ On)
3 fresin 6790 . . . . . . . 8 (𝐴:𝑥⟶{1o, 2o} → (𝐴𝐵):(𝑥𝐵)⟶{1o, 2o})
4 feq2 6729 . . . . . . . . 9 (𝑦 = (𝑥𝐵) → ((𝐴𝐵):𝑦⟶{1o, 2o} ↔ (𝐴𝐵):(𝑥𝐵)⟶{1o, 2o}))
54rspcev 3635 . . . . . . . 8 (((𝑥𝐵) ∈ On ∧ (𝐴𝐵):(𝑥𝐵)⟶{1o, 2o}) → ∃𝑦 ∈ On (𝐴𝐵):𝑦⟶{1o, 2o})
62, 3, 5syl2an 595 . . . . . . 7 (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴:𝑥⟶{1o, 2o}) → ∃𝑦 ∈ On (𝐴𝐵):𝑦⟶{1o, 2o})
76an32s 651 . . . . . 6 (((𝑥 ∈ On ∧ 𝐴:𝑥⟶{1o, 2o}) ∧ 𝐵 ∈ On) → ∃𝑦 ∈ On (𝐴𝐵):𝑦⟶{1o, 2o})
87ex 412 . . . . 5 ((𝑥 ∈ On ∧ 𝐴:𝑥⟶{1o, 2o}) → (𝐵 ∈ On → ∃𝑦 ∈ On (𝐴𝐵):𝑦⟶{1o, 2o}))
98rexlimiva 3153 . . . 4 (∃𝑥 ∈ On 𝐴:𝑥⟶{1o, 2o} → (𝐵 ∈ On → ∃𝑦 ∈ On (𝐴𝐵):𝑦⟶{1o, 2o}))
109imp 406 . . 3 ((∃𝑥 ∈ On 𝐴:𝑥⟶{1o, 2o} ∧ 𝐵 ∈ On) → ∃𝑦 ∈ On (𝐴𝐵):𝑦⟶{1o, 2o})
111, 10sylanb 580 . 2 ((𝐴 No 𝐵 ∈ On) → ∃𝑦 ∈ On (𝐴𝐵):𝑦⟶{1o, 2o})
12 elno 27708 . 2 ((𝐴𝐵) ∈ No ↔ ∃𝑦 ∈ On (𝐴𝐵):𝑦⟶{1o, 2o})
1311, 12sylibr 234 1 ((𝐴 No 𝐵 ∈ On) → (𝐴𝐵) ∈ No )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wcel 2108  wrex 3076  cin 3975  {cpr 4650  cres 5702  Oncon0 6395  wf 6569  1oc1o 8515  2oc2o 8516   No csur 27702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-tr 5284  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ord 6398  df-on 6399  df-fun 6575  df-fn 6576  df-f 6577  df-no 27705
This theorem is referenced by:  sltres  27725  nodenselem6  27752  noresle  27760  nosupbnd1lem1  27771  nosupbnd1lem2  27772  nosupbnd1lem6  27776  nosupbnd1  27777  nosupbnd2lem1  27778  nosupbnd2  27779  noinfbnd1lem1  27786  noinfbnd1lem2  27787  noinfbnd1lem6  27791  noinfbnd1  27792  noinfbnd2lem1  27793  noinfbnd2  27794  nosupinfsep  27795  noetasuplem4  27799  noetainflem4  27803
  Copyright terms: Public domain W3C validator