Metamath Proof Explorer

Theorem noeta

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, if the birthdays of members of A and B are strictly bounded above by O , then O non-strictly bounds the separator. Axiom FE of Alling p. 185. (Contributed by Scott Fenton, 9-Aug-2024)

Ref Expression
Assertion noeta ⊢ A ⊆ No ∧ A ∈ V ∧ B ⊆ No ∧ B ∈ W ∧ ∀ x ∈ A ∀ y ∈ B x < s y ∧ O ∈ On ∧ bday A ∪ B ⊆ O → ∃ z ∈ No ∀ x ∈ A x < s z ∧ ∀ y ∈ B z < s y ∧ bday ⁡ z ⊆ O

Proof

Step Hyp Ref Expression
1 eqid ⊢ if ∃ f ∈ A ∀ g ∈ A ¬ f < s g ι f ∈ A | ∀ g ∈ A ¬ f < s g ∪ dom ⁡ ι f ∈ A | ∀ g ∈ A ¬ f < s g 2 𝑜 h ∈ g | ∃ j ∈ A g ∈ dom ⁡ j ∧ ∀ k ∈ A ¬ k < s j → j ↾ suc ⁡ g = k ↾ suc ⁡ g ⟼ ι f | ∃ j ∈ A h ∈ dom ⁡ j ∧ ∀ k ∈ A ¬ k < s j → j ↾ suc ⁡ h = k ↾ suc ⁡ h ∧ j ⁡ h = f = if ∃ f ∈ A ∀ g ∈ A ¬ f < s g ι f ∈ A | ∀ g ∈ A ¬ f < s g ∪ dom ⁡ ι f ∈ A | ∀ g ∈ A ¬ f < s g 2 𝑜 h ∈ g | ∃ j ∈ A g ∈ dom ⁡ j ∧ ∀ k ∈ A ¬ k < s j → j ↾ suc ⁡ g = k ↾ suc ⁡ g ⟼ ι f | ∃ j ∈ A h ∈ dom ⁡ j ∧ ∀ k ∈ A ¬ k < s j → j ↾ suc ⁡ h = k ↾ suc ⁡ h ∧ j ⁡ h = f
2 1 nosupcbv ⊢ if ∃ f ∈ A ∀ g ∈ A ¬ f < s g ι f ∈ A | ∀ g ∈ A ¬ f < s g ∪ dom ⁡ ι f ∈ A | ∀ g ∈ A ¬ f < s g 2 𝑜 h ∈ g | ∃ j ∈ A g ∈ dom ⁡ j ∧ ∀ k ∈ A ¬ k < s j → j ↾ suc ⁡ g = k ↾ suc ⁡ g ⟼ ι f | ∃ j ∈ A h ∈ dom ⁡ j ∧ ∀ k ∈ A ¬ k < s j → j ↾ suc ⁡ h = k ↾ suc ⁡ h ∧ j ⁡ h = f = if ∃ a ∈ A ∀ b ∈ A ¬ a < s b ι a ∈ A | ∀ b ∈ A ¬ a < s b ∪ dom ⁡ ι a ∈ A | ∀ b ∈ A ¬ a < s b 2 𝑜 c ∈ b | ∃ d ∈ A b ∈ dom ⁡ d ∧ ∀ e ∈ A ¬ e < s d → d ↾ suc ⁡ b = e ↾ suc ⁡ b ⟼ ι a | ∃ d ∈ A c ∈ dom ⁡ d ∧ ∀ e ∈ A ¬ e < s d → d ↾ suc ⁡ c = e ↾ suc ⁡ c ∧ d ⁡ c = a
3 eqid ⊢ if ∃ f ∈ B ∀ g ∈ B ¬ g < s f ι f ∈ B | ∀ g ∈ B ¬ g < s f ∪ dom ⁡ ι f ∈ B | ∀ g ∈ B ¬ g < s f 1 𝑜 h ∈ g | ∃ j ∈ B g ∈ dom ⁡ j ∧ ∀ k ∈ B ¬ j < s k → j ↾ suc ⁡ g = k ↾ suc ⁡ g ⟼ ι f | ∃ j ∈ B h ∈ dom ⁡ j ∧ ∀ k ∈ B ¬ j < s k → j ↾ suc ⁡ h = k ↾ suc ⁡ h ∧ j ⁡ h = f = if ∃ f ∈ B ∀ g ∈ B ¬ g < s f ι f ∈ B | ∀ g ∈ B ¬ g < s f ∪ dom ⁡ ι f ∈ B | ∀ g ∈ B ¬ g < s f 1 𝑜 h ∈ g | ∃ j ∈ B g ∈ dom ⁡ j ∧ ∀ k ∈ B ¬ j < s k → j ↾ suc ⁡ g = k ↾ suc ⁡ g ⟼ ι f | ∃ j ∈ B h ∈ dom ⁡ j ∧ ∀ k ∈ B ¬ j < s k → j ↾ suc ⁡ h = k ↾ suc ⁡ h ∧ j ⁡ h = f
4 3 noinfcbv ⊢ if ∃ f ∈ B ∀ g ∈ B ¬ g < s f ι f ∈ B | ∀ g ∈ B ¬ g < s f ∪ dom ⁡ ι f ∈ B | ∀ g ∈ B ¬ g < s f 1 𝑜 h ∈ g | ∃ j ∈ B g ∈ dom ⁡ j ∧ ∀ k ∈ B ¬ j < s k → j ↾ suc ⁡ g = k ↾ suc ⁡ g ⟼ ι f | ∃ j ∈ B h ∈ dom ⁡ j ∧ ∀ k ∈ B ¬ j < s k → j ↾ suc ⁡ h = k ↾ suc ⁡ h ∧ j ⁡ h = f = if ∃ a ∈ B ∀ b ∈ B ¬ b < s a ι a ∈ B | ∀ b ∈ B ¬ b < s a ∪ dom ⁡ ι a ∈ B | ∀ b ∈ B ¬ b < s a 1 𝑜 c ∈ b | ∃ d ∈ B b ∈ dom ⁡ d ∧ ∀ e ∈ B ¬ d < s e → d ↾ suc ⁡ b = e ↾ suc ⁡ b ⟼ ι a | ∃ d ∈ B c ∈ dom ⁡ d ∧ ∀ e ∈ B ¬ d < s e → d ↾ suc ⁡ c = e ↾ suc ⁡ c ∧ d ⁡ c = a
5 2 4 noetalem2 ⊢ A ⊆ No ∧ A ∈ V ∧ B ⊆ No ∧ B ∈ W ∧ ∀ x ∈ A ∀ y ∈ B x < s y ∧ O ∈ On ∧ bday A ∪ B ⊆ O → ∃ z ∈ No ∀ x ∈ A x < s z ∧ ∀ y ∈ B z < s y ∧ bday ⁡ z ⊆ O