![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > noreson | Structured version Visualization version GIF version |
Description: The restriction of a surreal to an ordinal is still a surreal. (Contributed by Scott Fenton, 4-Sep-2011.) |
Ref | Expression |
---|---|
noreson | ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ On) → (𝐴 ↾ 𝐵) ∈ No ) |
Step | Hyp | Ref | 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})) | |
5 | 4 | rspcev 3635 | . . . . . . . 8 ⊢ (((𝑥 ∩ 𝐵) ∈ On ∧ (𝐴 ↾ 𝐵):(𝑥 ∩ 𝐵)⟶{1o, 2o}) → ∃𝑦 ∈ On (𝐴 ↾ 𝐵):𝑦⟶{1o, 2o}) |
6 | 2, 3, 5 | syl2an 595 | . . . . . . 7 ⊢ (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴:𝑥⟶{1o, 2o}) → ∃𝑦 ∈ On (𝐴 ↾ 𝐵):𝑦⟶{1o, 2o}) |
7 | 6 | an32s 651 | . . . . . 6 ⊢ (((𝑥 ∈ On ∧ 𝐴:𝑥⟶{1o, 2o}) ∧ 𝐵 ∈ On) → ∃𝑦 ∈ On (𝐴 ↾ 𝐵):𝑦⟶{1o, 2o}) |
8 | 7 | ex 412 | . . . . 5 ⊢ ((𝑥 ∈ On ∧ 𝐴:𝑥⟶{1o, 2o}) → (𝐵 ∈ On → ∃𝑦 ∈ On (𝐴 ↾ 𝐵):𝑦⟶{1o, 2o})) |
9 | 8 | rexlimiva 3153 | . . . 4 ⊢ (∃𝑥 ∈ On 𝐴:𝑥⟶{1o, 2o} → (𝐵 ∈ On → ∃𝑦 ∈ On (𝐴 ↾ 𝐵):𝑦⟶{1o, 2o})) |
10 | 9 | imp 406 | . . 3 ⊢ ((∃𝑥 ∈ On 𝐴:𝑥⟶{1o, 2o} ∧ 𝐵 ∈ On) → ∃𝑦 ∈ On (𝐴 ↾ 𝐵):𝑦⟶{1o, 2o}) |
11 | 1, 10 | sylanb 580 | . 2 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ On) → ∃𝑦 ∈ On (𝐴 ↾ 𝐵):𝑦⟶{1o, 2o}) |
12 | elno 27708 | . 2 ⊢ ((𝐴 ↾ 𝐵) ∈ No ↔ ∃𝑦 ∈ On (𝐴 ↾ 𝐵):𝑦⟶{1o, 2o}) | |
13 | 11, 12 | sylibr 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 |