Metamath Proof Explorer


Theorem nosupinfsep

Description: Given two sets of surreals, a surreal W separates them iff its restriction to the maximum of dom S and dom T separates them. Corollary 4.4 of Lipparini p. 7. (Contributed by Scott Fenton, 9-Aug-2024)

Ref Expression
Hypotheses nosupinfsep.1 𝑆 = if ( ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 , ( ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) )
nosupinfsep.2 𝑇 = if ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 , ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) )
Assertion nosupinfsep ( ( ( 𝐴 No 𝐴 ∈ V ) ∧ ( 𝐵 No 𝐵 ∈ V ) ∧ 𝑊 No ) → ( ( ∀ 𝑎𝐴 𝑎 <s 𝑊 ∧ ∀ 𝑏𝐵 𝑊 <s 𝑏 ) ↔ ( ∀ 𝑎𝐴 𝑎 <s ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ∧ ∀ 𝑏𝐵 ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) <s 𝑏 ) ) )

Proof

Step Hyp Ref Expression
1 nosupinfsep.1 𝑆 = if ( ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 , ( ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) )
2 nosupinfsep.2 𝑇 = if ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 , ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) )
3 ssun1 dom 𝑆 ⊆ ( dom 𝑆 ∪ dom 𝑇 )
4 resabs1 ( dom 𝑆 ⊆ ( dom 𝑆 ∪ dom 𝑇 ) → ( ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ↾ dom 𝑆 ) = ( 𝑊 ↾ dom 𝑆 ) )
5 3 4 ax-mp ( ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ↾ dom 𝑆 ) = ( 𝑊 ↾ dom 𝑆 )
6 5 breq1i ( ( ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ↾ dom 𝑆 ) <s 𝑆 ↔ ( 𝑊 ↾ dom 𝑆 ) <s 𝑆 )
7 6 notbii ( ¬ ( ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ↾ dom 𝑆 ) <s 𝑆 ↔ ¬ ( 𝑊 ↾ dom 𝑆 ) <s 𝑆 )
8 ssun2 dom 𝑇 ⊆ ( dom 𝑆 ∪ dom 𝑇 )
9 resabs1 ( dom 𝑇 ⊆ ( dom 𝑆 ∪ dom 𝑇 ) → ( ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ↾ dom 𝑇 ) = ( 𝑊 ↾ dom 𝑇 ) )
10 8 9 ax-mp ( ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ↾ dom 𝑇 ) = ( 𝑊 ↾ dom 𝑇 )
11 10 breq2i ( 𝑇 <s ( ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ↾ dom 𝑇 ) ↔ 𝑇 <s ( 𝑊 ↾ dom 𝑇 ) )
12 11 notbii ( ¬ 𝑇 <s ( ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ↾ dom 𝑇 ) ↔ ¬ 𝑇 <s ( 𝑊 ↾ dom 𝑇 ) )
13 7 12 anbi12i ( ( ¬ ( ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ↾ dom 𝑆 ) <s 𝑆 ∧ ¬ 𝑇 <s ( ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ↾ dom 𝑇 ) ) ↔ ( ¬ ( 𝑊 ↾ dom 𝑆 ) <s 𝑆 ∧ ¬ 𝑇 <s ( 𝑊 ↾ dom 𝑇 ) ) )
14 13 bicomi ( ( ¬ ( 𝑊 ↾ dom 𝑆 ) <s 𝑆 ∧ ¬ 𝑇 <s ( 𝑊 ↾ dom 𝑇 ) ) ↔ ( ¬ ( ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ↾ dom 𝑆 ) <s 𝑆 ∧ ¬ 𝑇 <s ( ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ↾ dom 𝑇 ) ) )
15 14 a1i ( ( ( 𝐴 No 𝐴 ∈ V ) ∧ ( 𝐵 No 𝐵 ∈ V ) ∧ 𝑊 No ) → ( ( ¬ ( 𝑊 ↾ dom 𝑆 ) <s 𝑆 ∧ ¬ 𝑇 <s ( 𝑊 ↾ dom 𝑇 ) ) ↔ ( ¬ ( ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ↾ dom 𝑆 ) <s 𝑆 ∧ ¬ 𝑇 <s ( ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ↾ dom 𝑇 ) ) ) )
16 simp1l ( ( ( 𝐴 No 𝐴 ∈ V ) ∧ ( 𝐵 No 𝐵 ∈ V ) ∧ 𝑊 No ) → 𝐴 No )
17 simp1r ( ( ( 𝐴 No 𝐴 ∈ V ) ∧ ( 𝐵 No 𝐵 ∈ V ) ∧ 𝑊 No ) → 𝐴 ∈ V )
18 simp3 ( ( ( 𝐴 No 𝐴 ∈ V ) ∧ ( 𝐵 No 𝐵 ∈ V ) ∧ 𝑊 No ) → 𝑊 No )
19 1 nosupbnd2 ( ( 𝐴 No 𝐴 ∈ V ∧ 𝑊 No ) → ( ∀ 𝑎𝐴 𝑎 <s 𝑊 ↔ ¬ ( 𝑊 ↾ dom 𝑆 ) <s 𝑆 ) )
20 16 17 18 19 syl3anc ( ( ( 𝐴 No 𝐴 ∈ V ) ∧ ( 𝐵 No 𝐵 ∈ V ) ∧ 𝑊 No ) → ( ∀ 𝑎𝐴 𝑎 <s 𝑊 ↔ ¬ ( 𝑊 ↾ dom 𝑆 ) <s 𝑆 ) )
21 simp2l ( ( ( 𝐴 No 𝐴 ∈ V ) ∧ ( 𝐵 No 𝐵 ∈ V ) ∧ 𝑊 No ) → 𝐵 No )
22 simp2r ( ( ( 𝐴 No 𝐴 ∈ V ) ∧ ( 𝐵 No 𝐵 ∈ V ) ∧ 𝑊 No ) → 𝐵 ∈ V )
23 2 noinfbnd2 ( ( 𝐵 No 𝐵 ∈ V ∧ 𝑊 No ) → ( ∀ 𝑏𝐵 𝑊 <s 𝑏 ↔ ¬ 𝑇 <s ( 𝑊 ↾ dom 𝑇 ) ) )
24 21 22 18 23 syl3anc ( ( ( 𝐴 No 𝐴 ∈ V ) ∧ ( 𝐵 No 𝐵 ∈ V ) ∧ 𝑊 No ) → ( ∀ 𝑏𝐵 𝑊 <s 𝑏 ↔ ¬ 𝑇 <s ( 𝑊 ↾ dom 𝑇 ) ) )
25 20 24 anbi12d ( ( ( 𝐴 No 𝐴 ∈ V ) ∧ ( 𝐵 No 𝐵 ∈ V ) ∧ 𝑊 No ) → ( ( ∀ 𝑎𝐴 𝑎 <s 𝑊 ∧ ∀ 𝑏𝐵 𝑊 <s 𝑏 ) ↔ ( ¬ ( 𝑊 ↾ dom 𝑆 ) <s 𝑆 ∧ ¬ 𝑇 <s ( 𝑊 ↾ dom 𝑇 ) ) ) )
26 1 nosupno ( ( 𝐴 No 𝐴 ∈ V ) → 𝑆 No )
27 nodmon ( 𝑆 No → dom 𝑆 ∈ On )
28 26 27 syl ( ( 𝐴 No 𝐴 ∈ V ) → dom 𝑆 ∈ On )
29 28 3ad2ant1 ( ( ( 𝐴 No 𝐴 ∈ V ) ∧ ( 𝐵 No 𝐵 ∈ V ) ∧ 𝑊 No ) → dom 𝑆 ∈ On )
30 2 noinfno ( ( 𝐵 No 𝐵 ∈ V ) → 𝑇 No )
31 nodmon ( 𝑇 No → dom 𝑇 ∈ On )
32 30 31 syl ( ( 𝐵 No 𝐵 ∈ V ) → dom 𝑇 ∈ On )
33 32 3ad2ant2 ( ( ( 𝐴 No 𝐴 ∈ V ) ∧ ( 𝐵 No 𝐵 ∈ V ) ∧ 𝑊 No ) → dom 𝑇 ∈ On )
34 onun2 ( ( dom 𝑆 ∈ On ∧ dom 𝑇 ∈ On ) → ( dom 𝑆 ∪ dom 𝑇 ) ∈ On )
35 29 33 34 syl2anc ( ( ( 𝐴 No 𝐴 ∈ V ) ∧ ( 𝐵 No 𝐵 ∈ V ) ∧ 𝑊 No ) → ( dom 𝑆 ∪ dom 𝑇 ) ∈ On )
36 noreson ( ( 𝑊 No ∧ ( dom 𝑆 ∪ dom 𝑇 ) ∈ On ) → ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ∈ No )
37 18 35 36 syl2anc ( ( ( 𝐴 No 𝐴 ∈ V ) ∧ ( 𝐵 No 𝐵 ∈ V ) ∧ 𝑊 No ) → ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ∈ No )
38 1 nosupbnd2 ( ( 𝐴 No 𝐴 ∈ V ∧ ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ∈ No ) → ( ∀ 𝑎𝐴 𝑎 <s ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ↔ ¬ ( ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ↾ dom 𝑆 ) <s 𝑆 ) )
39 16 17 37 38 syl3anc ( ( ( 𝐴 No 𝐴 ∈ V ) ∧ ( 𝐵 No 𝐵 ∈ V ) ∧ 𝑊 No ) → ( ∀ 𝑎𝐴 𝑎 <s ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ↔ ¬ ( ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ↾ dom 𝑆 ) <s 𝑆 ) )
40 21 22 37 3jca ( ( ( 𝐴 No 𝐴 ∈ V ) ∧ ( 𝐵 No 𝐵 ∈ V ) ∧ 𝑊 No ) → ( 𝐵 No 𝐵 ∈ V ∧ ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ∈ No ) )
41 2 noinfbnd2 ( ( 𝐵 No 𝐵 ∈ V ∧ ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ∈ No ) → ( ∀ 𝑏𝐵 ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) <s 𝑏 ↔ ¬ 𝑇 <s ( ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ↾ dom 𝑇 ) ) )
42 40 41 syl ( ( ( 𝐴 No 𝐴 ∈ V ) ∧ ( 𝐵 No 𝐵 ∈ V ) ∧ 𝑊 No ) → ( ∀ 𝑏𝐵 ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) <s 𝑏 ↔ ¬ 𝑇 <s ( ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ↾ dom 𝑇 ) ) )
43 39 42 anbi12d ( ( ( 𝐴 No 𝐴 ∈ V ) ∧ ( 𝐵 No 𝐵 ∈ V ) ∧ 𝑊 No ) → ( ( ∀ 𝑎𝐴 𝑎 <s ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ∧ ∀ 𝑏𝐵 ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) <s 𝑏 ) ↔ ( ¬ ( ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ↾ dom 𝑆 ) <s 𝑆 ∧ ¬ 𝑇 <s ( ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ↾ dom 𝑇 ) ) ) )
44 15 25 43 3bitr4d ( ( ( 𝐴 No 𝐴 ∈ V ) ∧ ( 𝐵 No 𝐵 ∈ V ) ∧ 𝑊 No ) → ( ( ∀ 𝑎𝐴 𝑎 <s 𝑊 ∧ ∀ 𝑏𝐵 𝑊 <s 𝑏 ) ↔ ( ∀ 𝑎𝐴 𝑎 <s ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) ∧ ∀ 𝑏𝐵 ( 𝑊 ↾ ( dom 𝑆 ∪ dom 𝑇 ) ) <s 𝑏 ) ) )