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