Theorem scutf 33275

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.

Step	Hyp	Ref	Expression
1		df-scut 33255	. . . 4 ⊢ |s = (𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ {𝑎}) ↦ (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))
2	1	mpofun 7278	. . 3 ⊢ Fun |s
3		dmscut 33274	. . 3 ⊢ dom |s = <<s
4		df-fn 6360	. . 3 ⊢ ( |s Fn <<s ↔ (Fun |s ∧ dom |s = <<s ))
5	2, 3, 4	mpbir2an 709	. 2 ⊢ |s Fn <<s
6	1	rnmpo 7286	. . 3 ⊢ ran |s = {𝑧 ∣ ∃𝑎 ∈ 𝒫 No ∃𝑏 ∈ ( <<s “ {𝑎})𝑧 = (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}))}
7		vex 3499	. . . . . . . . . 10 ⊢ 𝑎 ∈ V
8		vex 3499	. . . . . . . . . 10 ⊢ 𝑏 ∈ V
9	7, 8	elimasn 5956	. . . . . . . . 9 ⊢ (𝑏 ∈ ( <<s “ {𝑎}) ↔ ⟨𝑎, 𝑏⟩ ∈ <<s )
10		df-br 5069	. . . . . . . . 9 ⊢ (𝑎 <<s 𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ <<s )
11	9, 10	bitr4i 280	. . . . . . . 8 ⊢ (𝑏 ∈ ( <<s “ {𝑎}) ↔ 𝑎 <<s 𝑏)
12		scutval 33267	. . . . . . . . 9 ⊢ (𝑎 <<s 𝑏 → (𝑎 |s 𝑏) = (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))
13		scutcut 33268	. . . . . . . . . 10 ⊢ (𝑎 <<s 𝑏 → ((𝑎 |s 𝑏) ∈ No ∧ 𝑎 <<s {(𝑎 |s 𝑏)} ∧ {(𝑎 |s 𝑏)} <<s 𝑏))
14	13	simp1d 1138	. . . . . . . . 9 ⊢ (𝑎 <<s 𝑏 → (𝑎 |s 𝑏) ∈ No )
15	12, 14	eqeltrrd 2916	. . . . . . . 8 ⊢ (𝑎 <<s 𝑏 → (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})) ∈ No )
16	11, 15	sylbi 219	. . . . . . 7 ⊢ (𝑏 ∈ ( <<s “ {𝑎}) → (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})) ∈ No )
17		eleq1a 2910	. . . . . . 7 ⊢ ((℩𝑥 ∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})) ∈ No → (𝑧 = (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})) → 𝑧 ∈ No ))
18	16, 17	syl 17	. . . . . 6 ⊢ (𝑏 ∈ ( <<s “ {𝑎}) → (𝑧 = (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})) → 𝑧 ∈ No ))
19	18	adantl 484	. . . . 5 ⊢ ((𝑎 ∈ 𝒫 No ∧ 𝑏 ∈ ( <<s “ {𝑎})) → (𝑧 = (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})) → 𝑧 ∈ No ))
20	19	rexlimivv 3294	. . . 4 ⊢ (∃𝑎 ∈ 𝒫 No ∃𝑏 ∈ ( <<s “ {𝑎})𝑧 = (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})) → 𝑧 ∈ No )
21	20	abssi 4048	. . 3 ⊢ {𝑧 ∣ ∃𝑎 ∈ 𝒫 No ∃𝑏 ∈ ( <<s “ {𝑎})𝑧 = (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}))} ⊆ No
22	6, 21	eqsstri 4003	. 2 ⊢ ran |s ⊆ No
23		df-f 6361	. 2 ⊢ ( |s : <<s ⟶ No ↔ ( |s Fn <<s ∧ ran |s ⊆ No ))
24	5, 22, 23	mpbir2an 709	1 ⊢ |s : <<s ⟶ No

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114  {cab 2801  ∃wrex 3141  {crab 3144   ⊆ wss 3938  𝒫 cpw 4541  {csn 4569  ⟨cop 4575  ∩ cint 4878   class class class wbr 5068  dom cdm 5557  ran crn 5558   “ cima 5560  Fun wfun 6351   Fn wfn 6352  ⟶wf 6353  ‘cfv 6357  ℩crio 7115  (class class class)co 7158   No csur 33149   bday cbday 33151   <<s csslt 33252   |s cscut 33254

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-rep 5192  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-reu 3147  df-rmo 3148  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-int 4879  df-iun 4923  df-br 5069  df-opab 5131  df-mpt 5149  df-tr 5175  df-id 5462  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-we 5518  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-ord 6196  df-on 6197  df-suc 6199  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-riota 7116  df-ov 7161  df-oprab 7162  df-mpo 7163  df-1o 8104  df-2o 8105  df-no 33152  df-slt 33153  df-bday 33154  df-sslt 33253  df-scut 33255

This theorem is referenced by:  madeval  33291  madeval2  33292