Metamath Proof Explorer

Theorem ssltmul2

Description: One surreal set less-than relationship for cuts of A and B . (Contributed by Scott Fenton, 7-Mar-2025)

Ref Expression
Hypotheses ssltmul2.1 
|- ( ph -> L <
ssltmul2.2 
|- ( ph -> M <
ssltmul2.3 
|- ( ph -> A = ( L |s R ) )
ssltmul2.4 
|- ( ph -> B = ( M |s S ) )
Assertion ssltmul2 
|- ( ph -> { ( A x.s B ) } <

Proof

Step Hyp Ref Expression
1 ssltmul2.1 
 |-  ( ph -> L <
2 ssltmul2.2 
 |-  ( ph -> M <
3 ssltmul2.3 
 |-  ( ph -> A = ( L |s R ) )
4 ssltmul2.4 
 |-  ( ph -> B = ( M |s S ) )
5 snex 
 |-  { ( A x.s B ) } e. _V
6 5 a1i 
 |-  ( ph -> { ( A x.s B ) } e. _V )
7 eqid 
 |-  ( t e. L , u e. S |-> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) = ( t e. L , u e. S |-> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) )
8 7 rnmpo 
 |-  ran ( t e. L , u e. S |-> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) = { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) }
9 ssltex1 
 |-  ( L < L e. _V )
10 1 9 syl 
 |-  ( ph -> L e. _V )
11 ssltex2 
 |-  ( M < S e. _V )
12 2 11 syl 
 |-  ( ph -> S e. _V )
13 7 mpoexg 
 |-  ( ( L e. _V /\ S e. _V ) -> ( t e. L , u e. S |-> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) e. _V )
14 10 12 13 syl2anc 
 |-  ( ph -> ( t e. L , u e. S |-> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) e. _V )
15 rnexg 
 |-  ( ( t e. L , u e. S |-> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) e. _V -> ran ( t e. L , u e. S |-> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) e. _V )
16 14 15 syl 
 |-  ( ph -> ran ( t e. L , u e. S |-> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) e. _V )
17 8 16 eqeltrrid 
 |-  ( ph -> { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } e. _V )
18 eqid 
 |-  ( v e. R , w e. M |-> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) = ( v e. R , w e. M |-> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) )
19 18 rnmpo 
 |-  ran ( v e. R , w e. M |-> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) = { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) }
20 ssltex2 
 |-  ( L < R e. _V )
21 1 20 syl 
 |-  ( ph -> R e. _V )
22 ssltex1 
 |-  ( M < M e. _V )
23 2 22 syl 
 |-  ( ph -> M e. _V )
24 18 mpoexg 
 |-  ( ( R e. _V /\ M e. _V ) -> ( v e. R , w e. M |-> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) e. _V )
25 21 23 24 syl2anc 
 |-  ( ph -> ( v e. R , w e. M |-> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) e. _V )
26 rnexg 
 |-  ( ( v e. R , w e. M |-> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) e. _V -> ran ( v e. R , w e. M |-> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) e. _V )
27 25 26 syl 
 |-  ( ph -> ran ( v e. R , w e. M |-> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) e. _V )
28 19 27 eqeltrrid 
 |-  ( ph -> { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } e. _V )
29 17 28 unexd 
 |-  ( ph -> ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) e. _V )
30 1 scutcld 
 |-  ( ph -> ( L |s R ) e. No )
31 3 30 eqeltrd 
 |-  ( ph -> A e. No )
32 2 scutcld 
 |-  ( ph -> ( M |s S ) e. No )
33 4 32 eqeltrd 
 |-  ( ph -> B e. No )
34 31 33 mulscld 
 |-  ( ph -> ( A x.s B ) e. No )
35 34 snssd 
 |-  ( ph -> { ( A x.s B ) } C_ No )
36 ssltss1 
 |-  ( L < L C_ No )
37 1 36 syl 
 |-  ( ph -> L C_ No )
38 37 adantr 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> L C_ No )
39 simprl 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> t e. L )
40 38 39 sseldd 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> t e. No )
41 33 adantr 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> B e. No )
42 40 41 mulscld 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> ( t x.s B ) e. No )
43 31 adantr 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> A e. No )
44 ssltss2 
 |-  ( M < S C_ No )
