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 ( E. x e. A A. y e. A -. x . } ) , ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
nosupinfsep.2 
|- T = if ( E. x e. B A. y e. B -. y . } ) , ( g e. { y | E. u e. B ( y e. dom u /\ A. v e. B ( -. u  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. B ( g e. dom u /\ A. v e. B ( -. u  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
Assertion nosupinfsep 
|- ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ W e. No ) -> ( ( A. a e. A a  ( A. a e. A a

Proof

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