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

Theorem noeta 33330
 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 2875 . . . . . . 7 (𝑓 = 𝑐 → (𝑓 ∈ dom 𝑑𝑐 ∈ dom 𝑑))
2 suceq 6228 . . . . . . . . . . 11 (𝑓 = 𝑐 → suc 𝑓 = suc 𝑐)
32reseq2d 5822 . . . . . . . . . 10 (𝑓 = 𝑐 → (𝑑 ↾ suc 𝑓) = (𝑑 ↾ suc 𝑐))
42reseq2d 5822 . . . . . . . . . 10 (𝑓 = 𝑐 → (𝑒 ↾ suc 𝑓) = (𝑒 ↾ suc 𝑐))
53, 4eqeq12d 2817 . . . . . . . . 9 (𝑓 = 𝑐 → ((𝑑 ↾ suc 𝑓) = (𝑒 ↾ suc 𝑓) ↔ (𝑑 ↾ suc 𝑐) = (𝑒 ↾ suc 𝑐)))
65imbi2d 344 . . . . . . . 8 (𝑓 = 𝑐 → ((¬ 𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑓) = (𝑒 ↾ suc 𝑓)) ↔ (¬ 𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑐) = (𝑒 ↾ suc 𝑐))))
76ralbidv 3165 . . . . . . 7 (𝑓 = 𝑐 → (∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑓) = (𝑒 ↾ suc 𝑓)) ↔ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑐) = (𝑒 ↾ suc 𝑐))))
8 fveqeq2 6658 . . . . . . 7 (𝑓 = 𝑐 → ((𝑑𝑓) = 𝑎 ↔ (𝑑𝑐) = 𝑎))
91, 7, 83anbi123d 1433 . . . . . 6 (𝑓 = 𝑐 → ((𝑓 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑓) = (𝑒 ↾ suc 𝑓)) ∧ (𝑑𝑓) = 𝑎) ↔ (𝑐 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑐) = (𝑒 ↾ suc 𝑐)) ∧ (𝑑𝑐) = 𝑎)))
109rexbidv 3259 . . . . 5 (𝑓 = 𝑐 → (∃𝑑𝐴 (𝑓 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑓) = (𝑒 ↾ suc 𝑓)) ∧ (𝑑𝑓) = 𝑎) ↔ ∃𝑑𝐴 (𝑐 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑐) = (𝑒 ↾ suc 𝑐)) ∧ (𝑑𝑐) = 𝑎)))
1110iotabidv 6312 . . . 4 (𝑓 = 𝑐 → (℩𝑎𝑑𝐴 (𝑓 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑓) = (𝑒 ↾ suc 𝑓)) ∧ (𝑑𝑓) = 𝑎)) = (℩𝑎𝑑𝐴 (𝑐 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑐) = (𝑒 ↾ suc 𝑐)) ∧ (𝑑𝑐) = 𝑎)))
1211cbvmptv 5136 . . 3 (𝑓 ∈ {𝑏 ∣ ∃𝑑𝐴 (𝑏 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑏) = (𝑒 ↾ suc 𝑏)))} ↦ (℩𝑎𝑑𝐴 (𝑓 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑓) = (𝑒 ↾ suc 𝑓)) ∧ (𝑑𝑓) = 𝑎))) = (𝑐 ∈ {𝑏 ∣ ∃𝑑𝐴 (𝑏 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑏) = (𝑒 ↾ suc 𝑏)))} ↦ (℩𝑎𝑑𝐴 (𝑐 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑐) = (𝑒 ↾ suc 𝑐)) ∧ (𝑑𝑐) = 𝑎)))
13 ifeq2 4433 . . 3 ((𝑓 ∈ {𝑏 ∣ ∃𝑑𝐴 (𝑏 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑏) = (𝑒 ↾ suc 𝑏)))} ↦ (℩𝑎𝑑𝐴 (𝑓 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑓) = (𝑒 ↾ suc 𝑓)) ∧ (𝑑𝑓) = 𝑎))) = (𝑐 ∈ {𝑏 ∣ ∃𝑑𝐴 (𝑏 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑏) = (𝑒 ↾ suc 𝑏)))} ↦ (℩𝑎𝑑𝐴 (𝑐 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑐) = (𝑒 ↾ suc 𝑐)) ∧ (𝑑𝑐) = 𝑎))) → if(∃𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏, ((𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏) ∪ {⟨dom (𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏), 2o⟩}), (𝑓 ∈ {𝑏 ∣ ∃𝑑𝐴 (𝑏 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑏) = (𝑒 ↾ suc 𝑏)))} ↦ (℩𝑎𝑑𝐴 (𝑓 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑓) = (𝑒 ↾ suc 𝑓)) ∧ (𝑑𝑓) = 𝑎)))) = if(∃𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏, ((𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏) ∪ {⟨dom (𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏), 2o⟩}), (𝑐 ∈ {𝑏 ∣ ∃𝑑𝐴 (𝑏 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑏) = (𝑒 ↾ suc 𝑏)))} ↦ (℩𝑎𝑑𝐴 (𝑐 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑐) = (𝑒 ↾ suc 𝑐)) ∧ (𝑑𝑐) = 𝑎)))))
1412, 13ax-mp 5 . 2 if(∃𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏, ((𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏) ∪ {⟨dom (𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏), 2o⟩}), (𝑓 ∈ {𝑏 ∣ ∃𝑑𝐴 (𝑏 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑏) = (𝑒 ↾ suc 𝑏)))} ↦ (℩𝑎𝑑𝐴 (𝑓 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑓) = (𝑒 ↾ suc 𝑓)) ∧ (𝑑𝑓) = 𝑎)))) = if(∃𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏, ((𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏) ∪ {⟨dom (𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏), 2o⟩}), (𝑐 ∈ {𝑏 ∣ ∃𝑑𝐴 (𝑏 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑏) = (𝑒 ↾ suc 𝑏)))} ↦ (℩𝑎𝑑𝐴 (𝑐 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑐) = (𝑒 ↾ suc 𝑐)) ∧ (𝑑𝑐) = 𝑎))))
15 eqid 2801 . 2 (if(∃𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏, ((𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏) ∪ {⟨dom (𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏), 2o⟩}), (𝑓 ∈ {𝑏 ∣ ∃𝑑𝐴 (𝑏 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑏) = (𝑒 ↾ suc 𝑏)))} ↦ (℩𝑎𝑑𝐴 (𝑓 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑓) = (𝑒 ↾ suc 𝑓)) ∧ (𝑑𝑓) = 𝑎)))) ∪ ((suc ( bday 𝐵) ∖ dom if(∃𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏, ((𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏) ∪ {⟨dom (𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏), 2o⟩}), (𝑓 ∈ {𝑏 ∣ ∃𝑑𝐴 (𝑏 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑏) = (𝑒 ↾ suc 𝑏)))} ↦ (℩𝑎𝑑𝐴 (𝑓 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑓) = (𝑒 ↾ suc 𝑓)) ∧ (𝑑𝑓) = 𝑎))))) × {1o})) = (if(∃𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏, ((𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏) ∪ {⟨dom (𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏), 2o⟩}), (𝑓 ∈ {𝑏 ∣ ∃𝑑𝐴 (𝑏 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑏) = (𝑒 ↾ suc 𝑏)))} ↦ (℩𝑎𝑑𝐴 (𝑓 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑓) = (𝑒 ↾ suc 𝑓)) ∧ (𝑑𝑓) = 𝑎)))) ∪ ((suc ( bday 𝐵) ∖ dom if(∃𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏, ((𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏) ∪ {⟨dom (𝑎𝐴𝑏𝐴 ¬ 𝑎 <s 𝑏), 2o⟩}), (𝑓 ∈ {𝑏 ∣ ∃𝑑𝐴 (𝑏 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑏) = (𝑒 ↾ suc 𝑏)))} ↦ (℩𝑎𝑑𝐴 (𝑓 ∈ dom 𝑑 ∧ ∀𝑒𝐴𝑒 <s 𝑑 → (𝑑 ↾ suc 𝑓) = (𝑒 ↾ suc 𝑓)) ∧ (𝑑𝑓) = 𝑎))))) × {1o}))
1614, 15noetalem5 33329 1 (((𝐴 No 𝐴𝑉) ∧ (𝐵 No 𝐵𝑊) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 <s 𝑦) → ∃𝑧 No (∀𝑥𝐴 𝑥 <s 𝑧 ∧ ∀𝑦𝐵 𝑧 <s 𝑦 ∧ ( bday 𝑧) ⊆ suc ( bday “ (𝐴𝐵))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2112  {cab 2779  ∀wral 3109  ∃wrex 3110   ∖ cdif 3881   ∪ cun 3882   ⊆ wss 3884  ifcif 4428  {csn 4528  ⟨cop 4534  ∪ cuni 4803   class class class wbr 5033   ↦ cmpt 5113   × cxp 5521  dom cdm 5523   ↾ cres 5525   “ cima 5526  suc csuc 6165  ℩cio 6285  ‘cfv 6328  ℩crio 7096  1oc1o 8082  2oc2o 8083   No csur 33255
 Copyright terms: Public domain W3C validator