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

Theorem scutf 32225
 Description: Functionhood statement for the surreal cut operator. (Contributed by Scott Fenton, 15-Dec-2021.)
Assertion
Ref Expression
scutf |s : <<s ⟶ No

Proof of Theorem scutf
Dummy variables 𝑎 𝑏 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-scut 32205 . . . 4 |s = (𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ {𝑎}) ↦ (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))
21mpt2fun 6927 . . 3 Fun |s
3 dmscut 32224 . . 3 dom |s = <<s
4 df-fn 6052 . . 3 ( |s Fn <<s ↔ (Fun |s ∧ dom |s = <<s ))
52, 3, 4mpbir2an 993 . 2 |s Fn <<s
61rnmpt2 6935 . . 3 ran |s = {𝑧 ∣ ∃𝑎 ∈ 𝒫 No 𝑏 ∈ ( <<s “ {𝑎})𝑧 = (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}))}
7 vex 3343 . . . . . . . . . 10 𝑎 ∈ V
8 vex 3343 . . . . . . . . . 10 𝑏 ∈ V
97, 8elimasn 5648 . . . . . . . . 9 (𝑏 ∈ ( <<s “ {𝑎}) ↔ ⟨𝑎, 𝑏⟩ ∈ <<s )
10 df-br 4805 . . . . . . . . 9 (𝑎 <<s 𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ <<s )
119, 10bitr4i 267 . . . . . . . 8 (𝑏 ∈ ( <<s “ {𝑎}) ↔ 𝑎 <<s 𝑏)
12 scutval 32217 . . . . . . . . 9 (𝑎 <<s 𝑏 → (𝑎 |s 𝑏) = (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))
13 scutcut 32218 . . . . . . . . . 10 (𝑎 <<s 𝑏 → ((𝑎 |s 𝑏) ∈ No 𝑎 <<s {(𝑎 |s 𝑏)} ∧ {(𝑎 |s 𝑏)} <<s 𝑏))
1413simp1d 1137 . . . . . . . . 9 (𝑎 <<s 𝑏 → (𝑎 |s 𝑏) ∈ No )
1512, 14eqeltrrd 2840 . . . . . . . 8 (𝑎 <<s 𝑏 → (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})) ∈ No )
1611, 15sylbi 207 . . . . . . 7 (𝑏 ∈ ( <<s “ {𝑎}) → (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})) ∈ No )
17 eleq1a 2834 . . . . . . 7 ((𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})) ∈ No → (𝑧 = (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})) → 𝑧 No ))
1816, 17syl 17 . . . . . 6 (𝑏 ∈ ( <<s “ {𝑎}) → (𝑧 = (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})) → 𝑧 No ))
1918adantl 473 . . . . 5 ((𝑎 ∈ 𝒫 No 𝑏 ∈ ( <<s “ {𝑎})) → (𝑧 = (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})) → 𝑧 No ))
2019rexlimivv 3174 . . . 4 (∃𝑎 ∈ 𝒫 No 𝑏 ∈ ( <<s “ {𝑎})𝑧 = (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})) → 𝑧 No )
2120abssi 3818 . . 3 {𝑧 ∣ ∃𝑎 ∈ 𝒫 No 𝑏 ∈ ( <<s “ {𝑎})𝑧 = (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}))} ⊆ No
226, 21eqsstri 3776 . 2 ran |s ⊆ No
23 df-f 6053 . 2 ( |s : <<s ⟶ No ↔ ( |s Fn <<s ∧ ran |s ⊆ No ))
245, 22, 23mpbir2an 993 1 |s : <<s ⟶ No
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   = wceq 1632   ∈ wcel 2139  {cab 2746  ∃wrex 3051  {crab 3054   ⊆ wss 3715  𝒫 cpw 4302  {csn 4321  ⟨cop 4327  ∩ cint 4627   class class class wbr 4804  dom cdm 5266  ran crn 5267   “ cima 5269  Fun wfun 6043   Fn wfn 6044  ⟶wf 6045  ‘cfv 6049  ℩crio 6773  (class class class)co 6813   No csur 32099   bday cbday 32101   <
 Copyright terms: Public domain W3C validator