45 2 44 syl 
 |-  ( ph -> S C_ No )
46 45 adantr 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> S C_ No )
47 simprr 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> u e. S )
48 46 47 sseldd 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> u e. No )
49 43 48 mulscld 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> ( A x.s u ) e. No )
50 42 49 addscld 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> ( ( t x.s B ) +s ( A x.s u ) ) e. No )
51 40 48 mulscld 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> ( t x.s u ) e. No )
52 50 51 subscld 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) e. No )
53 eleq1 
 |-  ( c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( c e. No <-> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) e. No ) )
54 52 53 syl5ibrcom 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> ( c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> c e. No ) )
55 54 rexlimdvva 
 |-  ( ph -> ( E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> c e. No ) )
56 55 abssdv 
 |-  ( ph -> { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } C_ No )
57 ssltss2 
 |-  ( L < R C_ No )
58 1 57 syl 
 |-  ( ph -> R C_ No )
59 58 adantr 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> R C_ No )
60 simprl 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> v e. R )
61 59 60 sseldd 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> v e. No )
62 33 adantr 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> B e. No )
63 61 62 mulscld 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> ( v x.s B ) e. No )
64 31 adantr 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> A e. No )
65 ssltss1 
 |-  ( M < M C_ No )
66 2 65 syl 
 |-  ( ph -> M C_ No )
67 66 adantr 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> M C_ No )
68 simprr 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> w e. M )
69 67 68 sseldd 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> w e. No )
70 64 69 mulscld 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> ( A x.s w ) e. No )
71 63 70 addscld 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> ( ( v x.s B ) +s ( A x.s w ) ) e. No )
72 61 69 mulscld 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> ( v x.s w ) e. No )
73 71 72 subscld 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) e. No )
74 eleq1 
 |-  ( d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( d e. No <-> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) e. No ) )
75 73 74 syl5ibrcom 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> ( d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> d e. No ) )
76 75 rexlimdvva 
 |-  ( ph -> ( E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> d e. No ) )
77 76 abssdv 
 |-  ( ph -> { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } C_ No )
78 56 77 unssd 
 |-  ( ph -> ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) C_ No )
79 elun 
 |-  ( y e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) <-> ( y e. { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } \/ y e. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) )
80 vex 
 |-  y e. _V
81 eqeq1 
 |-  ( c = y -> ( c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <-> y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) )
82 81 2rexbidv 
 |-  ( c = y -> ( E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <-> E. t e. L E. u e. S y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) )
83 80 82 elab 
 |-  ( y e. { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } <-> E. t e. L E. u e. S y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) )
84 eqeq1 
 |-  ( d = y -> ( d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <-> y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) )
85 84 2rexbidv 
 |-  ( d = y -> ( E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <-> E. v e. R E. w e. M y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) )
86 80 85 elab 
 |-  ( y e. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } <-> E. v e. R E. w e. M y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) )
87 83 86 orbi12i 
 |-  ( ( y e. { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } \/ y e. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) <-> ( E. t e. L E. u e. S y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) \/ E. v e. R E. w e. M y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) )
88 79 87 bitri 
 |-  ( y e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) <-> ( E. t e. L E. u e. S y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) \/ E. v e. R E. w e. M y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) )
