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	⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) ∧ ( 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ) → ∃ 𝑧 ∈ No ( ∀ 𝑥 ∈ 𝐴 𝑥 <s 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 𝑧 <s 𝑦 ∧ ( bday ‘ 𝑧 ) ⊆ 𝑂 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ 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 ℎ ) ) ∧ ( 𝑗 ‘ ℎ ) = 𝑓 ) ) ) )
2	1	nosupcbv	⊢ 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 𝑐 ) ) ∧ ( 𝑑 ‘ 𝑐 ) = 𝑎 ) ) ) )
3		eqid	⊢ if ( ∃ 𝑓 ∈ 𝐵 ∀ 𝑔 ∈ 𝐵 ¬ 𝑔 <s 𝑓 , ( ( ℩ 𝑓 ∈ 𝐵 ∀ 𝑔 ∈ 𝐵 ¬ 𝑔 <s 𝑓 ) ∪ { ⟨ dom ( ℩ 𝑓 ∈ 𝐵 ∀ 𝑔 ∈ 𝐵 ¬ 𝑔 <s 𝑓 ) , 1o ⟩ } ) , ( ℎ ∈ { 𝑔 ∣ ∃ 𝑗 ∈ 𝐵 ( 𝑔 ∈ dom 𝑗 ∧ ∀ 𝑘 ∈ 𝐵 ( ¬ 𝑗 <s 𝑘 → ( 𝑗 ↾ suc 𝑔 ) = ( 𝑘 ↾ suc 𝑔 ) ) ) } ↦ ( ℩ 𝑓 ∃ 𝑗 ∈ 𝐵 ( ℎ ∈ dom 𝑗 ∧ ∀ 𝑘 ∈ 𝐵 ( ¬ 𝑗 <s 𝑘 → ( 𝑗 ↾ suc ℎ ) = ( 𝑘 ↾ suc ℎ ) ) ∧ ( 𝑗 ‘ ℎ ) = 𝑓 ) ) ) ) = if ( ∃ 𝑓 ∈ 𝐵 ∀ 𝑔 ∈ 𝐵 ¬ 𝑔 <s 𝑓 , ( ( ℩ 𝑓 ∈ 𝐵 ∀ 𝑔 ∈ 𝐵 ¬ 𝑔 <s 𝑓 ) ∪ { ⟨ dom ( ℩ 𝑓 ∈ 𝐵 ∀ 𝑔 ∈ 𝐵 ¬ 𝑔 <s 𝑓 ) , 1o ⟩ } ) , ( ℎ ∈ { 𝑔 ∣ ∃ 𝑗 ∈ 𝐵 ( 𝑔 ∈ dom 𝑗 ∧ ∀ 𝑘 ∈ 𝐵 ( ¬ 𝑗 <s 𝑘 → ( 𝑗 ↾ suc 𝑔 ) = ( 𝑘 ↾ suc 𝑔 ) ) ) } ↦ ( ℩ 𝑓 ∃ 𝑗 ∈ 𝐵 ( ℎ ∈ dom 𝑗 ∧ ∀ 𝑘 ∈ 𝐵 ( ¬ 𝑗 <s 𝑘 → ( 𝑗 ↾ suc ℎ ) = ( 𝑘 ↾ suc ℎ ) ) ∧ ( 𝑗 ‘ ℎ ) = 𝑓 ) ) ) )
4	3	noinfcbv	⊢ if ( ∃ 𝑓 ∈ 𝐵 ∀ 𝑔 ∈ 𝐵 ¬ 𝑔 <s 𝑓 , ( ( ℩ 𝑓 ∈ 𝐵 ∀ 𝑔 ∈ 𝐵 ¬ 𝑔 <s 𝑓 ) ∪ { ⟨ dom ( ℩ 𝑓 ∈ 𝐵 ∀ 𝑔 ∈ 𝐵 ¬ 𝑔 <s 𝑓 ) , 1o ⟩ } ) , ( ℎ ∈ { 𝑔 ∣ ∃ 𝑗 ∈ 𝐵 ( 𝑔 ∈ dom 𝑗 ∧ ∀ 𝑘 ∈ 𝐵 ( ¬ 𝑗 <s 𝑘 → ( 𝑗 ↾ suc 𝑔 ) = ( 𝑘 ↾ suc 𝑔 ) ) ) } ↦ ( ℩ 𝑓 ∃ 𝑗 ∈ 𝐵 ( ℎ ∈ dom 𝑗 ∧ ∀ 𝑘 ∈ 𝐵 ( ¬ 𝑗 <s 𝑘 → ( 𝑗 ↾ suc ℎ ) = ( 𝑘 ↾ suc ℎ ) ) ∧ ( 𝑗 ‘ ℎ ) = 𝑓 ) ) ) ) = if ( ∃ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ¬ 𝑏 <s 𝑎 , ( ( ℩ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ¬ 𝑏 <s 𝑎 ) ∪ { ⟨ dom ( ℩ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ¬ 𝑏 <s 𝑎 ) , 1o ⟩ } ) , ( 𝑐 ∈ { 𝑏 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑏 ∈ dom 𝑑 ∧ ∀ 𝑒 ∈ 𝐵 ( ¬ 𝑑 <s 𝑒 → ( 𝑑 ↾ suc 𝑏 ) = ( 𝑒 ↾ suc 𝑏 ) ) ) } ↦ ( ℩ 𝑎 ∃ 𝑑 ∈ 𝐵 ( 𝑐 ∈ dom 𝑑 ∧ ∀ 𝑒 ∈ 𝐵 ( ¬ 𝑑 <s 𝑒 → ( 𝑑 ↾ suc 𝑐 ) = ( 𝑒 ↾ suc 𝑐 ) ) ∧ ( 𝑑 ‘ 𝑐 ) = 𝑎 ) ) ) )
5	2 4	noetalem2	⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) ∧ ( 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ) → ∃ 𝑧 ∈ No ( ∀ 𝑥 ∈ 𝐴 𝑥 <s 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 𝑧 <s 𝑦 ∧ ( bday ‘ 𝑧 ) ⊆ 𝑂 ) )