Metamath Proof Explorer

Theorem ssltmul1

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

Ref Expression
Hypotheses ssltmul1.1 
|- ( ph -> L <
ssltmul1.2 
|- ( ph -> M <
ssltmul1.3 
|- ( ph -> A = ( L |s R ) )
ssltmul1.4 
|- ( ph -> B = ( M |s S ) )
Assertion ssltmul1 
|- ( ph -> ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) <

Proof

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