Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  nodenselem6 Structured version   Visualization version   GIF version

Theorem nodenselem6 31085
 Description: The restriction of a surreal to the abstraction from nodenselem4 31083 is still a surreal. (Contributed by Scott Fenton, 16-Jun-2011.)
Assertion
Ref Expression
nodenselem6 (((𝐴 No 𝐵 No ) ∧ (( bday 𝐴) = ( bday 𝐵) ∧ 𝐴 <s 𝐵)) → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ∈ No )
Distinct variable groups:   𝐴,𝑎   𝐵,𝑎

Proof of Theorem nodenselem6
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 nodenselem4 31083 . . . 4 (((𝐴 No 𝐵 No ) ∧ 𝐴 <s 𝐵) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
21adantrl 748 . . 3 (((𝐴 No 𝐵 No ) ∧ (( bday 𝐴) = ( bday 𝐵) ∧ 𝐴 <s 𝐵)) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
3 nofnbday 31049 . . . . . 6 (𝐴 No 𝐴 Fn ( bday 𝐴))
43ad2antrr 758 . . . . 5 (((𝐴 No 𝐵 No ) ∧ (( bday 𝐴) = ( bday 𝐵) ∧ 𝐴 <s 𝐵)) → 𝐴 Fn ( bday 𝐴))
5 nodenselem5 31084 . . . . . 6 (((𝐴 No 𝐵 No ) ∧ (( bday 𝐴) = ( bday 𝐵) ∧ 𝐴 <s 𝐵)) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ ( bday 𝐴))
6 bdayelon 31079 . . . . . . 7 ( bday 𝐴) ∈ On
76onelssi 5753 . . . . . 6 ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ ( bday 𝐴) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ⊆ ( bday 𝐴))
85, 7syl 17 . . . . 5 (((𝐴 No 𝐵 No ) ∧ (( bday 𝐴) = ( bday 𝐵) ∧ 𝐴 <s 𝐵)) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ⊆ ( bday 𝐴))
9 fnssres 5918 . . . . 5 ((𝐴 Fn ( bday 𝐴) ∧ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ⊆ ( bday 𝐴)) → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) Fn {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
104, 8, 9syl2anc 691 . . . 4 (((𝐴 No 𝐵 No ) ∧ (( bday 𝐴) = ( bday 𝐵) ∧ 𝐴 <s 𝐵)) → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) Fn {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
11 resss 5342 . . . . . 6 (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ⊆ 𝐴
12 rnss 5275 . . . . . 6 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ⊆ 𝐴 → ran (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ⊆ ran 𝐴)
1311, 12ax-mp 5 . . . . 5 ran (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ⊆ ran 𝐴
14 norn 31048 . . . . . 6 (𝐴 No → ran 𝐴 ⊆ {1𝑜, 2𝑜})
1514ad2antrr 758 . . . . 5 (((𝐴 No 𝐵 No ) ∧ (( bday 𝐴) = ( bday 𝐵) ∧ 𝐴 <s 𝐵)) → ran 𝐴 ⊆ {1𝑜, 2𝑜})
1613, 15syl5ss 3579 . . . 4 (((𝐴 No 𝐵 No ) ∧ (( bday 𝐴) = ( bday 𝐵) ∧ 𝐴 <s 𝐵)) → ran (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ⊆ {1𝑜, 2𝑜})
17 df-f 5808 . . . 4 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}): {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}⟶{1𝑜, 2𝑜} ↔ ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) Fn {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∧ ran (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ⊆ {1𝑜, 2𝑜}))
1810, 16, 17sylanbrc 695 . . 3 (((𝐴 No 𝐵 No ) ∧ (( bday 𝐴) = ( bday 𝐵) ∧ 𝐴 <s 𝐵)) → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}): {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}⟶{1𝑜, 2𝑜})
19 feq2 5940 . . . 4 (𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}):𝑥⟶{1𝑜, 2𝑜} ↔ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}): {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}⟶{1𝑜, 2𝑜}))
2019rspcev 3282 . . 3 (( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}): {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}⟶{1𝑜, 2𝑜}) → ∃𝑥 ∈ On (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}):𝑥⟶{1𝑜, 2𝑜})
212, 18, 20syl2anc 691 . 2 (((𝐴 No 𝐵 No ) ∧ (( bday 𝐴) = ( bday 𝐵) ∧ 𝐴 <s 𝐵)) → ∃𝑥 ∈ On (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}):𝑥⟶{1𝑜, 2𝑜})
22 elno 31043 . 2 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ∈ No ↔ ∃𝑥 ∈ On (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}):𝑥⟶{1𝑜, 2𝑜})
2321, 22sylibr 223 1 (((𝐴 No 𝐵 No ) ∧ (( bday 𝐴) = ( bday 𝐵) ∧ 𝐴 <s 𝐵)) → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ∈ No )
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∃wrex 2897  {crab 2900   ⊆ wss 3540  {cpr 4127  ∩ cint 4410   class class class wbr 4583  ran crn 5039   ↾ cres 5040  Oncon0 5640   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  1𝑜c1o 7440  2𝑜c2o 7441   No csur 31037
 Copyright terms: Public domain W3C validator