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	$$⊢\phi \to L{\ll }_{s}R$$
	ssltmul2.2	$$⊢\phi \to M{\ll }_{s}S$$
	ssltmul2.3	$$⊢\phi \to A=L{|}_{s}R$$
	ssltmul2.4	$$⊢\phi \to B=M{|}_{s}S$$
Assertion	ssltmul2	Could not format assertion : No typesetting found for |- ( ph -> { ( A x.s B ) } <

Proof

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