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 ordirr 
 |-  ( Ord dom A -> -. dom A e. dom A )
15 ndmfv 
 |-  ( -. dom A e. dom A -> ( A ` dom A ) = (/) )
16 13 3 14 15 4syl 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> ( A ` dom A ) = (/) )
17 16 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 ) ) )
18 eqcom 
 |-  ( (/) = ( B ` dom A ) <-> ( B ` dom A ) = (/) )
19 17 18 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 ) = (/) ) )
20 simpl2 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> B e. No )
21 nofun 
 |-  ( B e. No -> Fun B )
22 20 21 syl 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> Fun B )
23 nosgnn0 
 |-  -. (/) e. { 1o , 2o }
24 norn 
 |-  ( B e. No -> ran B C_ { 1o , 2o } )
25 20 24 syl 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> ran B C_ { 1o , 2o } )
26 25 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 } ) )
27 23 26 mtoi 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> -. (/) e. ran B )
28 funeldmb 
 |-  ( ( Fun B /\ -. (/) e. ran B ) -> ( dom A e. dom B <-> ( B ` dom A ) =/= (/) ) )
29 22 27 28 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 ) =/= (/) ) )
30 29 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 ) )
31 nodmord 
 |-  ( B e. No -> Ord dom B )
32 31 3ad2ant2 
 |-  ( ( A e. No /\ B e. No /\ A =/= B ) -> Ord dom B )
33 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 ) )
34 32 33 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 ) )
35 34 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 ) )
36 35 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 ) )
37 30 36 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 ) )
38 19 37 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 ) )
39 12 38 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 )
40 ndmfv 
 |-  ( -. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom B -> ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) )
41 39 40 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 ) } ) = (/) )
42 11 41 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 ) } ) )
43 2 42 mtand 
 |-  ( ( A e. No /\ B e. No /\ A =/= B ) -> -. dom A e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } )
44 nosepon 
 |-  ( ( A e. No /\ B e. No /\ A =/= B ) -> |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. On )
45 nodmon 
 |-  ( A e. No -> dom A e. On )
46 45 3ad2ant1 
 |-  ( ( A e. No /\ B e. No /\ A =/= B ) -> dom A e. On )
47 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 ) } ) )
48 44 46 47 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 ) } ) )
49 43 48 mpbird 
 |-  ( ( A e. No /\ B e. No /\ A =/= B ) -> |^| { x e. On | ( A ` x ) =/= ( B ` x ) } C_ dom A )