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

Theorem nosupdm 33204
Description: The domain of the surreal supremum when there is no maximum. The primary point of this theorem is to change bound variable. (Contributed by Scott Fenton, 6-Dec-2021.)
Hypothesis
Ref Expression
nosupdm.1 𝑆 = if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
Assertion
Ref Expression
nosupdm (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = {𝑧 ∣ ∃𝑝𝐴 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))})
Distinct variable groups:   𝐴,𝑔   𝐴,𝑝,𝑞,𝑢,𝑣,𝑦,𝑧   𝑢,𝑔,𝑣,𝑦   𝑞,𝑝,𝑢,𝑣,𝑦,𝑧
Allowed substitution hints:   𝐴(𝑥)   𝑆(𝑥,𝑦,𝑧,𝑣,𝑢,𝑔,𝑞,𝑝)

Proof of Theorem nosupdm
StepHypRef Expression
1 nosupdm.1 . . . . 5 𝑆 = if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
2 iffalse 4475 . . . . 5 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
31, 2syl5eq 2868 . . . 4 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦𝑆 = (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
43dmeqd 5773 . . 3 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = dom (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
5 iotaex 6334 . . . 4 (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)) ∈ V
6 eqid 2821 . . . 4 (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))
75, 6dmmpti 6491 . . 3 dom (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) = {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}
84, 7syl6eq 2872 . 2 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
9 dmeq 5771 . . . . . . 7 (𝑢 = 𝑝 → dom 𝑢 = dom 𝑝)
109eleq2d 2898 . . . . . 6 (𝑢 = 𝑝 → (𝑦 ∈ dom 𝑢𝑦 ∈ dom 𝑝))
11 breq1 5068 . . . . . . . . . 10 (𝑣 = 𝑞 → (𝑣 <s 𝑢𝑞 <s 𝑢))
1211notbid 320 . . . . . . . . 9 (𝑣 = 𝑞 → (¬ 𝑣 <s 𝑢 ↔ ¬ 𝑞 <s 𝑢))
13 reseq1 5846 . . . . . . . . . 10 (𝑣 = 𝑞 → (𝑣 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦))
1413eqeq2d 2832 . . . . . . . . 9 (𝑣 = 𝑞 → ((𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦) ↔ (𝑢 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦)))
1512, 14imbi12d 347 . . . . . . . 8 (𝑣 = 𝑞 → ((¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ (¬ 𝑞 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦))))
1615cbvralvw 3449 . . . . . . 7 (∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ ∀𝑞𝐴𝑞 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦)))
17 breq2 5069 . . . . . . . . . 10 (𝑢 = 𝑝 → (𝑞 <s 𝑢𝑞 <s 𝑝))
1817notbid 320 . . . . . . . . 9 (𝑢 = 𝑝 → (¬ 𝑞 <s 𝑢 ↔ ¬ 𝑞 <s 𝑝))
19 reseq1 5846 . . . . . . . . . 10 (𝑢 = 𝑝 → (𝑢 ↾ suc 𝑦) = (𝑝 ↾ suc 𝑦))
2019eqeq1d 2823 . . . . . . . . 9 (𝑢 = 𝑝 → ((𝑢 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦) ↔ (𝑝 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦)))
2118, 20imbi12d 347 . . . . . . . 8 (𝑢 = 𝑝 → ((¬ 𝑞 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦)) ↔ (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦))))
2221ralbidv 3197 . . . . . . 7 (𝑢 = 𝑝 → (∀𝑞𝐴𝑞 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦)) ↔ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦))))
2316, 22syl5bb 285 . . . . . 6 (𝑢 = 𝑝 → (∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦))))
2410, 23anbi12d 632 . . . . 5 (𝑢 = 𝑝 → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ (𝑦 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦)))))
2524cbvrexvw 3450 . . . 4 (∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ∃𝑝𝐴 (𝑦 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦))))
26 eleq1w 2895 . . . . . 6 (𝑦 = 𝑧 → (𝑦 ∈ dom 𝑝𝑧 ∈ dom 𝑝))
27 suceq 6255 . . . . . . . . . 10 (𝑦 = 𝑧 → suc 𝑦 = suc 𝑧)
2827reseq2d 5852 . . . . . . . . 9 (𝑦 = 𝑧 → (𝑝 ↾ suc 𝑦) = (𝑝 ↾ suc 𝑧))
2927reseq2d 5852 . . . . . . . . 9 (𝑦 = 𝑧 → (𝑞 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑧))
3028, 29eqeq12d 2837 . . . . . . . 8 (𝑦 = 𝑧 → ((𝑝 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦) ↔ (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))
3130imbi2d 343 . . . . . . 7 (𝑦 = 𝑧 → ((¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦)) ↔ (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧))))
3231ralbidv 3197 . . . . . 6 (𝑦 = 𝑧 → (∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦)) ↔ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧))))
3326, 32anbi12d 632 . . . . 5 (𝑦 = 𝑧 → ((𝑦 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦))) ↔ (𝑧 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))))
3433rexbidv 3297 . . . 4 (𝑦 = 𝑧 → (∃𝑝𝐴 (𝑦 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦))) ↔ ∃𝑝𝐴 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))))
3525, 34syl5bb 285 . . 3 (𝑦 = 𝑧 → (∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ∃𝑝𝐴 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))))
3635cbvabv 2889 . 2 {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} = {𝑧 ∣ ∃𝑝𝐴 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))}
378, 36syl6eq 2872 1 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = {𝑧 ∣ ∃𝑝𝐴 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))})
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 398  w3a 1083   = wceq 1533  wcel 2110  {cab 2799  wral 3138  wrex 3139  cun 3933  ifcif 4466  {csn 4566  cop 4572   class class class wbr 5065  cmpt 5145  dom cdm 5554  cres 5556  suc csuc 6192  cio 6311  cfv 6354  crio 7112  2oc2o 8095   <s cslt 33148
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pr 5329
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4838  df-br 5066  df-opab 5128  df-mpt 5146  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-res 5566  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357
This theorem is referenced by:  nosupbnd1lem3  33210  nosupbnd1lem5  33212  nosupbnd2  33216
  Copyright terms: Public domain W3C validator