Metamath Proof Explorer

Theorem nosepssdm

Description: Given two non-equal surreals, their separator is less than or equal to the domain of one of them. Part of Lemma 2.1.1 of Lipparini p. 3. (Contributed by Scott Fenton, 6-Dec-2021)

Ref Expression
Assertion nosepssdm 
|- ( ( A e. No /\ B e. No /\ A =/= B ) -> |^| { x e. On | ( A ` x ) =/= ( B ` x ) } C_ dom A )

Proof

Step Hyp Ref Expression
1 nosepne 
 |-  ( ( A e. No /\ B e. No /\ A =/= B ) -> ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) =/= ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) )
2 1 neneqd 
 |-  ( ( A e. No /\ B e. No /\ A =/= B ) -> -. ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) )
3 nodmord 
 |-  ( A e. No -> Ord dom A )
4 3 3ad2ant1 
 |-  ( ( A e. No /\ B e. No /\ A =/= B ) -> Ord dom A )
5 ordn2lp 
 |-  ( Ord dom A -> -. ( dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } /\ |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom A ) )
6 4 5 syl 
 |-  ( ( A e. No /\ B e. No /\ A =/= B ) -> -. ( dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } /\ |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom A ) )
7 imnan 
 |-  ( ( dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } -> -. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom A ) <-> -. ( dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } /\ |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom A ) )
8 6 7 sylibr 
 |-  ( ( A e. No /\ B e. No /\ A =/= B ) -> ( dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } -> -. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom A ) )
9 8 imp 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> -. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom A )
10 ndmfv 
 |-  ( -. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom A -> ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) )
11 9 10 syl 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) )
12 nosepeq 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> ( A ` dom A ) = ( B ` dom A ) )
13 simpl1 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> A e. No )
14 13 3 syl 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> Ord dom A )
15 ordirr 
 |-  ( Ord dom A -> -. dom A e. dom A )
16 ndmfv 
 |-  ( -. dom A e. dom A -> ( A ` dom A ) = (/) )
17 14 15 16 3syl 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> ( A ` dom A ) = (/) )
18 17 eqeq1d 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> ( ( A ` dom A ) = ( B ` dom A ) <-> (/) = ( B ` dom A ) ) )
19 eqcom 
 |-  ( (/) = ( B ` dom A ) <-> ( B ` dom A ) = (/) )
20 18 19 bitrdi 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> ( ( A ` dom A ) = ( B ` dom A ) <-> ( B ` dom A ) = (/) ) )
21 simpl2 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> B e. No )
22 nofun 
 |-  ( B e. No -> Fun B )
23 21 22 syl 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> Fun B )
24 nosgnn0 
 |-  -. (/) e. { 1o , 2o }
25 norn 
 |-  ( B e. No -> ran B C_ { 1o , 2o } )
26 21 25 syl 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> ran B C_ { 1o , 2o } )
27 26 sseld 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> ( (/) e. ran B -> (/) e. { 1o , 2o } ) )
28 24 27 mtoi 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> -. (/) e. ran B )
29 funeldmb 
 |-  ( ( Fun B /\ -. (/) e. ran B ) -> ( dom A e. dom B <-> ( B ` dom A ) =/= (/) ) )
30 23 28 29 syl2anc 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> ( dom A e. dom B <-> ( B ` dom A ) =/= (/) ) )
31 30 necon2bbid 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> ( ( B ` dom A ) = (/) <-> -. dom A e. dom B ) )
32 nodmord 
 |-  ( B e. No -> Ord dom B )
33 32 3ad2ant2 
 |-  ( ( A e. No /\ B e. No /\ A =/= B ) -> Ord dom B )
34 ordtr1 
 |-  ( Ord dom B -> ( ( dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } /\ |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom B ) -> dom A e. dom B ) )
35 33 34 syl 
 |-  ( ( A e. No /\ B e. No /\ A =/= B ) -> ( ( dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } /\ |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom B ) -> dom A e. dom B ) )
36 35 expdimp 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> ( |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom B -> dom A e. dom B ) )
37 36 con3d 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> ( -. dom A e. dom B -> -. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom B ) )
38 31 37 sylbid 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> ( ( B ` dom A ) = (/) -> -. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom B ) )
39 20 38 sylbid 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> ( ( A ` dom A ) = ( B ` dom A ) -> -. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom B ) )
40 12 39 mpd 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> -. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom B )
41 ndmfv 
 |-  ( -. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom B -> ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) )
42 40 41 syl 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) )
43 11 42 eqtr4d 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) )
44 2 43 mtand 
 |-  ( ( A e. No /\ B e. No /\ A =/= B ) -> -. dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } )
45 nosepon 
 |-  ( ( A e. No /\ B e. No /\ A =/= B ) -> |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. On )
46 nodmon 
 |-  ( A e. No -> dom A e. On )
47 46 3ad2ant1 
 |-  ( ( A e. No /\ B e. No /\ A =/= B ) -> dom A e. On )
48 ontri1 
 |-  ( ( |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. On /\ dom A e. On ) -> ( |^| { x e. On | ( A ` x ) =/= ( B ` x ) } C_ dom A <-> -. dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) )
49 45 47 48 syl2anc 
 |-  ( ( A e. No /\ B e. No /\ A =/= B ) -> ( |^| { x e. On | ( A ` x ) =/= ( B ` x ) } C_ dom A <-> -. dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) )
50 44 49 mpbird 
 |-  ( ( A e. No /\ B e. No /\ A =/= B ) -> |^| { x e. On | ( A ` x ) =/= ( B ` x ) } C_ dom A )