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 𝑏 ) ) )