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 S = if x A y A ¬ x < s y ι x A | y A ¬ x < s y dom ι x A | y A ¬ x < s y 2 𝑜 g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x
nosupinfsep.2 T = if x B y B ¬ y < s x ι x B | y B ¬ y < s x dom ι x B | y B ¬ y < s x 1 𝑜 g y | u B y dom u v B ¬ u < s v u suc y = v suc y ι x | u B g dom u v B ¬ u < s v u suc g = v suc g u g = x
Assertion nosupinfsep A No A V B No B V W No a A a < s W b B W < s b a A a < s W dom S dom T b B W dom S dom T < s b

Proof

Step Hyp Ref Expression
1 nosupinfsep.1 S = if x A y A ¬ x < s y ι x A | y A ¬ x < s y dom ι x A | y A ¬ x < s y 2 𝑜 g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x
2 nosupinfsep.2 T = if x B y B ¬ y < s x ι x B | y B ¬ y < s x dom ι x B | y B ¬ y < s x 1 𝑜 g y | u B y dom u v B ¬ u < s v u suc y = v suc y ι x | u B g dom u v B ¬ u < s v u suc g = v suc g u g = x
3 ssun1 dom S dom S dom T
4 resabs1 dom S dom S dom T W dom S dom T dom S = W dom S
5 3 4 ax-mp W dom S dom T dom S = W dom S
6 5 breq1i W dom S dom T dom S < s S W dom S < s S
7 6 notbii ¬ W dom S dom T dom S < s S ¬ W dom S < s S
8 ssun2 dom T dom S dom T
9 resabs1 dom T dom S dom T W dom S dom T dom T = W dom T
10 8 9 ax-mp W dom S dom T dom T = W dom T
11 10 breq2i T < s W dom S dom T dom T T < s W dom T
12 11 notbii ¬ T < s W dom S dom T dom T ¬ T < s W dom T
13 7 12 anbi12i ¬ W dom S dom T dom S < s S ¬ T < s W dom S dom T dom T ¬ W dom S < s S ¬ T < s W dom T
14 13 bicomi ¬ W dom S < s S ¬ T < s W dom T ¬ W dom S dom T dom S < s S ¬ T < s W dom S dom T dom T
15 14 a1i A No A V B No B V W No ¬ W dom S < s S ¬ T < s W dom T ¬ W dom S dom T dom S < s S ¬ T < s W dom S dom T dom T
16 simp1l A No A V B No B V W No A No
17 simp1r A No A V B No B V W No A V
18 simp3 A No A V B No B V W No W No
19 1 nosupbnd2 A No A V W No a A a < s W ¬ W dom S < s S
20 16 17 18 19 syl3anc A No A V B No B V W No a A a < s W ¬ W dom S < s S
21 simp2l A No A V B No B V W No B No
22 simp2r A No A V B No B V W No B V
23 2 noinfbnd2 B No B V W No b B W < s b ¬ T < s W dom T
24 21 22 18 23 syl3anc A No A V B No B V W No b B W < s b ¬ T < s W dom T
25 20 24 anbi12d A No A V B No B V W No a A a < s W b B W < s b ¬ W dom S < s S ¬ T < s W dom T
26 1 nosupno A No A V S No
27 nodmon S No dom S On
28 26 27 syl A No A V dom S On
29 28 3ad2ant1 A No A V B No B V W No dom S On
30 2 noinfno B No B V T No
31 nodmon T No dom T On
32 30 31 syl B No B V dom T On
33 32 3ad2ant2 A No A V B No B V W No dom T On
34 onun2 dom S On dom T On dom S dom T On
35 29 33 34 syl2anc A No A V B No B V W No dom S dom T On
36 noreson W No dom S dom T On W dom S dom T No
37 18 35 36 syl2anc A No A V B No B V W No W dom S dom T No
38 1 nosupbnd2 A No A V W dom S dom T No a A a < s W dom S dom T ¬ W dom S dom T dom S < s S
39 16 17 37 38 syl3anc A No A V B No B V W No a A a < s W dom S dom T ¬ W dom S dom T dom S < s S
40 21 22 37 3jca A No A V B No B V W No B No B V W dom S dom T No
41 2 noinfbnd2 B No B V W dom S dom T No b B W dom S dom T < s b ¬ T < s W dom S dom T dom T
42 40 41 syl A No A V B No B V W No b B W dom S dom T < s b ¬ T < s W dom S dom T dom T
43 39 42 anbi12d A No A V B No B V W No a A a < s W dom S dom T b B W dom S dom T < s b ¬ W dom S dom T dom S < s S ¬ T < s W dom S dom T dom T
44 15 25 43 3bitr4d A No A V B No B V W No a A a < s W b B W < s b a A a < s W dom S dom T b B W dom S dom T < s b