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

Theorem noeta 32243
Description: The full-eta axiom for the surreal numbers. This is the single most important property of the surreals. It says that, given two sets of surreals such that one comes completely before the other, there is a surreal lying strictly between the two. Furthermore, there is an upper bound on the birthday of that surreal. Alling's axiom FE. (Contributed by Scott Fenton, 7-Dec-2021.)
Assertion
Ref Expression
noeta (((𝐴 No 𝐴𝑉) ∧ (𝐵 No 𝐵𝑊) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 <s 𝑦) → ∃𝑧 No (∀𝑥𝐴 𝑥 <s 𝑧 ∧ ∀𝑦𝐵 𝑧 <s 𝑦 ∧ ( bday 𝑧) ⊆ suc ( bday “ (𝐴𝐵))))
Distinct variable groups:   𝑥,𝐴,𝑦,𝑧   𝑥,𝐵,𝑦,𝑧
Allowed substitution hints:   𝑉(𝑥,𝑦,𝑧)   𝑊(𝑥,𝑦,𝑧)

Proof of Theorem noeta
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eleq1w 2826 . . . . . . 7 (𝑓 = 𝑐 → (𝑓 ∈ dom 𝑑𝑐 ∈ dom 𝑑))
2 suceq 5972 . . . . . . . . . . 11 (𝑓 = 𝑐 → suc 𝑓 = suc 𝑐)
32reseq2d 5564 . . . . . . . . . 10 (𝑓 = 𝑐 → (𝑑 ↾ suc 𝑓) = (𝑑 ↾ suc 𝑐))
42reseq2d 5564 . . . . . . . . . 10 (𝑓 = 𝑐 → (𝑒 ↾ suc 𝑓) = (𝑒 ↾ suc 𝑐))
53, 4eqeq12d 2779 . . . . . . . . 9 (𝑓 = 𝑐 → ((𝑑 ↾ suc 𝑓) = (𝑒 ↾ suc 𝑓) ↔ (𝑑 ↾ suc 𝑐) = (𝑒 ↾ suc 𝑐)))
65imbi2d 331 . . . . . . . 8 (𝑓 = 𝑐 → ((¬ 𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑓) = (𝑒 ↾ suc 𝑓)) ↔ (¬ 𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑐) = (𝑒 ↾ suc 𝑐))))
76ralbidv 3132 . . . . . . 7 (𝑓 = 𝑐 → (∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑓) = (𝑒 ↾ suc 𝑓)) ↔ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑐) = (𝑒 ↾ suc 𝑐))))
8 fveqeq2 6383 . . . . . . 7 (𝑓 = 𝑐 → ((𝑑𝑓) = 𝑎 ↔ (𝑑𝑐) = 𝑎))
91, 7, 83anbi123d 1560 . . . . . 6 (𝑓 = 𝑐 → ((𝑓 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑓) = (𝑒 ↾ suc 𝑓)) ∧ (𝑑𝑓) = 𝑎) ↔ (𝑐 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑐) = (𝑒 ↾ suc 𝑐)) ∧ (𝑑𝑐) = 𝑎)))
109rexbidv 3198 . . . . 5 (𝑓 = 𝑐 → (∃𝑑𝐴 (𝑓 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑓) = (𝑒 ↾ suc 𝑓)) ∧ (𝑑𝑓) = 𝑎) ↔ ∃𝑑𝐴 (𝑐 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑐) = (𝑒 ↾ suc 𝑐)) ∧ (𝑑𝑐) = 𝑎)))
1110iotabidv 6051 . . . 4 (𝑓 = 𝑐 → (℩𝑎𝑑𝐴 (𝑓 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑓) = (𝑒 ↾ suc 𝑓)) ∧ (𝑑𝑓) = 𝑎)) = (℩𝑎𝑑𝐴 (𝑐 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑐) = (𝑒 ↾ suc 𝑐)) ∧ (𝑑𝑐) = 𝑎)))
1211cbvmptv 4908 . . 3 (𝑓 ∈ {𝑏 ∣ ∃𝑑𝐴 (𝑏 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑏) = (𝑒 ↾ suc 𝑏)))} ↦ (℩𝑎𝑑𝐴 (𝑓 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑓) = (𝑒 ↾ suc 𝑓)) ∧ (𝑑𝑓) = 𝑎))) = (𝑐 ∈ {𝑏 ∣ ∃𝑑𝐴 (𝑏 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑏) = (𝑒 ↾ suc 𝑏)))} ↦ (℩𝑎𝑑𝐴 (𝑐 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑐) = (𝑒 ↾ suc 𝑐)) ∧ (𝑑𝑐) = 𝑎)))
13 ifeq2 4247 . . 3 ((𝑓 ∈ {𝑏 ∣ ∃𝑑𝐴 (𝑏 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑏) = (𝑒 ↾ suc 𝑏)))} ↦ (℩𝑎𝑑𝐴 (𝑓 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑓) = (𝑒 ↾ suc 𝑓)) ∧ (𝑑𝑓) = 𝑎))) = (𝑐 ∈ {𝑏 ∣ ∃𝑑𝐴 (𝑏 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑏) = (𝑒 ↾ suc 𝑏)))} ↦ (℩𝑎𝑑𝐴 (𝑐 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑐) = (𝑒 ↾ suc 𝑐)) ∧ (𝑑𝑐) = 𝑎))) → if(∃𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏, ((𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏) ∪ {⟨dom (𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏), 2𝑜⟩}), (𝑓 ∈ {𝑏 ∣ ∃𝑑𝐴 (𝑏 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑏) = (𝑒 ↾ suc 𝑏)))} ↦ (℩𝑎𝑑𝐴 (𝑓 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑓) = (𝑒 ↾ suc 𝑓)) ∧ (𝑑𝑓) = 𝑎)))) = if(∃𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏, ((𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏) ∪ {⟨dom (𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏), 2𝑜⟩}), (𝑐 ∈ {𝑏 ∣ ∃𝑑𝐴 (𝑏 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑏) = (𝑒 ↾ suc 𝑏)))} ↦ (℩𝑎𝑑𝐴 (𝑐 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑐) = (𝑒 ↾ suc 𝑐)) ∧ (𝑑𝑐) = 𝑎)))))
1412, 13ax-mp 5 . 2 if(∃𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏, ((𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏) ∪ {⟨dom (𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏), 2𝑜⟩}), (𝑓 ∈ {𝑏 ∣ ∃𝑑𝐴 (𝑏 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑏) = (𝑒 ↾ suc 𝑏)))} ↦ (℩𝑎𝑑𝐴 (𝑓 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑓) = (𝑒 ↾ suc 𝑓)) ∧ (𝑑𝑓) = 𝑎)))) = if(∃𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏, ((𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏) ∪ {⟨dom (𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏), 2𝑜⟩}), (𝑐 ∈ {𝑏 ∣ ∃𝑑𝐴 (𝑏 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑏) = (𝑒 ↾ suc 𝑏)))} ↦ (℩𝑎𝑑𝐴 (𝑐 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑐) = (𝑒 ↾ suc 𝑐)) ∧ (𝑑𝑐) = 𝑎))))
15 eqid 2764 . 2 (if(∃𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏, ((𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏) ∪ {⟨dom (𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏), 2𝑜⟩}), (𝑓 ∈ {𝑏 ∣ ∃𝑑𝐴 (𝑏 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑏) = (𝑒 ↾ suc 𝑏)))} ↦ (℩𝑎𝑑𝐴 (𝑓 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑓) = (𝑒 ↾ suc 𝑓)) ∧ (𝑑𝑓) = 𝑎)))) ∪ ((suc ( bday 𝐵) ∖ dom if(∃𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏, ((𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏) ∪ {⟨dom (𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏), 2𝑜⟩}), (𝑓 ∈ {𝑏 ∣ ∃𝑑𝐴 (𝑏 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑏) = (𝑒 ↾ suc 𝑏)))} ↦ (℩𝑎𝑑𝐴 (𝑓 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑓) = (𝑒 ↾ suc 𝑓)) ∧ (𝑑𝑓) = 𝑎))))) × {1𝑜})) = (if(∃𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏, ((𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏) ∪ {⟨dom (𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏), 2𝑜⟩}), (𝑓 ∈ {𝑏 ∣ ∃𝑑𝐴 (𝑏 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑏) = (𝑒 ↾ suc 𝑏)))} ↦ (℩𝑎𝑑𝐴 (𝑓 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑓) = (𝑒 ↾ suc 𝑓)) ∧ (𝑑𝑓) = 𝑎)))) ∪ ((suc ( bday 𝐵) ∖ dom if(∃𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏, ((𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏) ∪ {⟨dom (𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏), 2𝑜⟩}), (𝑓 ∈ {𝑏 ∣ ∃𝑑𝐴 (𝑏 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑏) = (𝑒 ↾ suc 𝑏)))} ↦ (℩𝑎𝑑𝐴 (𝑓 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑓) = (𝑒 ↾ suc 𝑓)) ∧ (𝑑𝑓) = 𝑎))))) × {1𝑜}))
1614, 15noetalem5 32242 1 (((𝐴 No 𝐴𝑉) ∧ (𝐵 No 𝐵𝑊) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 <s 𝑦) → ∃𝑧 No (∀𝑥𝐴 𝑥 <s 𝑧 ∧ ∀𝑦𝐵 𝑧 <s 𝑦 ∧ ( bday 𝑧) ⊆ suc ( bday “ (𝐴𝐵))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384  w3a 1107   = wceq 1652  wcel 2155  {cab 2750  wral 3054  wrex 3055  cdif 3728  cun 3729  wss 3731  ifcif 4242  {csn 4333  cop 4339   cuni 4593   class class class wbr 4808  cmpt 4887   × cxp 5274  dom cdm 5276  cres 5278  cima 5279  suc csuc 5909  cio 6028  cfv 6067  crio 6801  1𝑜c1o 7756  2𝑜c2o 7757   No csur 32168   <s cslt 32169   bday cbday 32170
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-rep 4929  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-pss 3747  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-tp 4338  df-op 4340  df-uni 4594  df-int 4633  df-iun 4677  df-br 4809  df-opab 4871  df-mpt 4888  df-tr 4911  df-id 5184  df-eprel 5189  df-po 5197  df-so 5198  df-fr 5235  df-we 5237  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-ord 5910  df-on 5911  df-suc 5913  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-riota 6802  df-1o 7763  df-2o 7764  df-no 32171  df-slt 32172  df-bday 32173
This theorem is referenced by:  conway  32285  etasslt  32295
  Copyright terms: Public domain W3C validator