89 scutcut 
 |-  ( L < ( ( L |s R ) e. No /\ L <
90 1 89 syl 
 |-  ( ph -> ( ( L |s R ) e. No /\ L <
91 90 simp2d 
 |-  ( ph -> L <
92 91 adantr 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> L <
93 ovex 
 |-  ( L |s R ) e. _V
94 93 snid 
 |-  ( L |s R ) e. { ( L |s R ) }
95 3 94 eqeltrdi 
 |-  ( ph -> A e. { ( L |s R ) } )
96 95 adantr 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> A e. { ( L |s R ) } )
97 92 39 96 ssltsepcd 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> t
98 scutcut 
 |-  ( M < ( ( M |s S ) e. No /\ M <
99 2 98 syl 
 |-  ( ph -> ( ( M |s S ) e. No /\ M <
100 99 simp3d 
 |-  ( ph -> { ( M |s S ) } <
101 100 adantr 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> { ( M |s S ) } <
102 ovex 
 |-  ( M |s S ) e. _V
103 102 snid 
 |-  ( M |s S ) e. { ( M |s S ) }
104 4 103 eqeltrdi 
 |-  ( ph -> B e. { ( M |s S ) } )
105 104 adantr 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> B e. { ( M |s S ) } )
106 101 105 47 ssltsepcd 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> B
107 40 43 41 48 97 106 sltmuld 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> ( ( t x.s u ) -s ( t x.s B ) )
108 34 adantr 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> ( A x.s B ) e. No )
109 51 42 49 108 sltsubsub2bd 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> ( ( ( t x.s u ) -s ( t x.s B ) )  ( ( A x.s B ) -s ( A x.s u ) )
110 42 51 subscld 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> ( ( t x.s B ) -s ( t x.s u ) ) e. No )
111 108 49 110 sltsubaddd 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> ( ( ( A x.s B ) -s ( A x.s u ) )  ( A x.s B )
112 109 111 bitrd 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> ( ( ( t x.s u ) -s ( t x.s B ) )  ( A x.s B )
113 107 112 mpbid 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> ( A x.s B )
114 42 49 51 addsubsd 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) = ( ( ( t x.s B ) -s ( t x.s u ) ) +s ( A x.s u ) ) )
115 113 114 breqtrrd 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> ( A x.s B )
116 breq2 
 |-  ( y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( ( A x.s B )  ( A x.s B )
117 115 116 syl5ibrcom 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> ( y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( A x.s B )
118 117 rexlimdvva 
 |-  ( ph -> ( E. t e. L E. u e. S y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( A x.s B )
119 90 simp3d 
 |-  ( ph -> { ( L |s R ) } <
120 119 adantr 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> { ( L |s R ) } <
121 95 adantr 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> A e. { ( L |s R ) } )
122 120 121 60 ssltsepcd 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> A
123 99 simp2d 
 |-  ( ph -> M <
124 123 adantr 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> M <
125 104 adantr 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> B e. { ( M |s S ) } )
126 124 68 125 ssltsepcd 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> w
127 64 61 69 62 122 126 sltmuld 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> ( ( A x.s B ) -s ( A x.s w ) )
128 34 adantr 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> ( A x.s B ) e. No )
129 63 72 subscld 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> ( ( v x.s B ) -s ( v x.s w ) ) e. No )
130 128 70 129 sltsubaddd 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> ( ( ( A x.s B ) -s ( A x.s w ) )  ( A x.s B )
131 127 130 mpbid 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> ( A x.s B )
132 63 70 72 addsubsd 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) = ( ( ( v x.s B ) -s ( v x.s w ) ) +s ( A x.s w ) ) )
133 131 132 breqtrrd 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> ( A x.s B )
134 breq2 
 |-  ( y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( ( A x.s B )  ( A x.s B )
135 133 134 syl5ibrcom 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> ( y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( A x.s B )
136 135 rexlimdvva 
 |-  ( ph -> ( E. v e. R E. w e. M y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( A x.s B )
137 118 136 jaod 
 |-  ( ph -> ( ( E. t e. L E. u e. S y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) \/ E. v e. R E. w e. M y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) -> ( A x.s B )
138 88 137 biimtrid 
 |-  ( ph -> ( y e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) -> ( A x.s B )
139 velsn 
 |-  ( x e. { ( A x.s B ) } <-> x = ( A x.s B ) )
140 breq1 
 |-  ( x = ( A x.s B ) -> ( x  ( A x.s B )
141 140 imbi2d 
 |-  ( x = ( A x.s B ) -> ( ( y e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) -> x  ( y e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) -> ( A x.s B )
142 139 141 sylbi 
 |-  ( x e. { ( A x.s B ) } -> ( ( y e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) -> x  ( y e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) -> ( A x.s B )
143 138 142 syl5ibrcom 
 |-  ( ph -> ( x e. { ( A x.s B ) } -> ( y e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) -> x
144 143 3imp 
 |-  ( ( ph /\ x e. { ( A x.s B ) } /\ y e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) -> x
145 6 29 35 78 144 ssltd 
 |-  ( ph -> { ( A x.s B ) } <