MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nosupdm Structured version   Visualization version   GIF version

Theorem nosupdm 27075
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 4499 . . . . 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, 2eqtrid 2785 . . . 4 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦𝑆 = (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
43dmeqd 5865 . . 3 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = dom (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
5 iotaex 6473 . . . 4 (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)) ∈ V
6 eqid 2733 . . . 4 (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))
75, 6dmmpti 6649 . . 3 dom (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) = {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}
84, 7eqtrdi 2789 . 2 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
9 dmeq 5863 . . . . . . 7 (𝑢 = 𝑝 → dom 𝑢 = dom 𝑝)
109eleq2d 2820 . . . . . 6 (𝑢 = 𝑝 → (𝑦 ∈ dom 𝑢𝑦 ∈ dom 𝑝))
11 breq1 5112 . . . . . . . . . 10 (𝑣 = 𝑞 → (𝑣 <s 𝑢𝑞 <s 𝑢))
1211notbid 318 . . . . . . . . 9 (𝑣 = 𝑞 → (¬ 𝑣 <s 𝑢 ↔ ¬ 𝑞 <s 𝑢))
13 reseq1 5935 . . . . . . . . . 10 (𝑣 = 𝑞 → (𝑣 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦))
1413eqeq2d 2744 . . . . . . . . 9 (𝑣 = 𝑞 → ((𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦) ↔ (𝑢 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦)))
1512, 14imbi12d 345 . . . . . . . 8 (𝑣 = 𝑞 → ((¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ (¬ 𝑞 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦))))
1615cbvralvw 3224 . . . . . . 7 (∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ ∀𝑞𝐴𝑞 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦)))
17 breq2 5113 . . . . . . . . . 10 (𝑢 = 𝑝 → (𝑞 <s 𝑢𝑞 <s 𝑝))
1817notbid 318 . . . . . . . . 9 (𝑢 = 𝑝 → (¬ 𝑞 <s 𝑢 ↔ ¬ 𝑞 <s 𝑝))
19 reseq1 5935 . . . . . . . . . 10 (𝑢 = 𝑝 → (𝑢 ↾ suc 𝑦) = (𝑝 ↾ suc 𝑦))
2019eqeq1d 2735 . . . . . . . . 9 (𝑢 = 𝑝 → ((𝑢 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦) ↔ (𝑝 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦)))
2118, 20imbi12d 345 . . . . . . . 8 (𝑢 = 𝑝 → ((¬ 𝑞 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦)) ↔ (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦))))
2221ralbidv 3171 . . . . . . 7 (𝑢 = 𝑝 → (∀𝑞𝐴𝑞 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦)) ↔ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦))))
2316, 22bitrid 283 . . . . . 6 (𝑢 = 𝑝 → (∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦))))
2410, 23anbi12d 632 . . . . 5 (𝑢 = 𝑝 → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ (𝑦 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦)))))
2524cbvrexvw 3225 . . . 4 (∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ∃𝑝𝐴 (𝑦 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦))))
26 eleq1w 2817 . . . . . 6 (𝑦 = 𝑧 → (𝑦 ∈ dom 𝑝𝑧 ∈ dom 𝑝))
27 suceq 6387 . . . . . . . . . 10 (𝑦 = 𝑧 → suc 𝑦 = suc 𝑧)
2827reseq2d 5941 . . . . . . . . 9 (𝑦 = 𝑧 → (𝑝 ↾ suc 𝑦) = (𝑝 ↾ suc 𝑧))
2927reseq2d 5941 . . . . . . . . 9 (𝑦 = 𝑧 → (𝑞 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑧))
3028, 29eqeq12d 2749 . . . . . . . 8 (𝑦 = 𝑧 → ((𝑝 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦) ↔ (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))
3130imbi2d 341 . . . . . . 7 (𝑦 = 𝑧 → ((¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦)) ↔ (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧))))
3231ralbidv 3171 . . . . . 6 (𝑦 = 𝑧 → (∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦)) ↔ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧))))
3326, 32anbi12d 632 . . . . 5 (𝑦 = 𝑧 → ((𝑦 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦))) ↔ (𝑧 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))))
3433rexbidv 3172 . . . 4 (𝑦 = 𝑧 → (∃𝑝𝐴 (𝑦 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑦) = (𝑞 ↾ suc 𝑦))) ↔ ∃𝑝𝐴 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))))
3525, 34bitrid 283 . . 3 (𝑦 = 𝑧 → (∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ∃𝑝𝐴 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))))
3635cbvabv 2806 . 2 {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} = {𝑧 ∣ ∃𝑝𝐴 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))}
378, 36eqtrdi 2789 1 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = {𝑧 ∣ ∃𝑝𝐴 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))})
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397  w3a 1088   = wceq 1542  wcel 2107  {cab 2710  wral 3061  wrex 3070  cun 3912  ifcif 4490  {csn 4590  cop 4596   class class class wbr 5109  cmpt 5192  dom cdm 5637  cres 5639  suc csuc 6323  cio 6450  cfv 6500  crio 7316  2oc2o 8410   <s cslt 27012
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5260  ax-nul 5267  ax-pr 5388
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-br 5110  df-opab 5172  df-mpt 5193  df-id 5535  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-res 5649  df-suc 6327  df-iota 6452  df-fun 6502  df-fn 6503
This theorem is referenced by:  nosupbnd1lem3  27081  nosupbnd1lem5  27083  nosupbnd2  27087
  Copyright terms: Public domain W3C validator