Theorem addsuniflem

Description: Lemma for addsunif . State the whole theorem with extra distinct variable conditions. (Contributed by Scott Fenton, 21-Jan-2025)

	Ref	Expression
Hypotheses	addsuniflem.1	$$⊢\phi \to L{\ll }_{s}R$$
	addsuniflem.2	$$⊢\phi \to M{\ll }_{s}S$$
	addsuniflem.3	$$⊢\phi \to A=L{|}_{s}R$$
	addsuniflem.4	$$⊢\phi \to B=M{|}_{s}S$$
Assertion	addsuniflem	Could not format assertion : No typesetting found for |- ( ph -> ( A +s B ) = ( ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) |s ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		addsuniflem.1	$$⊢\phi \to L{\ll }_{s}R$$
2		addsuniflem.2	$$⊢\phi \to M{\ll }_{s}S$$
3		addsuniflem.3	$$⊢\phi \to A=L{|}_{s}R$$
4		addsuniflem.4	$$⊢\phi \to B=M{|}_{s}S$$
5	1	scutcld	$$⊢\phi \to L{|}_{s}R\in \mathrm{No}$$
6	3 5	eqeltrd	$$⊢\phi \to A\in \mathrm{No}$$
7	2	scutcld	$$⊢\phi \to M{|}_{s}S\in \mathrm{No}$$
8	4 7	eqeltrd	$$⊢\phi \to B\in \mathrm{No}$$
9		addsval2	Could not format ( ( A e. No /\ B e. No ) -> ( A +s B ) = ( ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) |s ( { c | E. e e. ( _Right ` A ) c = ( e +s B ) } u. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( A +s B ) = ( ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) |s ( { c | E. e e. ( _Right ` A ) c = ( e +s B ) } u. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } ) ) ) with typecode |-
10	6 8 9	syl2anc	Could not format ( ph -> ( A +s B ) = ( ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) |s ( { c | E. e e. ( _Right ` A ) c = ( e +s B ) } u. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } ) ) ) : No typesetting found for |- ( ph -> ( A +s B ) = ( ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) |s ( { c | E. e e. ( _Right ` A ) c = ( e +s B ) } u. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } ) ) ) with typecode |-
11	6 8	addscut	Could not format ( ph -> ( ( A +s B ) e. No /\ ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) < ( ( A +s B ) e. No /\ ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) <
12	11	simp2d	Could not format ( ph -> ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) < ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) <
13	11	simp3d	Could not format ( ph -> { ( A +s B ) } < { ( A +s B ) } <
14		ovex	Could not format ( A +s B ) e. _V : No typesetting found for |- ( A +s B ) e. _V with typecode |-
15	14	snnz	Could not format { ( A +s B ) } =/= (/) : No typesetting found for |- { ( A +s B ) } =/= (/) with typecode |-
16		sslttr	Could not format ( ( ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) < ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) < ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) <
17	15 16	mp3an3	Could not format ( ( ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) < ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) < ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) <
18	12 13 17	syl2anc	Could not format ( ph -> ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) < ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) <
19	1 3	cofcutr1d	Could not format ( ph -> A. p e. ( _Left ` A ) E. l e. L p <_s l ) : No typesetting found for |- ( ph -> A. p e. ( _Left ` A ) E. l e. L p <_s l ) with typecode |-
20		leftssno	Could not format ( _Left ` A ) C_ No : No typesetting found for |- ( _Left ` A ) C_ No with typecode |-
21	20	sseli	Could not format ( p e. ( _Left ` A ) -> p e. No ) : No typesetting found for |- ( p e. ( _Left ` A ) -> p e. No ) with typecode |-
22	21	ad2antlr	Could not format ( ( ( ph /\ p e. ( _Left ` A ) ) /\ l e. L ) -> p e. No ) : No typesetting found for |- ( ( ( ph /\ p e. ( _Left ` A ) ) /\ l e. L ) -> p e. No ) with typecode |-
23		ssltss1	$$⊢L{\ll }_{s}R\to L\subseteq \mathrm{No}$$
24	1 23	syl	$$⊢\phi \to L\subseteq \mathrm{No}$$
25	24	adantr	Could not format ( ( ph /\ p e. ( _Left ` A ) ) -> L C_ No ) : No typesetting found for |- ( ( ph /\ p e. ( _Left ` A ) ) -> L C_ No ) with typecode |-
26	25	sselda	Could not format ( ( ( ph /\ p e. ( _Left ` A ) ) /\ l e. L ) -> l e. No ) : No typesetting found for |- ( ( ( ph /\ p e. ( _Left ` A ) ) /\ l e. L ) -> l e. No ) with typecode |-
27	8	ad2antrr	Could not format ( ( ( ph /\ p e. ( _Left ` A ) ) /\ l e. L ) -> B e. No ) : No typesetting found for |- ( ( ( ph /\ p e. ( _Left ` A ) ) /\ l e. L ) -> B e. No ) with typecode |-
28	22 26 27	sleadd1d	Could not format ( ( ( ph /\ p e. ( _Left ` A ) ) /\ l e. L ) -> ( p <_s l <-> ( p +s B ) <_s ( l +s B ) ) ) : No typesetting found for |- ( ( ( ph /\ p e. ( _Left ` A ) ) /\ l e. L ) -> ( p <_s l <-> ( p +s B ) <_s ( l +s B ) ) ) with typecode |-
29	28	rexbidva	Could not format ( ( ph /\ p e. ( _Left ` A ) ) -> ( E. l e. L p <_s l <-> E. l e. L ( p +s B ) <_s ( l +s B ) ) ) : No typesetting found for |- ( ( ph /\ p e. ( _Left ` A ) ) -> ( E. l e. L p <_s l <-> E. l e. L ( p +s B ) <_s ( l +s B ) ) ) with typecode |-
30	29	ralbidva	Could not format ( ph -> ( A. p e. ( _Left ` A ) E. l e. L p <_s l <-> A. p e. ( _Left ` A ) E. l e. L ( p +s B ) <_s ( l +s B ) ) ) : No typesetting found for |- ( ph -> ( A. p e. ( _Left ` A ) E. l e. L p <_s l <-> A. p e. ( _Left ` A ) E. l e. L ( p +s B ) <_s ( l +s B ) ) ) with typecode |-
31	19 30	mpbid	Could not format ( ph -> A. p e. ( _Left ` A ) E. l e. L ( p +s B ) <_s ( l +s B ) ) : No typesetting found for |- ( ph -> A. p e. ( _Left ` A ) E. l e. L ( p +s B ) <_s ( l +s B ) ) with typecode |-
32		eqeq1	Could not format ( y = s -> ( y = ( l +s B ) <-> s = ( l +s B ) ) ) : No typesetting found for |- ( y = s -> ( y = ( l +s B ) <-> s = ( l +s B ) ) ) with typecode |-
33	32	rexbidv	Could not format ( y = s -> ( E. l e. L y = ( l +s B ) <-> E. l e. L s = ( l +s B ) ) ) : No typesetting found for |- ( y = s -> ( E. l e. L y = ( l +s B ) <-> E. l e. L s = ( l +s B ) ) ) with typecode |-
34	33	rexab	Could not format ( E. s e. { y | E. l e. L y = ( l +s B ) } ( p +s B ) <_s s <-> E. s ( E. l e. L s = ( l +s B ) /\ ( p +s B ) <_s s ) ) : No typesetting found for |- ( E. s e. { y | E. l e. L y = ( l +s B ) } ( p +s B ) <_s s <-> E. s ( E. l e. L s = ( l +s B ) /\ ( p +s B ) <_s s ) ) with typecode |-
35		rexcom4	Could not format ( E. l e. L E. s ( s = ( l +s B ) /\ ( p +s B ) <_s s ) <-> E. s E. l e. L ( s = ( l +s B ) /\ ( p +s B ) <_s s ) ) : No typesetting found for |- ( E. l e. L E. s ( s = ( l +s B ) /\ ( p +s B ) <_s s ) <-> E. s E. l e. L ( s = ( l +s B ) /\ ( p +s B ) <_s s ) ) with typecode |-
36		ovex	Could not format ( l +s B ) e. _V : No typesetting found for |- ( l +s B ) e. _V with typecode |-
37		breq2	Could not format ( s = ( l +s B ) -> ( ( p +s B ) <_s s <-> ( p +s B ) <_s ( l +s B ) ) ) : No typesetting found for |- ( s = ( l +s B ) -> ( ( p +s B ) <_s s <-> ( p +s B ) <_s ( l +s B ) ) ) with typecode |-
38	36 37	ceqsexv	Could not format ( E. s ( s = ( l +s B ) /\ ( p +s B ) <_s s ) <-> ( p +s B ) <_s ( l +s B ) ) : No typesetting found for |- ( E. s ( s = ( l +s B ) /\ ( p +s B ) <_s s ) <-> ( p +s B ) <_s ( l +s B ) ) with typecode |-
39	38	rexbii	Could not format ( E. l e. L E. s ( s = ( l +s B ) /\ ( p +s B ) <_s s ) <-> E. l e. L ( p +s B ) <_s ( l +s B ) ) : No typesetting found for |- ( E. l e. L E. s ( s = ( l +s B ) /\ ( p +s B ) <_s s ) <-> E. l e. L ( p +s B ) <_s ( l +s B ) ) with typecode |-
40		r19.41v	Could not format ( E. l e. L ( s = ( l +s B ) /\ ( p +s B ) <_s s ) <-> ( E. l e. L s = ( l +s B ) /\ ( p +s B ) <_s s ) ) : No typesetting found for |- ( E. l e. L ( s = ( l +s B ) /\ ( p +s B ) <_s s ) <-> ( E. l e. L s = ( l +s B ) /\ ( p +s B ) <_s s ) ) with typecode |-
41	40	exbii	Could not format ( E. s E. l e. L ( s = ( l +s B ) /\ ( p +s B ) <_s s ) <-> E. s ( E. l e. L s = ( l +s B ) /\ ( p +s B ) <_s s ) ) : No typesetting found for |- ( E. s E. l e. L ( s = ( l +s B ) /\ ( p +s B ) <_s s ) <-> E. s ( E. l e. L s = ( l +s B ) /\ ( p +s B ) <_s s ) ) with typecode |-
42	35 39 41	3bitr3ri	Could not format ( E. s ( E. l e. L s = ( l +s B ) /\ ( p +s B ) <_s s ) <-> E. l e. L ( p +s B ) <_s ( l +s B ) ) : No typesetting found for |- ( E. s ( E. l e. L s = ( l +s B ) /\ ( p +s B ) <_s s ) <-> E. l e. L ( p +s B ) <_s ( l +s B ) ) with typecode |-
43	34 42	bitri	Could not format ( E. s e. { y | E. l e. L y = ( l +s B ) } ( p +s B ) <_s s <-> E. l e. L ( p +s B ) <_s ( l +s B ) ) : No typesetting found for |- ( E. s e. { y | E. l e. L y = ( l +s B ) } ( p +s B ) <_s s <-> E. l e. L ( p +s B ) <_s ( l +s B ) ) with typecode |-
44		ssun1	Could not format { y | E. l e. L y = ( l +s B ) } C_ ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) : No typesetting found for |- { y | E. l e. L y = ( l +s B ) } C_ ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) with typecode |-
45		ssrexv	Could not format ( { y | E. l e. L y = ( l +s B ) } C_ ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) -> ( E. s e. { y | E. l e. L y = ( l +s B ) } ( p +s B ) <_s s -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s ) ) : No typesetting found for |- ( { y | E. l e. L y = ( l +s B ) } C_ ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) -> ( E. s e. { y | E. l e. L y = ( l +s B ) } ( p +s B ) <_s s -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s ) ) with typecode |-
46	44 45	ax-mp	Could not format ( E. s e. { y | E. l e. L y = ( l +s B ) } ( p +s B ) <_s s -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s ) : No typesetting found for |- ( E. s e. { y | E. l e. L y = ( l +s B ) } ( p +s B ) <_s s -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s ) with typecode |-
47	43 46	sylbir	Could not format ( E. l e. L ( p +s B ) <_s ( l +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s ) : No typesetting found for |- ( E. l e. L ( p +s B ) <_s ( l +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s ) with typecode |-
48	47	ralimi	Could not format ( A. p e. ( _Left ` A ) E. l e. L ( p +s B ) <_s ( l +s B ) -> A. p e. ( _Left ` A ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s ) : No typesetting found for |- ( A. p e. ( _Left ` A ) E. l e. L ( p +s B ) <_s ( l +s B ) -> A. p e. ( _Left ` A ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s ) with typecode |-
49	31 48	syl	Could not format ( ph -> A. p e. ( _Left ` A ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s ) : No typesetting found for |- ( ph -> A. p e. ( _Left ` A ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s ) with typecode |-
50	2 4	cofcutr1d	Could not format ( ph -> A. q e. ( _Left ` B ) E. m e. M q <_s m ) : No typesetting found for |- ( ph -> A. q e. ( _Left ` B ) E. m e. M q <_s m ) with typecode |-
51		leftssno	Could not format ( _Left ` B ) C_ No : No typesetting found for |- ( _Left ` B ) C_ No with typecode |-
52	51	sseli	Could not format ( q e. ( _Left ` B ) -> q e. No ) : No typesetting found for |- ( q e. ( _Left ` B ) -> q e. No ) with typecode |-
53	52	ad2antlr	Could not format ( ( ( ph /\ q e. ( _Left ` B ) ) /\ m e. M ) -> q e. No ) : No typesetting found for |- ( ( ( ph /\ q e. ( _Left ` B ) ) /\ m e. M ) -> q e. No ) with typecode |-
54		ssltss1	$$⊢M{\ll }_{s}S\to M\subseteq \mathrm{No}$$
55	2 54	syl	$$⊢\phi \to M\subseteq \mathrm{No}$$
56	55	adantr	Could not format ( ( ph /\ q e. ( _Left ` B ) ) -> M C_ No ) : No typesetting found for |- ( ( ph /\ q e. ( _Left ` B ) ) -> M C_ No ) with typecode |-
57	56	sselda	Could not format ( ( ( ph /\ q e. ( _Left ` B ) ) /\ m e. M ) -> m e. No ) : No typesetting found for |- ( ( ( ph /\ q e. ( _Left ` B ) ) /\ m e. M ) -> m e. No ) with typecode |-
58	6	ad2antrr	Could not format ( ( ( ph /\ q e. ( _Left ` B ) ) /\ m e. M ) -> A e. No ) : No typesetting found for |- ( ( ( ph /\ q e. ( _Left ` B ) ) /\ m e. M ) -> A e. No ) with typecode |-
59	53 57 58	sleadd2d	Could not format ( ( ( ph /\ q e. ( _Left ` B ) ) /\ m e. M ) -> ( q <_s m <-> ( A +s q ) <_s ( A +s m ) ) ) : No typesetting found for |- ( ( ( ph /\ q e. ( _Left ` B ) ) /\ m e. M ) -> ( q <_s m <-> ( A +s q ) <_s ( A +s m ) ) ) with typecode |-
60	59	rexbidva	Could not format ( ( ph /\ q e. ( _Left ` B ) ) -> ( E. m e. M q <_s m <-> E. m e. M ( A +s q ) <_s ( A +s m ) ) ) : No typesetting found for |- ( ( ph /\ q e. ( _Left ` B ) ) -> ( E. m e. M q <_s m <-> E. m e. M ( A +s q ) <_s ( A +s m ) ) ) with typecode |-
61	60	ralbidva	Could not format ( ph -> ( A. q e. ( _Left ` B ) E. m e. M q <_s m <-> A. q e. ( _Left ` B ) E. m e. M ( A +s q ) <_s ( A +s m ) ) ) : No typesetting found for |- ( ph -> ( A. q e. ( _Left ` B ) E. m e. M q <_s m <-> A. q e. ( _Left ` B ) E. m e. M ( A +s q ) <_s ( A +s m ) ) ) with typecode |-
62	50 61	mpbid	Could not format ( ph -> A. q e. ( _Left ` B ) E. m e. M ( A +s q ) <_s ( A +s m ) ) : No typesetting found for |- ( ph -> A. q e. ( _Left ` B ) E. m e. M ( A +s q ) <_s ( A +s m ) ) with typecode |-
63		eqeq1	Could not format ( z = s -> ( z = ( A +s m ) <-> s = ( A +s m ) ) ) : No typesetting found for |- ( z = s -> ( z = ( A +s m ) <-> s = ( A +s m ) ) ) with typecode |-
64	63	rexbidv	Could not format ( z = s -> ( E. m e. M z = ( A +s m ) <-> E. m e. M s = ( A +s m ) ) ) : No typesetting found for |- ( z = s -> ( E. m e. M z = ( A +s m ) <-> E. m e. M s = ( A +s m ) ) ) with typecode |-
65	64	rexab	Could not format ( E. s e. { z | E. m e. M z = ( A +s m ) } ( A +s q ) <_s s <-> E. s ( E. m e. M s = ( A +s m ) /\ ( A +s q ) <_s s ) ) : No typesetting found for |- ( E. s e. { z | E. m e. M z = ( A +s m ) } ( A +s q ) <_s s <-> E. s ( E. m e. M s = ( A +s m ) /\ ( A +s q ) <_s s ) ) with typecode |-
66		rexcom4	Could not format ( E. m e. M E. s ( s = ( A +s m ) /\ ( A +s q ) <_s s ) <-> E. s E. m e. M ( s = ( A +s m ) /\ ( A +s q ) <_s s ) ) : No typesetting found for |- ( E. m e. M E. s ( s = ( A +s m ) /\ ( A +s q ) <_s s ) <-> E. s E. m e. M ( s = ( A +s m ) /\ ( A +s q ) <_s s ) ) with typecode |-
67		ovex	Could not format ( A +s m ) e. _V : No typesetting found for |- ( A +s m ) e. _V with typecode |-
68		breq2	Could not format ( s = ( A +s m ) -> ( ( A +s q ) <_s s <-> ( A +s q ) <_s ( A +s m ) ) ) : No typesetting found for |- ( s = ( A +s m ) -> ( ( A +s q ) <_s s <-> ( A +s q ) <_s ( A +s m ) ) ) with typecode |-
69	67 68	ceqsexv	Could not format ( E. s ( s = ( A +s m ) /\ ( A +s q ) <_s s ) <-> ( A +s q ) <_s ( A +s m ) ) : No typesetting found for |- ( E. s ( s = ( A +s m ) /\ ( A +s q ) <_s s ) <-> ( A +s q ) <_s ( A +s m ) ) with typecode |-
70	69	rexbii	Could not format ( E. m e. M E. s ( s = ( A +s m ) /\ ( A +s q ) <_s s ) <-> E. m e. M ( A +s q ) <_s ( A +s m ) ) : No typesetting found for |- ( E. m e. M E. s ( s = ( A +s m ) /\ ( A +s q ) <_s s ) <-> E. m e. M ( A +s q ) <_s ( A +s m ) ) with typecode |-
71		r19.41v	Could not format ( E. m e. M ( s = ( A +s m ) /\ ( A +s q ) <_s s ) <-> ( E. m e. M s = ( A +s m ) /\ ( A +s q ) <_s s ) ) : No typesetting found for |- ( E. m e. M ( s = ( A +s m ) /\ ( A +s q ) <_s s ) <-> ( E. m e. M s = ( A +s m ) /\ ( A +s q ) <_s s ) ) with typecode |-
72	71	exbii	Could not format ( E. s E. m e. M ( s = ( A +s m ) /\ ( A +s q ) <_s s ) <-> E. s ( E. m e. M s = ( A +s m ) /\ ( A +s q ) <_s s ) ) : No typesetting found for |- ( E. s E. m e. M ( s = ( A +s m ) /\ ( A +s q ) <_s s ) <-> E. s ( E. m e. M s = ( A +s m ) /\ ( A +s q ) <_s s ) ) with typecode |-
73	66 70 72	3bitr3ri	Could not format ( E. s ( E. m e. M s = ( A +s m ) /\ ( A +s q ) <_s s ) <-> E. m e. M ( A +s q ) <_s ( A +s m ) ) : No typesetting found for |- ( E. s ( E. m e. M s = ( A +s m ) /\ ( A +s q ) <_s s ) <-> E. m e. M ( A +s q ) <_s ( A +s m ) ) with typecode |-
74	65 73	bitri	Could not format ( E. s e. { z | E. m e. M z = ( A +s m ) } ( A +s q ) <_s s <-> E. m e. M ( A +s q ) <_s ( A +s m ) ) : No typesetting found for |- ( E. s e. { z | E. m e. M z = ( A +s m ) } ( A +s q ) <_s s <-> E. m e. M ( A +s q ) <_s ( A +s m ) ) with typecode |-
75		ssun2	Could not format { z | E. m e. M z = ( A +s m ) } C_ ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) : No typesetting found for |- { z | E. m e. M z = ( A +s m ) } C_ ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) with typecode |-
76		ssrexv	Could not format ( { z | E. m e. M z = ( A +s m ) } C_ ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) -> ( E. s e. { z | E. m e. M z = ( A +s m ) } ( A +s q ) <_s s -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s ) ) : No typesetting found for |- ( { z | E. m e. M z = ( A +s m ) } C_ ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) -> ( E. s e. { z | E. m e. M z = ( A +s m ) } ( A +s q ) <_s s -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s ) ) with typecode |-
77	75 76	ax-mp	Could not format ( E. s e. { z | E. m e. M z = ( A +s m ) } ( A +s q ) <_s s -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s ) : No typesetting found for |- ( E. s e. { z | E. m e. M z = ( A +s m ) } ( A +s q ) <_s s -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s ) with typecode |-
78	74 77	sylbir	Could not format ( E. m e. M ( A +s q ) <_s ( A +s m ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s ) : No typesetting found for |- ( E. m e. M ( A +s q ) <_s ( A +s m ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s ) with typecode |-
79	78	ralimi	Could not format ( A. q e. ( _Left ` B ) E. m e. M ( A +s q ) <_s ( A +s m ) -> A. q e. ( _Left ` B ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s ) : No typesetting found for |- ( A. q e. ( _Left ` B ) E. m e. M ( A +s q ) <_s ( A +s m ) -> A. q e. ( _Left ` B ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s ) with typecode |-
80	62 79	syl	Could not format ( ph -> A. q e. ( _Left ` B ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s ) : No typesetting found for |- ( ph -> A. q e. ( _Left ` B ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s ) with typecode |-
81		ralunb	Could not format ( A. r e. ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s <-> ( A. r e. { a | E. p e. ( _Left ` A ) a = ( p +s B ) } E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s /\ A. r e. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) ) : No typesetting found for |- ( A. r e. ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s <-> ( A. r e. { a | E. p e. ( _Left ` A ) a = ( p +s B ) } E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s /\ A. r e. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) ) with typecode |-
82		eqeq1	Could not format ( a = r -> ( a = ( p +s B ) <-> r = ( p +s B ) ) ) : No typesetting found for |- ( a = r -> ( a = ( p +s B ) <-> r = ( p +s B ) ) ) with typecode |-
83	82	rexbidv	Could not format ( a = r -> ( E. p e. ( _Left ` A ) a = ( p +s B ) <-> E. p e. ( _Left ` A ) r = ( p +s B ) ) ) : No typesetting found for |- ( a = r -> ( E. p e. ( _Left ` A ) a = ( p +s B ) <-> E. p e. ( _Left ` A ) r = ( p +s B ) ) ) with typecode |-
84	83	ralab	Could not format ( A. r e. { a | E. p e. ( _Left ` A ) a = ( p +s B ) } E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s <-> A. r ( E. p e. ( _Left ` A ) r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) ) : No typesetting found for |- ( A. r e. { a | E. p e. ( _Left ` A ) a = ( p +s B ) } E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s <-> A. r ( E. p e. ( _Left ` A ) r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) ) with typecode |-
85		ralcom4	Could not format ( A. p e. ( _Left ` A ) A. r ( r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> A. r A. p e. ( _Left ` A ) ( r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) ) : No typesetting found for |- ( A. p e. ( _Left ` A ) A. r ( r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> A. r A. p e. ( _Left ` A ) ( r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) ) with typecode |-
86		ovex	Could not format ( p +s B ) e. _V : No typesetting found for |- ( p +s B ) e. _V with typecode |-
87		breq1	Could not format ( r = ( p +s B ) -> ( r <_s s <-> ( p +s B ) <_s s ) ) : No typesetting found for |- ( r = ( p +s B ) -> ( r <_s s <-> ( p +s B ) <_s s ) ) with typecode |-
88	87	rexbidv	Could not format ( r = ( p +s B ) -> ( E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s <-> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s ) ) : No typesetting found for |- ( r = ( p +s B ) -> ( E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s <-> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s ) ) with typecode |-
89	86 88	ceqsalv	Could not format ( A. r ( r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s ) : No typesetting found for |- ( A. r ( r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s ) with typecode |-
90	89	ralbii	Could not format ( A. p e. ( _Left ` A ) A. r ( r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> A. p e. ( _Left ` A ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s ) : No typesetting found for |- ( A. p e. ( _Left ` A ) A. r ( r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> A. p e. ( _Left ` A ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s ) with typecode |-
91		r19.23v	Could not format ( A. p e. ( _Left ` A ) ( r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> ( E. p e. ( _Left ` A ) r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) ) : No typesetting found for |- ( A. p e. ( _Left ` A ) ( r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> ( E. p e. ( _Left ` A ) r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) ) with typecode |-
92	91	albii	Could not format ( A. r A. p e. ( _Left ` A ) ( r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> A. r ( E. p e. ( _Left ` A ) r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) ) : No typesetting found for |- ( A. r A. p e. ( _Left ` A ) ( r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> A. r ( E. p e. ( _Left ` A ) r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) ) with typecode |-
93	85 90 92	3bitr3ri	Could not format ( A. r ( E. p e. ( _Left ` A ) r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> A. p e. ( _Left ` A ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s ) : No typesetting found for |- ( A. r ( E. p e. ( _Left ` A ) r = ( p +s B ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> A. p e. ( _Left ` A ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s ) with typecode |-
94	84 93	bitri	Could not format ( A. r e. { a | E. p e. ( _Left ` A ) a = ( p +s B ) } E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s <-> A. p e. ( _Left ` A ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s ) : No typesetting found for |- ( A. r e. { a | E. p e. ( _Left ` A ) a = ( p +s B ) } E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s <-> A. p e. ( _Left ` A ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s ) with typecode |-
95		eqeq1	Could not format ( b = r -> ( b = ( A +s q ) <-> r = ( A +s q ) ) ) : No typesetting found for |- ( b = r -> ( b = ( A +s q ) <-> r = ( A +s q ) ) ) with typecode |-
96	95	rexbidv	Could not format ( b = r -> ( E. q e. ( _Left ` B ) b = ( A +s q ) <-> E. q e. ( _Left ` B ) r = ( A +s q ) ) ) : No typesetting found for |- ( b = r -> ( E. q e. ( _Left ` B ) b = ( A +s q ) <-> E. q e. ( _Left ` B ) r = ( A +s q ) ) ) with typecode |-
97	96	ralab	Could not format ( A. r e. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s <-> A. r ( E. q e. ( _Left ` B ) r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) ) : No typesetting found for |- ( A. r e. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s <-> A. r ( E. q e. ( _Left ` B ) r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) ) with typecode |-
98		ralcom4	Could not format ( A. q e. ( _Left ` B ) A. r ( r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> A. r A. q e. ( _Left ` B ) ( r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) ) : No typesetting found for |- ( A. q e. ( _Left ` B ) A. r ( r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> A. r A. q e. ( _Left ` B ) ( r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) ) with typecode |-
99		ovex	Could not format ( A +s q ) e. _V : No typesetting found for |- ( A +s q ) e. _V with typecode |-
100		breq1	Could not format ( r = ( A +s q ) -> ( r <_s s <-> ( A +s q ) <_s s ) ) : No typesetting found for |- ( r = ( A +s q ) -> ( r <_s s <-> ( A +s q ) <_s s ) ) with typecode |-
101	100	rexbidv	Could not format ( r = ( A +s q ) -> ( E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s <-> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s ) ) : No typesetting found for |- ( r = ( A +s q ) -> ( E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s <-> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s ) ) with typecode |-
102	99 101	ceqsalv	Could not format ( A. r ( r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s ) : No typesetting found for |- ( A. r ( r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s ) with typecode |-
103	102	ralbii	Could not format ( A. q e. ( _Left ` B ) A. r ( r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> A. q e. ( _Left ` B ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s ) : No typesetting found for |- ( A. q e. ( _Left ` B ) A. r ( r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> A. q e. ( _Left ` B ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s ) with typecode |-
104		r19.23v	Could not format ( A. q e. ( _Left ` B ) ( r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> ( E. q e. ( _Left ` B ) r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) ) : No typesetting found for |- ( A. q e. ( _Left ` B ) ( r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> ( E. q e. ( _Left ` B ) r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) ) with typecode |-
105	104	albii	Could not format ( A. r A. q e. ( _Left ` B ) ( r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> A. r ( E. q e. ( _Left ` B ) r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) ) : No typesetting found for |- ( A. r A. q e. ( _Left ` B ) ( r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> A. r ( E. q e. ( _Left ` B ) r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) ) with typecode |-
106	98 103 105	3bitr3ri	Could not format ( A. r ( E. q e. ( _Left ` B ) r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> A. q e. ( _Left ` B ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s ) : No typesetting found for |- ( A. r ( E. q e. ( _Left ` B ) r = ( A +s q ) -> E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> A. q e. ( _Left ` B ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s ) with typecode |-
107	97 106	bitri	Could not format ( A. r e. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s <-> A. q e. ( _Left ` B ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s ) : No typesetting found for |- ( A. r e. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s <-> A. q e. ( _Left ` B ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s ) with typecode |-
108	94 107	anbi12i	Could not format ( ( A. r e. { a | E. p e. ( _Left ` A ) a = ( p +s B ) } E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s /\ A. r e. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> ( A. p e. ( _Left ` A ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s /\ A. q e. ( _Left ` B ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s ) ) : No typesetting found for |- ( ( A. r e. { a | E. p e. ( _Left ` A ) a = ( p +s B ) } E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s /\ A. r e. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) <-> ( A. p e. ( _Left ` A ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s /\ A. q e. ( _Left ` B ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s ) ) with typecode |-
109	81 108	bitri	Could not format ( A. r e. ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s <-> ( A. p e. ( _Left ` A ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s /\ A. q e. ( _Left ` B ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s ) ) : No typesetting found for |- ( A. r e. ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s <-> ( A. p e. ( _Left ` A ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( p +s B ) <_s s /\ A. q e. ( _Left ` B ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ( A +s q ) <_s s ) ) with typecode |-
110	49 80 109	sylanbrc	Could not format ( ph -> A. r e. ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) : No typesetting found for |- ( ph -> A. r e. ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) E. s e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) r <_s s ) with typecode |-
111	1 3	cofcutr2d	Could not format ( ph -> A. e e. ( _Right ` A ) E. r e. R r <_s e ) : No typesetting found for |- ( ph -> A. e e. ( _Right ` A ) E. r e. R r <_s e ) with typecode |-
112		ssltss2	$$⊢L{\ll }_{s}R\to R\subseteq \mathrm{No}$$
113	1 112	syl	$$⊢\phi \to R\subseteq \mathrm{No}$$
114	113	adantr	Could not format ( ( ph /\ e e. ( _Right ` A ) ) -> R C_ No ) : No typesetting found for |- ( ( ph /\ e e. ( _Right ` A ) ) -> R C_ No ) with typecode |-
115	114	sselda	Could not format ( ( ( ph /\ e e. ( _Right ` A ) ) /\ r e. R ) -> r e. No ) : No typesetting found for |- ( ( ( ph /\ e e. ( _Right ` A ) ) /\ r e. R ) -> r e. No ) with typecode |-
116		rightssno	Could not format ( _Right ` A ) C_ No : No typesetting found for |- ( _Right ` A ) C_ No with typecode |-
117	116	sseli	Could not format ( e e. ( _Right ` A ) -> e e. No ) : No typesetting found for |- ( e e. ( _Right ` A ) -> e e. No ) with typecode |-
118	117	ad2antlr	Could not format ( ( ( ph /\ e e. ( _Right ` A ) ) /\ r e. R ) -> e e. No ) : No typesetting found for |- ( ( ( ph /\ e e. ( _Right ` A ) ) /\ r e. R ) -> e e. No ) with typecode |-
119	8	ad2antrr	Could not format ( ( ( ph /\ e e. ( _Right ` A ) ) /\ r e. R ) -> B e. No ) : No typesetting found for |- ( ( ( ph /\ e e. ( _Right ` A ) ) /\ r e. R ) -> B e. No ) with typecode |-
120	115 118 119	sleadd1d	Could not format ( ( ( ph /\ e e. ( _Right ` A ) ) /\ r e. R ) -> ( r <_s e <-> ( r +s B ) <_s ( e +s B ) ) ) : No typesetting found for |- ( ( ( ph /\ e e. ( _Right ` A ) ) /\ r e. R ) -> ( r <_s e <-> ( r +s B ) <_s ( e +s B ) ) ) with typecode |-
121	120	rexbidva	Could not format ( ( ph /\ e e. ( _Right ` A ) ) -> ( E. r e. R r <_s e <-> E. r e. R ( r +s B ) <_s ( e +s B ) ) ) : No typesetting found for |- ( ( ph /\ e e. ( _Right ` A ) ) -> ( E. r e. R r <_s e <-> E. r e. R ( r +s B ) <_s ( e +s B ) ) ) with typecode |-
122	121	ralbidva	Could not format ( ph -> ( A. e e. ( _Right ` A ) E. r e. R r <_s e <-> A. e e. ( _Right ` A ) E. r e. R ( r +s B ) <_s ( e +s B ) ) ) : No typesetting found for |- ( ph -> ( A. e e. ( _Right ` A ) E. r e. R r <_s e <-> A. e e. ( _Right ` A ) E. r e. R ( r +s B ) <_s ( e +s B ) ) ) with typecode |-
123	111 122	mpbid	Could not format ( ph -> A. e e. ( _Right ` A ) E. r e. R ( r +s B ) <_s ( e +s B ) ) : No typesetting found for |- ( ph -> A. e e. ( _Right ` A ) E. r e. R ( r +s B ) <_s ( e +s B ) ) with typecode |-
124		eqeq1	Could not format ( w = b -> ( w = ( r +s B ) <-> b = ( r +s B ) ) ) : No typesetting found for |- ( w = b -> ( w = ( r +s B ) <-> b = ( r +s B ) ) ) with typecode |-
125	124	rexbidv	Could not format ( w = b -> ( E. r e. R w = ( r +s B ) <-> E. r e. R b = ( r +s B ) ) ) : No typesetting found for |- ( w = b -> ( E. r e. R w = ( r +s B ) <-> E. r e. R b = ( r +s B ) ) ) with typecode |-
126	125	rexab	Could not format ( E. b e. { w | E. r e. R w = ( r +s B ) } b <_s ( e +s B ) <-> E. b ( E. r e. R b = ( r +s B ) /\ b <_s ( e +s B ) ) ) : No typesetting found for |- ( E. b e. { w | E. r e. R w = ( r +s B ) } b <_s ( e +s B ) <-> E. b ( E. r e. R b = ( r +s B ) /\ b <_s ( e +s B ) ) ) with typecode |-
127		rexcom4	Could not format ( E. r e. R E. b ( b = ( r +s B ) /\ b <_s ( e +s B ) ) <-> E. b E. r e. R ( b = ( r +s B ) /\ b <_s ( e +s B ) ) ) : No typesetting found for |- ( E. r e. R E. b ( b = ( r +s B ) /\ b <_s ( e +s B ) ) <-> E. b E. r e. R ( b = ( r +s B ) /\ b <_s ( e +s B ) ) ) with typecode |-
128		ovex	Could not format ( r +s B ) e. _V : No typesetting found for |- ( r +s B ) e. _V with typecode |-
129		breq1	Could not format ( b = ( r +s B ) -> ( b <_s ( e +s B ) <-> ( r +s B ) <_s ( e +s B ) ) ) : No typesetting found for |- ( b = ( r +s B ) -> ( b <_s ( e +s B ) <-> ( r +s B ) <_s ( e +s B ) ) ) with typecode |-
130	128 129	ceqsexv	Could not format ( E. b ( b = ( r +s B ) /\ b <_s ( e +s B ) ) <-> ( r +s B ) <_s ( e +s B ) ) : No typesetting found for |- ( E. b ( b = ( r +s B ) /\ b <_s ( e +s B ) ) <-> ( r +s B ) <_s ( e +s B ) ) with typecode |-
131	130	rexbii	Could not format ( E. r e. R E. b ( b = ( r +s B ) /\ b <_s ( e +s B ) ) <-> E. r e. R ( r +s B ) <_s ( e +s B ) ) : No typesetting found for |- ( E. r e. R E. b ( b = ( r +s B ) /\ b <_s ( e +s B ) ) <-> E. r e. R ( r +s B ) <_s ( e +s B ) ) with typecode |-
132		r19.41v	Could not format ( E. r e. R ( b = ( r +s B ) /\ b <_s ( e +s B ) ) <-> ( E. r e. R b = ( r +s B ) /\ b <_s ( e +s B ) ) ) : No typesetting found for |- ( E. r e. R ( b = ( r +s B ) /\ b <_s ( e +s B ) ) <-> ( E. r e. R b = ( r +s B ) /\ b <_s ( e +s B ) ) ) with typecode |-
133	132	exbii	Could not format ( E. b E. r e. R ( b = ( r +s B ) /\ b <_s ( e +s B ) ) <-> E. b ( E. r e. R b = ( r +s B ) /\ b <_s ( e +s B ) ) ) : No typesetting found for |- ( E. b E. r e. R ( b = ( r +s B ) /\ b <_s ( e +s B ) ) <-> E. b ( E. r e. R b = ( r +s B ) /\ b <_s ( e +s B ) ) ) with typecode |-
134	127 131 133	3bitr3ri	Could not format ( E. b ( E. r e. R b = ( r +s B ) /\ b <_s ( e +s B ) ) <-> E. r e. R ( r +s B ) <_s ( e +s B ) ) : No typesetting found for |- ( E. b ( E. r e. R b = ( r +s B ) /\ b <_s ( e +s B ) ) <-> E. r e. R ( r +s B ) <_s ( e +s B ) ) with typecode |-
135	126 134	bitri	Could not format ( E. b e. { w | E. r e. R w = ( r +s B ) } b <_s ( e +s B ) <-> E. r e. R ( r +s B ) <_s ( e +s B ) ) : No typesetting found for |- ( E. b e. { w | E. r e. R w = ( r +s B ) } b <_s ( e +s B ) <-> E. r e. R ( r +s B ) <_s ( e +s B ) ) with typecode |-
136		ssun1	Could not format { w | E. r e. R w = ( r +s B ) } C_ ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) : No typesetting found for |- { w | E. r e. R w = ( r +s B ) } C_ ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) with typecode |-
137		ssrexv	Could not format ( { w | E. r e. R w = ( r +s B ) } C_ ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) -> ( E. b e. { w | E. r e. R w = ( r +s B ) } b <_s ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) ) ) : No typesetting found for |- ( { w | E. r e. R w = ( r +s B ) } C_ ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) -> ( E. b e. { w | E. r e. R w = ( r +s B ) } b <_s ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) ) ) with typecode |-
138	136 137	ax-mp	Could not format ( E. b e. { w | E. r e. R w = ( r +s B ) } b <_s ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) ) : No typesetting found for |- ( E. b e. { w | E. r e. R w = ( r +s B ) } b <_s ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) ) with typecode |-
139	135 138	sylbir	Could not format ( E. r e. R ( r +s B ) <_s ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) ) : No typesetting found for |- ( E. r e. R ( r +s B ) <_s ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) ) with typecode |-
140	139	ralimi	Could not format ( A. e e. ( _Right ` A ) E. r e. R ( r +s B ) <_s ( e +s B ) -> A. e e. ( _Right ` A ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) ) : No typesetting found for |- ( A. e e. ( _Right ` A ) E. r e. R ( r +s B ) <_s ( e +s B ) -> A. e e. ( _Right ` A ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) ) with typecode |-
141	123 140	syl	Could not format ( ph -> A. e e. ( _Right ` A ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) ) : No typesetting found for |- ( ph -> A. e e. ( _Right ` A ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) ) with typecode |-
142	2 4	cofcutr2d	Could not format ( ph -> A. f e. ( _Right ` B ) E. s e. S s <_s f ) : No typesetting found for |- ( ph -> A. f e. ( _Right ` B ) E. s e. S s <_s f ) with typecode |-
143		ssltss2	$$⊢M{\ll }_{s}S\to S\subseteq \mathrm{No}$$
144	2 143	syl	$$⊢\phi \to S\subseteq \mathrm{No}$$
145	144	adantr	Could not format ( ( ph /\ f e. ( _Right ` B ) ) -> S C_ No ) : No typesetting found for |- ( ( ph /\ f e. ( _Right ` B ) ) -> S C_ No ) with typecode |-
146	145	sselda	Could not format ( ( ( ph /\ f e. ( _Right ` B ) ) /\ s e. S ) -> s e. No ) : No typesetting found for |- ( ( ( ph /\ f e. ( _Right ` B ) ) /\ s e. S ) -> s e. No ) with typecode |-
147		rightssno	Could not format ( _Right ` B ) C_ No : No typesetting found for |- ( _Right ` B ) C_ No with typecode |-
148	147	sseli	Could not format ( f e. ( _Right ` B ) -> f e. No ) : No typesetting found for |- ( f e. ( _Right ` B ) -> f e. No ) with typecode |-
149	148	ad2antlr	Could not format ( ( ( ph /\ f e. ( _Right ` B ) ) /\ s e. S ) -> f e. No ) : No typesetting found for |- ( ( ( ph /\ f e. ( _Right ` B ) ) /\ s e. S ) -> f e. No ) with typecode |-
150	6	ad2antrr	Could not format ( ( ( ph /\ f e. ( _Right ` B ) ) /\ s e. S ) -> A e. No ) : No typesetting found for |- ( ( ( ph /\ f e. ( _Right ` B ) ) /\ s e. S ) -> A e. No ) with typecode |-
151	146 149 150	sleadd2d	Could not format ( ( ( ph /\ f e. ( _Right ` B ) ) /\ s e. S ) -> ( s <_s f <-> ( A +s s ) <_s ( A +s f ) ) ) : No typesetting found for |- ( ( ( ph /\ f e. ( _Right ` B ) ) /\ s e. S ) -> ( s <_s f <-> ( A +s s ) <_s ( A +s f ) ) ) with typecode |-
152	151	rexbidva	Could not format ( ( ph /\ f e. ( _Right ` B ) ) -> ( E. s e. S s <_s f <-> E. s e. S ( A +s s ) <_s ( A +s f ) ) ) : No typesetting found for |- ( ( ph /\ f e. ( _Right ` B ) ) -> ( E. s e. S s <_s f <-> E. s e. S ( A +s s ) <_s ( A +s f ) ) ) with typecode |-
153	152	ralbidva	Could not format ( ph -> ( A. f e. ( _Right ` B ) E. s e. S s <_s f <-> A. f e. ( _Right ` B ) E. s e. S ( A +s s ) <_s ( A +s f ) ) ) : No typesetting found for |- ( ph -> ( A. f e. ( _Right ` B ) E. s e. S s <_s f <-> A. f e. ( _Right ` B ) E. s e. S ( A +s s ) <_s ( A +s f ) ) ) with typecode |-
154	142 153	mpbid	Could not format ( ph -> A. f e. ( _Right ` B ) E. s e. S ( A +s s ) <_s ( A +s f ) ) : No typesetting found for |- ( ph -> A. f e. ( _Right ` B ) E. s e. S ( A +s s ) <_s ( A +s f ) ) with typecode |-
155		eqeq1	Could not format ( t = b -> ( t = ( A +s s ) <-> b = ( A +s s ) ) ) : No typesetting found for |- ( t = b -> ( t = ( A +s s ) <-> b = ( A +s s ) ) ) with typecode |-
156	155	rexbidv	Could not format ( t = b -> ( E. s e. S t = ( A +s s ) <-> E. s e. S b = ( A +s s ) ) ) : No typesetting found for |- ( t = b -> ( E. s e. S t = ( A +s s ) <-> E. s e. S b = ( A +s s ) ) ) with typecode |-
157	156	rexab	Could not format ( E. b e. { t | E. s e. S t = ( A +s s ) } b <_s ( A +s f ) <-> E. b ( E. s e. S b = ( A +s s ) /\ b <_s ( A +s f ) ) ) : No typesetting found for |- ( E. b e. { t | E. s e. S t = ( A +s s ) } b <_s ( A +s f ) <-> E. b ( E. s e. S b = ( A +s s ) /\ b <_s ( A +s f ) ) ) with typecode |-
158		rexcom4	Could not format ( E. s e. S E. b ( b = ( A +s s ) /\ b <_s ( A +s f ) ) <-> E. b E. s e. S ( b = ( A +s s ) /\ b <_s ( A +s f ) ) ) : No typesetting found for |- ( E. s e. S E. b ( b = ( A +s s ) /\ b <_s ( A +s f ) ) <-> E. b E. s e. S ( b = ( A +s s ) /\ b <_s ( A +s f ) ) ) with typecode |-
159		ovex	Could not format ( A +s s ) e. _V : No typesetting found for |- ( A +s s ) e. _V with typecode |-
160		breq1	Could not format ( b = ( A +s s ) -> ( b <_s ( A +s f ) <-> ( A +s s ) <_s ( A +s f ) ) ) : No typesetting found for |- ( b = ( A +s s ) -> ( b <_s ( A +s f ) <-> ( A +s s ) <_s ( A +s f ) ) ) with typecode |-
161	159 160	ceqsexv	Could not format ( E. b ( b = ( A +s s ) /\ b <_s ( A +s f ) ) <-> ( A +s s ) <_s ( A +s f ) ) : No typesetting found for |- ( E. b ( b = ( A +s s ) /\ b <_s ( A +s f ) ) <-> ( A +s s ) <_s ( A +s f ) ) with typecode |-
162	161	rexbii	Could not format ( E. s e. S E. b ( b = ( A +s s ) /\ b <_s ( A +s f ) ) <-> E. s e. S ( A +s s ) <_s ( A +s f ) ) : No typesetting found for |- ( E. s e. S E. b ( b = ( A +s s ) /\ b <_s ( A +s f ) ) <-> E. s e. S ( A +s s ) <_s ( A +s f ) ) with typecode |-
163		r19.41v	Could not format ( E. s e. S ( b = ( A +s s ) /\ b <_s ( A +s f ) ) <-> ( E. s e. S b = ( A +s s ) /\ b <_s ( A +s f ) ) ) : No typesetting found for |- ( E. s e. S ( b = ( A +s s ) /\ b <_s ( A +s f ) ) <-> ( E. s e. S b = ( A +s s ) /\ b <_s ( A +s f ) ) ) with typecode |-
164	163	exbii	Could not format ( E. b E. s e. S ( b = ( A +s s ) /\ b <_s ( A +s f ) ) <-> E. b ( E. s e. S b = ( A +s s ) /\ b <_s ( A +s f ) ) ) : No typesetting found for |- ( E. b E. s e. S ( b = ( A +s s ) /\ b <_s ( A +s f ) ) <-> E. b ( E. s e. S b = ( A +s s ) /\ b <_s ( A +s f ) ) ) with typecode |-
165	158 162 164	3bitr3ri	Could not format ( E. b ( E. s e. S b = ( A +s s ) /\ b <_s ( A +s f ) ) <-> E. s e. S ( A +s s ) <_s ( A +s f ) ) : No typesetting found for |- ( E. b ( E. s e. S b = ( A +s s ) /\ b <_s ( A +s f ) ) <-> E. s e. S ( A +s s ) <_s ( A +s f ) ) with typecode |-
166	157 165	bitri	Could not format ( E. b e. { t | E. s e. S t = ( A +s s ) } b <_s ( A +s f ) <-> E. s e. S ( A +s s ) <_s ( A +s f ) ) : No typesetting found for |- ( E. b e. { t | E. s e. S t = ( A +s s ) } b <_s ( A +s f ) <-> E. s e. S ( A +s s ) <_s ( A +s f ) ) with typecode |-
167		ssun2	Could not format { t | E. s e. S t = ( A +s s ) } C_ ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) : No typesetting found for |- { t | E. s e. S t = ( A +s s ) } C_ ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) with typecode |-
168		ssrexv	Could not format ( { t | E. s e. S t = ( A +s s ) } C_ ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) -> ( E. b e. { t | E. s e. S t = ( A +s s ) } b <_s ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) ) ) : No typesetting found for |- ( { t | E. s e. S t = ( A +s s ) } C_ ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) -> ( E. b e. { t | E. s e. S t = ( A +s s ) } b <_s ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) ) ) with typecode |-
169	167 168	ax-mp	Could not format ( E. b e. { t | E. s e. S t = ( A +s s ) } b <_s ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) ) : No typesetting found for |- ( E. b e. { t | E. s e. S t = ( A +s s ) } b <_s ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) ) with typecode |-
170	166 169	sylbir	Could not format ( E. s e. S ( A +s s ) <_s ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) ) : No typesetting found for |- ( E. s e. S ( A +s s ) <_s ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) ) with typecode |-
171	170	ralimi	Could not format ( A. f e. ( _Right ` B ) E. s e. S ( A +s s ) <_s ( A +s f ) -> A. f e. ( _Right ` B ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) ) : No typesetting found for |- ( A. f e. ( _Right ` B ) E. s e. S ( A +s s ) <_s ( A +s f ) -> A. f e. ( _Right ` B ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) ) with typecode |-
172	154 171	syl	Could not format ( ph -> A. f e. ( _Right ` B ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) ) : No typesetting found for |- ( ph -> A. f e. ( _Right ` B ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) ) with typecode |-
173		ralunb	Could not format ( A. a e. ( { c | E. e e. ( _Right ` A ) c = ( e +s B ) } u. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a <-> ( A. a e. { c | E. e e. ( _Right ` A ) c = ( e +s B ) } E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a /\ A. a e. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) ) : No typesetting found for |- ( A. a e. ( { c | E. e e. ( _Right ` A ) c = ( e +s B ) } u. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a <-> ( A. a e. { c | E. e e. ( _Right ` A ) c = ( e +s B ) } E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a /\ A. a e. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) ) with typecode |-
174		eqeq1	Could not format ( c = a -> ( c = ( e +s B ) <-> a = ( e +s B ) ) ) : No typesetting found for |- ( c = a -> ( c = ( e +s B ) <-> a = ( e +s B ) ) ) with typecode |-
175	174	rexbidv	Could not format ( c = a -> ( E. e e. ( _Right ` A ) c = ( e +s B ) <-> E. e e. ( _Right ` A ) a = ( e +s B ) ) ) : No typesetting found for |- ( c = a -> ( E. e e. ( _Right ` A ) c = ( e +s B ) <-> E. e e. ( _Right ` A ) a = ( e +s B ) ) ) with typecode |-
176	175	ralab	Could not format ( A. a e. { c | E. e e. ( _Right ` A ) c = ( e +s B ) } E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a <-> A. a ( E. e e. ( _Right ` A ) a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) ) : No typesetting found for |- ( A. a e. { c | E. e e. ( _Right ` A ) c = ( e +s B ) } E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a <-> A. a ( E. e e. ( _Right ` A ) a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) ) with typecode |-
177		ralcom4	Could not format ( A. e e. ( _Right ` A ) A. a ( a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> A. a A. e e. ( _Right ` A ) ( a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) ) : No typesetting found for |- ( A. e e. ( _Right ` A ) A. a ( a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> A. a A. e e. ( _Right ` A ) ( a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) ) with typecode |-
178		ovex	Could not format ( e +s B ) e. _V : No typesetting found for |- ( e +s B ) e. _V with typecode |-
179		breq2	Could not format ( a = ( e +s B ) -> ( b <_s a <-> b <_s ( e +s B ) ) ) : No typesetting found for |- ( a = ( e +s B ) -> ( b <_s a <-> b <_s ( e +s B ) ) ) with typecode |-
180	179	rexbidv	Could not format ( a = ( e +s B ) -> ( E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a <-> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) ) ) : No typesetting found for |- ( a = ( e +s B ) -> ( E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a <-> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) ) ) with typecode |-
181	178 180	ceqsalv	Could not format ( A. a ( a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) ) : No typesetting found for |- ( A. a ( a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) ) with typecode |-
182	181	ralbii	Could not format ( A. e e. ( _Right ` A ) A. a ( a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> A. e e. ( _Right ` A ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) ) : No typesetting found for |- ( A. e e. ( _Right ` A ) A. a ( a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> A. e e. ( _Right ` A ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) ) with typecode |-
183		r19.23v	Could not format ( A. e e. ( _Right ` A ) ( a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> ( E. e e. ( _Right ` A ) a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) ) : No typesetting found for |- ( A. e e. ( _Right ` A ) ( a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> ( E. e e. ( _Right ` A ) a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) ) with typecode |-
184	183	albii	Could not format ( A. a A. e e. ( _Right ` A ) ( a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> A. a ( E. e e. ( _Right ` A ) a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) ) : No typesetting found for |- ( A. a A. e e. ( _Right ` A ) ( a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> A. a ( E. e e. ( _Right ` A ) a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) ) with typecode |-
185	177 182 184	3bitr3ri	Could not format ( A. a ( E. e e. ( _Right ` A ) a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> A. e e. ( _Right ` A ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) ) : No typesetting found for |- ( A. a ( E. e e. ( _Right ` A ) a = ( e +s B ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> A. e e. ( _Right ` A ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) ) with typecode |-
186	176 185	bitri	Could not format ( A. a e. { c | E. e e. ( _Right ` A ) c = ( e +s B ) } E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a <-> A. e e. ( _Right ` A ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) ) : No typesetting found for |- ( A. a e. { c | E. e e. ( _Right ` A ) c = ( e +s B ) } E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a <-> A. e e. ( _Right ` A ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) ) with typecode |-
187		eqeq1	Could not format ( d = a -> ( d = ( A +s f ) <-> a = ( A +s f ) ) ) : No typesetting found for |- ( d = a -> ( d = ( A +s f ) <-> a = ( A +s f ) ) ) with typecode |-
188	187	rexbidv	Could not format ( d = a -> ( E. f e. ( _Right ` B ) d = ( A +s f ) <-> E. f e. ( _Right ` B ) a = ( A +s f ) ) ) : No typesetting found for |- ( d = a -> ( E. f e. ( _Right ` B ) d = ( A +s f ) <-> E. f e. ( _Right ` B ) a = ( A +s f ) ) ) with typecode |-
189	188	ralab	Could not format ( A. a e. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a <-> A. a ( E. f e. ( _Right ` B ) a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) ) : No typesetting found for |- ( A. a e. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a <-> A. a ( E. f e. ( _Right ` B ) a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) ) with typecode |-
190		ralcom4	Could not format ( A. f e. ( _Right ` B ) A. a ( a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> A. a A. f e. ( _Right ` B ) ( a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) ) : No typesetting found for |- ( A. f e. ( _Right ` B ) A. a ( a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> A. a A. f e. ( _Right ` B ) ( a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) ) with typecode |-
191		ovex	Could not format ( A +s f ) e. _V : No typesetting found for |- ( A +s f ) e. _V with typecode |-
192		breq2	Could not format ( a = ( A +s f ) -> ( b <_s a <-> b <_s ( A +s f ) ) ) : No typesetting found for |- ( a = ( A +s f ) -> ( b <_s a <-> b <_s ( A +s f ) ) ) with typecode |-
193	192	rexbidv	Could not format ( a = ( A +s f ) -> ( E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a <-> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) ) ) : No typesetting found for |- ( a = ( A +s f ) -> ( E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a <-> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) ) ) with typecode |-
194	191 193	ceqsalv	Could not format ( A. a ( a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) ) : No typesetting found for |- ( A. a ( a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) ) with typecode |-
195	194	ralbii	Could not format ( A. f e. ( _Right ` B ) A. a ( a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> A. f e. ( _Right ` B ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) ) : No typesetting found for |- ( A. f e. ( _Right ` B ) A. a ( a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> A. f e. ( _Right ` B ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) ) with typecode |-
196		r19.23v	Could not format ( A. f e. ( _Right ` B ) ( a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> ( E. f e. ( _Right ` B ) a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) ) : No typesetting found for |- ( A. f e. ( _Right ` B ) ( a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> ( E. f e. ( _Right ` B ) a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) ) with typecode |-
197	196	albii	Could not format ( A. a A. f e. ( _Right ` B ) ( a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> A. a ( E. f e. ( _Right ` B ) a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) ) : No typesetting found for |- ( A. a A. f e. ( _Right ` B ) ( a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> A. a ( E. f e. ( _Right ` B ) a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) ) with typecode |-
198	190 195 197	3bitr3ri	Could not format ( A. a ( E. f e. ( _Right ` B ) a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> A. f e. ( _Right ` B ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) ) : No typesetting found for |- ( A. a ( E. f e. ( _Right ` B ) a = ( A +s f ) -> E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> A. f e. ( _Right ` B ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) ) with typecode |-
199	189 198	bitri	Could not format ( A. a e. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a <-> A. f e. ( _Right ` B ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) ) : No typesetting found for |- ( A. a e. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a <-> A. f e. ( _Right ` B ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) ) with typecode |-
200	186 199	anbi12i	Could not format ( ( A. a e. { c | E. e e. ( _Right ` A ) c = ( e +s B ) } E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a /\ A. a e. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> ( A. e e. ( _Right ` A ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) /\ A. f e. ( _Right ` B ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) ) ) : No typesetting found for |- ( ( A. a e. { c | E. e e. ( _Right ` A ) c = ( e +s B ) } E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a /\ A. a e. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) <-> ( A. e e. ( _Right ` A ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) /\ A. f e. ( _Right ` B ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) ) ) with typecode |-
201	173 200	bitri	Could not format ( A. a e. ( { c | E. e e. ( _Right ` A ) c = ( e +s B ) } u. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a <-> ( A. e e. ( _Right ` A ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) /\ A. f e. ( _Right ` B ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) ) ) : No typesetting found for |- ( A. a e. ( { c | E. e e. ( _Right ` A ) c = ( e +s B ) } u. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a <-> ( A. e e. ( _Right ` A ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( e +s B ) /\ A. f e. ( _Right ` B ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s ( A +s f ) ) ) with typecode |-
202	141 172 201	sylanbrc	Could not format ( ph -> A. a e. ( { c | E. e e. ( _Right ` A ) c = ( e +s B ) } u. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) : No typesetting found for |- ( ph -> A. a e. ( { c | E. e e. ( _Right ` A ) c = ( e +s B ) } u. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } ) E. b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) b <_s a ) with typecode |-
203		eqid	Could not format ( l e. L |-> ( l +s B ) ) = ( l e. L |-> ( l +s B ) ) : No typesetting found for |- ( l e. L |-> ( l +s B ) ) = ( l e. L |-> ( l +s B ) ) with typecode |-
204	203	rnmpt	Could not format ran ( l e. L |-> ( l +s B ) ) = { y | E. l e. L y = ( l +s B ) } : No typesetting found for |- ran ( l e. L |-> ( l +s B ) ) = { y | E. l e. L y = ( l +s B ) } with typecode |-
205		ssltex1	$$⊢L{\ll }_{s}R\to L\in \mathrm{V}$$
206	1 205	syl	$$⊢\phi \to L\in \mathrm{V}$$
207	206	mptexd	Could not format ( ph -> ( l e. L |-> ( l +s B ) ) e. _V ) : No typesetting found for |- ( ph -> ( l e. L |-> ( l +s B ) ) e. _V ) with typecode |-
208		rnexg	Could not format ( ( l e. L |-> ( l +s B ) ) e. _V -> ran ( l e. L |-> ( l +s B ) ) e. _V ) : No typesetting found for |- ( ( l e. L |-> ( l +s B ) ) e. _V -> ran ( l e. L |-> ( l +s B ) ) e. _V ) with typecode |-
209	207 208	syl	Could not format ( ph -> ran ( l e. L |-> ( l +s B ) ) e. _V ) : No typesetting found for |- ( ph -> ran ( l e. L |-> ( l +s B ) ) e. _V ) with typecode |-
210	204 209	eqeltrrid	Could not format ( ph -> { y | E. l e. L y = ( l +s B ) } e. _V ) : No typesetting found for |- ( ph -> { y | E. l e. L y = ( l +s B ) } e. _V ) with typecode |-
211		eqid	Could not format ( m e. M |-> ( A +s m ) ) = ( m e. M |-> ( A +s m ) ) : No typesetting found for |- ( m e. M |-> ( A +s m ) ) = ( m e. M |-> ( A +s m ) ) with typecode |-
212	211	rnmpt	Could not format ran ( m e. M |-> ( A +s m ) ) = { z | E. m e. M z = ( A +s m ) } : No typesetting found for |- ran ( m e. M |-> ( A +s m ) ) = { z | E. m e. M z = ( A +s m ) } with typecode |-
213		ssltex1	$$⊢M{\ll }_{s}S\to M\in \mathrm{V}$$
214	2 213	syl	$$⊢\phi \to M\in \mathrm{V}$$
215	214	mptexd	Could not format ( ph -> ( m e. M |-> ( A +s m ) ) e. _V ) : No typesetting found for |- ( ph -> ( m e. M |-> ( A +s m ) ) e. _V ) with typecode |-
216		rnexg	Could not format ( ( m e. M |-> ( A +s m ) ) e. _V -> ran ( m e. M |-> ( A +s m ) ) e. _V ) : No typesetting found for |- ( ( m e. M |-> ( A +s m ) ) e. _V -> ran ( m e. M |-> ( A +s m ) ) e. _V ) with typecode |-
217	215 216	syl	Could not format ( ph -> ran ( m e. M |-> ( A +s m ) ) e. _V ) : No typesetting found for |- ( ph -> ran ( m e. M |-> ( A +s m ) ) e. _V ) with typecode |-
218	212 217	eqeltrrid	Could not format ( ph -> { z | E. m e. M z = ( A +s m ) } e. _V ) : No typesetting found for |- ( ph -> { z | E. m e. M z = ( A +s m ) } e. _V ) with typecode |-
219	210 218	unexd	Could not format ( ph -> ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) e. _V ) : No typesetting found for |- ( ph -> ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) e. _V ) with typecode |-
220		snex	Could not format { ( A +s B ) } e. _V : No typesetting found for |- { ( A +s B ) } e. _V with typecode |-
221	220	a1i	Could not format ( ph -> { ( A +s B ) } e. _V ) : No typesetting found for |- ( ph -> { ( A +s B ) } e. _V ) with typecode |-
222	24	sselda	$$⊢\left(\phi \wedge l\in L\right)\to l\in \mathrm{No}$$
223	8	adantr	$$⊢\left(\phi \wedge l\in L\right)\to B\in \mathrm{No}$$
224	222 223	addscld	Could not format ( ( ph /\ l e. L ) -> ( l +s B ) e. No ) : No typesetting found for |- ( ( ph /\ l e. L ) -> ( l +s B ) e. No ) with typecode |-
225		eleq1	Could not format ( y = ( l +s B ) -> ( y e. No <-> ( l +s B ) e. No ) ) : No typesetting found for |- ( y = ( l +s B ) -> ( y e. No <-> ( l +s B ) e. No ) ) with typecode |-
226	224 225	syl5ibrcom	Could not format ( ( ph /\ l e. L ) -> ( y = ( l +s B ) -> y e. No ) ) : No typesetting found for |- ( ( ph /\ l e. L ) -> ( y = ( l +s B ) -> y e. No ) ) with typecode |-
227	226	rexlimdva	Could not format ( ph -> ( E. l e. L y = ( l +s B ) -> y e. No ) ) : No typesetting found for |- ( ph -> ( E. l e. L y = ( l +s B ) -> y e. No ) ) with typecode |-
228	227	abssdv	Could not format ( ph -> { y | E. l e. L y = ( l +s B ) } C_ No ) : No typesetting found for |- ( ph -> { y | E. l e. L y = ( l +s B ) } C_ No ) with typecode |-
229	6	adantr	$$⊢\left(\phi \wedge m\in M\right)\to A\in \mathrm{No}$$
230	55	sselda	$$⊢\left(\phi \wedge m\in M\right)\to m\in \mathrm{No}$$
231	229 230	addscld	Could not format ( ( ph /\ m e. M ) -> ( A +s m ) e. No ) : No typesetting found for |- ( ( ph /\ m e. M ) -> ( A +s m ) e. No ) with typecode |-
232		eleq1	Could not format ( z = ( A +s m ) -> ( z e. No <-> ( A +s m ) e. No ) ) : No typesetting found for |- ( z = ( A +s m ) -> ( z e. No <-> ( A +s m ) e. No ) ) with typecode |-
233	231 232	syl5ibrcom	Could not format ( ( ph /\ m e. M ) -> ( z = ( A +s m ) -> z e. No ) ) : No typesetting found for |- ( ( ph /\ m e. M ) -> ( z = ( A +s m ) -> z e. No ) ) with typecode |-
234	233	rexlimdva	Could not format ( ph -> ( E. m e. M z = ( A +s m ) -> z e. No ) ) : No typesetting found for |- ( ph -> ( E. m e. M z = ( A +s m ) -> z e. No ) ) with typecode |-
235	234	abssdv	Could not format ( ph -> { z | E. m e. M z = ( A +s m ) } C_ No ) : No typesetting found for |- ( ph -> { z | E. m e. M z = ( A +s m ) } C_ No ) with typecode |-
236	228 235	unssd	Could not format ( ph -> ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) C_ No ) : No typesetting found for |- ( ph -> ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) C_ No ) with typecode |-
237	6 8	addscld	Could not format ( ph -> ( A +s B ) e. No ) : No typesetting found for |- ( ph -> ( A +s B ) e. No ) with typecode |-
238	237	snssd	Could not format ( ph -> { ( A +s B ) } C_ No ) : No typesetting found for |- ( ph -> { ( A +s B ) } C_ No ) with typecode |-
239		velsn	Could not format ( b e. { ( A +s B ) } <-> b = ( A +s B ) ) : No typesetting found for |- ( b e. { ( A +s B ) } <-> b = ( A +s B ) ) with typecode |-
240		elun	Could not format ( a e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) <-> ( a e. { y | E. l e. L y = ( l +s B ) } \/ a e. { z | E. m e. M z = ( A +s m ) } ) ) : No typesetting found for |- ( a e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) <-> ( a e. { y | E. l e. L y = ( l +s B ) } \/ a e. { z | E. m e. M z = ( A +s m ) } ) ) with typecode |-
241		vex	$$⊢a\in \mathrm{V}$$
242		eqeq1	Could not format ( y = a -> ( y = ( l +s B ) <-> a = ( l +s B ) ) ) : No typesetting found for |- ( y = a -> ( y = ( l +s B ) <-> a = ( l +s B ) ) ) with typecode |-
243	242	rexbidv	Could not format ( y = a -> ( E. l e. L y = ( l +s B ) <-> E. l e. L a = ( l +s B ) ) ) : No typesetting found for |- ( y = a -> ( E. l e. L y = ( l +s B ) <-> E. l e. L a = ( l +s B ) ) ) with typecode |-
244	241 243	elab	Could not format ( a e. { y | E. l e. L y = ( l +s B ) } <-> E. l e. L a = ( l +s B ) ) : No typesetting found for |- ( a e. { y | E. l e. L y = ( l +s B ) } <-> E. l e. L a = ( l +s B ) ) with typecode |-
245		eqeq1	Could not format ( z = a -> ( z = ( A +s m ) <-> a = ( A +s m ) ) ) : No typesetting found for |- ( z = a -> ( z = ( A +s m ) <-> a = ( A +s m ) ) ) with typecode |-
246	245	rexbidv	Could not format ( z = a -> ( E. m e. M z = ( A +s m ) <-> E. m e. M a = ( A +s m ) ) ) : No typesetting found for |- ( z = a -> ( E. m e. M z = ( A +s m ) <-> E. m e. M a = ( A +s m ) ) ) with typecode |-
247	241 246	elab	Could not format ( a e. { z | E. m e. M z = ( A +s m ) } <-> E. m e. M a = ( A +s m ) ) : No typesetting found for |- ( a e. { z | E. m e. M z = ( A +s m ) } <-> E. m e. M a = ( A +s m ) ) with typecode |-
248	244 247	orbi12i	Could not format ( ( a e. { y | E. l e. L y = ( l +s B ) } \/ a e. { z | E. m e. M z = ( A +s m ) } ) <-> ( E. l e. L a = ( l +s B ) \/ E. m e. M a = ( A +s m ) ) ) : No typesetting found for |- ( ( a e. { y | E. l e. L y = ( l +s B ) } \/ a e. { z | E. m e. M z = ( A +s m ) } ) <-> ( E. l e. L a = ( l +s B ) \/ E. m e. M a = ( A +s m ) ) ) with typecode |-
249	240 248	bitri	Could not format ( a e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) <-> ( E. l e. L a = ( l +s B ) \/ E. m e. M a = ( A +s m ) ) ) : No typesetting found for |- ( a e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) <-> ( E. l e. L a = ( l +s B ) \/ E. m e. M a = ( A +s m ) ) ) with typecode |-
250		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)$$
251	1 250	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)$$
252	251	simp2d	$$⊢\phi \to L{\ll }_s\left\{L{|}_{s}R\right\}$$
253	252	adantr	$$⊢\left(\phi \wedge l\in L\right)\to L{\ll }_s\left\{L{|}_{s}R\right\}$$
254		simpr	$$⊢\left(\phi \wedge l\in L\right)\to l\in L$$
255		ovex	$$⊢L{|}_{s}R\in \mathrm{V}$$
256	255	snid	$$⊢L{|}_{s}R\in \left\{L{|}_{s}R\right\}$$
257	256	a1i	$$⊢\left(\phi \wedge l\in L\right)\to L{|}_{s}R\in \left\{L{|}_{s}R\right\}$$
258	253 254 257	ssltsepcd	$$⊢\left(\phi \wedge l\in L\right)\to l{<}_s\left(L{|}_{s}R\right)$$
259	3	adantr	$$⊢\left(\phi \wedge l\in L\right)\to A=L{|}_{s}R$$
260	258 259	breqtrrd	$$⊢\left(\phi \wedge l\in L\right)\to l{<}_{s}A$$
261	6	adantr	$$⊢\left(\phi \wedge l\in L\right)\to A\in \mathrm{No}$$
262	222 261 223	sltadd1d	Could not format ( ( ph /\ l e. L ) -> ( l ( l +s B ) ( l ( l +s B )
263	260 262	mpbid	Could not format ( ( ph /\ l e. L ) -> ( l +s B ) ( l +s B )
264		breq1	Could not format ( a = ( l +s B ) -> ( a ( l +s B ) ( a ( l +s B )
265	263 264	syl5ibrcom	Could not format ( ( ph /\ l e. L ) -> ( a = ( l +s B ) -> a ( a = ( l +s B ) -> a
266	265	rexlimdva	Could not format ( ph -> ( E. l e. L a = ( l +s B ) -> a ( E. l e. L a = ( l +s B ) -> a
267		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)$$
268	2 267	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)$$
269	268	simp2d	$$⊢\phi \to M{\ll }_s\left\{M{|}_{s}S\right\}$$
270	269	adantr	$$⊢\left(\phi \wedge m\in M\right)\to M{\ll }_s\left\{M{|}_{s}S\right\}$$
271		simpr	$$⊢\left(\phi \wedge m\in M\right)\to m\in M$$
272		ovex	$$⊢M{|}_{s}S\in \mathrm{V}$$
273	272	snid	$$⊢M{|}_{s}S\in \left\{M{|}_{s}S\right\}$$
274	273	a1i	$$⊢\left(\phi \wedge m\in M\right)\to M{|}_{s}S\in \left\{M{|}_{s}S\right\}$$
275	270 271 274	ssltsepcd	$$⊢\left(\phi \wedge m\in M\right)\to m{<}_s\left(M{|}_{s}S\right)$$
276	4	adantr	$$⊢\left(\phi \wedge m\in M\right)\to B=M{|}_{s}S$$
277	275 276	breqtrrd	$$⊢\left(\phi \wedge m\in M\right)\to m{<}_{s}B$$
278	8	adantr	$$⊢\left(\phi \wedge m\in M\right)\to B\in \mathrm{No}$$
279	230 278 229	sltadd2d	Could not format ( ( ph /\ m e. M ) -> ( m ( A +s m ) ( m ( A +s m )
280	277 279	mpbid	Could not format ( ( ph /\ m e. M ) -> ( A +s m ) ( A +s m )
281		breq1	Could not format ( a = ( A +s m ) -> ( a ( A +s m ) ( a ( A +s m )
282	280 281	syl5ibrcom	Could not format ( ( ph /\ m e. M ) -> ( a = ( A +s m ) -> a ( a = ( A +s m ) -> a
283	282	rexlimdva	Could not format ( ph -> ( E. m e. M a = ( A +s m ) -> a ( E. m e. M a = ( A +s m ) -> a
284	266 283	jaod	Could not format ( ph -> ( ( E. l e. L a = ( l +s B ) \/ E. m e. M a = ( A +s m ) ) -> a ( ( E. l e. L a = ( l +s B ) \/ E. m e. M a = ( A +s m ) ) -> a
285	249 284	biimtrid	Could not format ( ph -> ( a e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) -> a ( a e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) -> a
286	285	imp	Could not format ( ( ph /\ a e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ) -> a a
287		breq2	Could not format ( b = ( A +s B ) -> ( a a ( a a
288	286 287	syl5ibrcom	Could not format ( ( ph /\ a e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ) -> ( b = ( A +s B ) -> a ( b = ( A +s B ) -> a
289	239 288	biimtrid	Could not format ( ( ph /\ a e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) ) -> ( b e. { ( A +s B ) } -> a ( b e. { ( A +s B ) } -> a
290	289	3impia	Could not format ( ( ph /\ a e. ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) /\ b e. { ( A +s B ) } ) -> a a
291	219 221 236 238 290	ssltd	Could not format ( ph -> ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) < ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) <
292	10	sneqd	Could not format ( ph -> { ( A +s B ) } = { ( ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) |s ( { c | E. e e. ( _Right ` A ) c = ( e +s B ) } u. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } ) ) } ) : No typesetting found for |- ( ph -> { ( A +s B ) } = { ( ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) |s ( { c | E. e e. ( _Right ` A ) c = ( e +s B ) } u. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } ) ) } ) with typecode |-
293	291 292	breqtrd	Could not format ( ph -> ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) < ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) <
294		eqid	Could not format ( r e. R |-> ( r +s B ) ) = ( r e. R |-> ( r +s B ) ) : No typesetting found for |- ( r e. R |-> ( r +s B ) ) = ( r e. R |-> ( r +s B ) ) with typecode |-
295	294	rnmpt	Could not format ran ( r e. R |-> ( r +s B ) ) = { w | E. r e. R w = ( r +s B ) } : No typesetting found for |- ran ( r e. R |-> ( r +s B ) ) = { w | E. r e. R w = ( r +s B ) } with typecode |-
296		ssltex2	$$⊢L{\ll }_{s}R\to R\in \mathrm{V}$$
297	1 296	syl	$$⊢\phi \to R\in \mathrm{V}$$
298	297	mptexd	Could not format ( ph -> ( r e. R |-> ( r +s B ) ) e. _V ) : No typesetting found for |- ( ph -> ( r e. R |-> ( r +s B ) ) e. _V ) with typecode |-
299		rnexg	Could not format ( ( r e. R |-> ( r +s B ) ) e. _V -> ran ( r e. R |-> ( r +s B ) ) e. _V ) : No typesetting found for |- ( ( r e. R |-> ( r +s B ) ) e. _V -> ran ( r e. R |-> ( r +s B ) ) e. _V ) with typecode |-
300	298 299	syl	Could not format ( ph -> ran ( r e. R |-> ( r +s B ) ) e. _V ) : No typesetting found for |- ( ph -> ran ( r e. R |-> ( r +s B ) ) e. _V ) with typecode |-
301	295 300	eqeltrrid	Could not format ( ph -> { w | E. r e. R w = ( r +s B ) } e. _V ) : No typesetting found for |- ( ph -> { w | E. r e. R w = ( r +s B ) } e. _V ) with typecode |-
302		eqid	Could not format ( s e. S |-> ( A +s s ) ) = ( s e. S |-> ( A +s s ) ) : No typesetting found for |- ( s e. S |-> ( A +s s ) ) = ( s e. S |-> ( A +s s ) ) with typecode |-
303	302	rnmpt	Could not format ran ( s e. S |-> ( A +s s ) ) = { t | E. s e. S t = ( A +s s ) } : No typesetting found for |- ran ( s e. S |-> ( A +s s ) ) = { t | E. s e. S t = ( A +s s ) } with typecode |-
304		ssltex2	$$⊢M{\ll }_{s}S\to S\in \mathrm{V}$$
305	2 304	syl	$$⊢\phi \to S\in \mathrm{V}$$
306	305	mptexd	Could not format ( ph -> ( s e. S |-> ( A +s s ) ) e. _V ) : No typesetting found for |- ( ph -> ( s e. S |-> ( A +s s ) ) e. _V ) with typecode |-
307		rnexg	Could not format ( ( s e. S |-> ( A +s s ) ) e. _V -> ran ( s e. S |-> ( A +s s ) ) e. _V ) : No typesetting found for |- ( ( s e. S |-> ( A +s s ) ) e. _V -> ran ( s e. S |-> ( A +s s ) ) e. _V ) with typecode |-
308	306 307	syl	Could not format ( ph -> ran ( s e. S |-> ( A +s s ) ) e. _V ) : No typesetting found for |- ( ph -> ran ( s e. S |-> ( A +s s ) ) e. _V ) with typecode |-
309	303 308	eqeltrrid	Could not format ( ph -> { t | E. s e. S t = ( A +s s ) } e. _V ) : No typesetting found for |- ( ph -> { t | E. s e. S t = ( A +s s ) } e. _V ) with typecode |-
310	301 309	unexd	Could not format ( ph -> ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) e. _V ) : No typesetting found for |- ( ph -> ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) e. _V ) with typecode |-
311	113	sselda	$$⊢\left(\phi \wedge r\in R\right)\to r\in \mathrm{No}$$
312	8	adantr	$$⊢\left(\phi \wedge r\in R\right)\to B\in \mathrm{No}$$
313	311 312	addscld	Could not format ( ( ph /\ r e. R ) -> ( r +s B ) e. No ) : No typesetting found for |- ( ( ph /\ r e. R ) -> ( r +s B ) e. No ) with typecode |-
314		eleq1	Could not format ( w = ( r +s B ) -> ( w e. No <-> ( r +s B ) e. No ) ) : No typesetting found for |- ( w = ( r +s B ) -> ( w e. No <-> ( r +s B ) e. No ) ) with typecode |-
315	313 314	syl5ibrcom	Could not format ( ( ph /\ r e. R ) -> ( w = ( r +s B ) -> w e. No ) ) : No typesetting found for |- ( ( ph /\ r e. R ) -> ( w = ( r +s B ) -> w e. No ) ) with typecode |-
316	315	rexlimdva	Could not format ( ph -> ( E. r e. R w = ( r +s B ) -> w e. No ) ) : No typesetting found for |- ( ph -> ( E. r e. R w = ( r +s B ) -> w e. No ) ) with typecode |-
317	316	abssdv	Could not format ( ph -> { w | E. r e. R w = ( r +s B ) } C_ No ) : No typesetting found for |- ( ph -> { w | E. r e. R w = ( r +s B ) } C_ No ) with typecode |-
318	6	adantr	$$⊢\left(\phi \wedge s\in S\right)\to A\in \mathrm{No}$$
319	144	sselda	$$⊢\left(\phi \wedge s\in S\right)\to s\in \mathrm{No}$$
320	318 319	addscld	Could not format ( ( ph /\ s e. S ) -> ( A +s s ) e. No ) : No typesetting found for |- ( ( ph /\ s e. S ) -> ( A +s s ) e. No ) with typecode |-
321		eleq1	Could not format ( t = ( A +s s ) -> ( t e. No <-> ( A +s s ) e. No ) ) : No typesetting found for |- ( t = ( A +s s ) -> ( t e. No <-> ( A +s s ) e. No ) ) with typecode |-
322	320 321	syl5ibrcom	Could not format ( ( ph /\ s e. S ) -> ( t = ( A +s s ) -> t e. No ) ) : No typesetting found for |- ( ( ph /\ s e. S ) -> ( t = ( A +s s ) -> t e. No ) ) with typecode |-
323	322	rexlimdva	Could not format ( ph -> ( E. s e. S t = ( A +s s ) -> t e. No ) ) : No typesetting found for |- ( ph -> ( E. s e. S t = ( A +s s ) -> t e. No ) ) with typecode |-
324	323	abssdv	Could not format ( ph -> { t | E. s e. S t = ( A +s s ) } C_ No ) : No typesetting found for |- ( ph -> { t | E. s e. S t = ( A +s s ) } C_ No ) with typecode |-
325	317 324	unssd	Could not format ( ph -> ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) C_ No ) : No typesetting found for |- ( ph -> ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) C_ No ) with typecode |-
326		velsn	Could not format ( a e. { ( A +s B ) } <-> a = ( A +s B ) ) : No typesetting found for |- ( a e. { ( A +s B ) } <-> a = ( A +s B ) ) with typecode |-
327		elun	Could not format ( b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) <-> ( b e. { w | E. r e. R w = ( r +s B ) } \/ b e. { t | E. s e. S t = ( A +s s ) } ) ) : No typesetting found for |- ( b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) <-> ( b e. { w | E. r e. R w = ( r +s B ) } \/ b e. { t | E. s e. S t = ( A +s s ) } ) ) with typecode |-
328		vex	$$⊢b\in \mathrm{V}$$
329	328 125	elab	Could not format ( b e. { w | E. r e. R w = ( r +s B ) } <-> E. r e. R b = ( r +s B ) ) : No typesetting found for |- ( b e. { w | E. r e. R w = ( r +s B ) } <-> E. r e. R b = ( r +s B ) ) with typecode |-
330	328 156	elab	Could not format ( b e. { t | E. s e. S t = ( A +s s ) } <-> E. s e. S b = ( A +s s ) ) : No typesetting found for |- ( b e. { t | E. s e. S t = ( A +s s ) } <-> E. s e. S b = ( A +s s ) ) with typecode |-
331	329 330	orbi12i	Could not format ( ( b e. { w | E. r e. R w = ( r +s B ) } \/ b e. { t | E. s e. S t = ( A +s s ) } ) <-> ( E. r e. R b = ( r +s B ) \/ E. s e. S b = ( A +s s ) ) ) : No typesetting found for |- ( ( b e. { w | E. r e. R w = ( r +s B ) } \/ b e. { t | E. s e. S t = ( A +s s ) } ) <-> ( E. r e. R b = ( r +s B ) \/ E. s e. S b = ( A +s s ) ) ) with typecode |-
332	327 331	bitri	Could not format ( b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) <-> ( E. r e. R b = ( r +s B ) \/ E. s e. S b = ( A +s s ) ) ) : No typesetting found for |- ( b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) <-> ( E. r e. R b = ( r +s B ) \/ E. s e. S b = ( A +s s ) ) ) with typecode |-
333	3	adantr	$$⊢\left(\phi \wedge r\in R\right)\to A=L{|}_{s}R$$
334	251	simp3d	$$⊢\phi \to \left\{L{|}_{s}R\right\}{\ll }_{s}R$$
335	334	adantr	$$⊢\left(\phi \wedge r\in R\right)\to \left\{L{|}_{s}R\right\}{\ll }_{s}R$$
336	256	a1i	$$⊢\left(\phi \wedge r\in R\right)\to L{|}_{s}R\in \left\{L{|}_{s}R\right\}$$
337		simpr	$$⊢\left(\phi \wedge r\in R\right)\to r\in R$$
338	335 336 337	ssltsepcd	$$⊢\left(\phi \wedge r\in R\right)\to \left(L{|}_{s}R\right){<}_{s}r$$
339	333 338	eqbrtrd	$$⊢\left(\phi \wedge r\in R\right)\to A{<}_{s}r$$
340	6	adantr	$$⊢\left(\phi \wedge r\in R\right)\to A\in \mathrm{No}$$
341	340 311 312	sltadd1d	Could not format ( ( ph /\ r e. R ) -> ( A ( A +s B ) ( A ( A +s B )
342	339 341	mpbid	Could not format ( ( ph /\ r e. R ) -> ( A +s B ) ( A +s B )
343		breq2	Could not format ( b = ( r +s B ) -> ( ( A +s B ) ( A +s B ) ( ( A +s B ) ( A +s B )
344	342 343	syl5ibrcom	Could not format ( ( ph /\ r e. R ) -> ( b = ( r +s B ) -> ( A +s B ) ( b = ( r +s B ) -> ( A +s B )
345	344	rexlimdva	Could not format ( ph -> ( E. r e. R b = ( r +s B ) -> ( A +s B ) ( E. r e. R b = ( r +s B ) -> ( A +s B )
346	4	adantr	$$⊢\left(\phi \wedge s\in S\right)\to B=M{|}_{s}S$$
347	268	simp3d	$$⊢\phi \to \left\{M{|}_{s}S\right\}{\ll }_{s}S$$
348	347	adantr	$$⊢\left(\phi \wedge s\in S\right)\to \left\{M{|}_{s}S\right\}{\ll }_{s}S$$
349	273	a1i	$$⊢\left(\phi \wedge s\in S\right)\to M{|}_{s}S\in \left\{M{|}_{s}S\right\}$$
350		simpr	$$⊢\left(\phi \wedge s\in S\right)\to s\in S$$
351	348 349 350	ssltsepcd	$$⊢\left(\phi \wedge s\in S\right)\to \left(M{|}_{s}S\right){<}_{s}s$$
352	346 351	eqbrtrd	$$⊢\left(\phi \wedge s\in S\right)\to B{<}_{s}s$$
353	8	adantr	$$⊢\left(\phi \wedge s\in S\right)\to B\in \mathrm{No}$$
354	353 319 318	sltadd2d	Could not format ( ( ph /\ s e. S ) -> ( B ( A +s B ) ( B ( A +s B )
355	352 354	mpbid	Could not format ( ( ph /\ s e. S ) -> ( A +s B ) ( A +s B )
356		breq2	Could not format ( b = ( A +s s ) -> ( ( A +s B ) ( A +s B ) ( ( A +s B ) ( A +s B )
357	355 356	syl5ibrcom	Could not format ( ( ph /\ s e. S ) -> ( b = ( A +s s ) -> ( A +s B ) ( b = ( A +s s ) -> ( A +s B )
358	357	rexlimdva	Could not format ( ph -> ( E. s e. S b = ( A +s s ) -> ( A +s B ) ( E. s e. S b = ( A +s s ) -> ( A +s B )
359	345 358	jaod	Could not format ( ph -> ( ( E. r e. R b = ( r +s B ) \/ E. s e. S b = ( A +s s ) ) -> ( A +s B ) ( ( E. r e. R b = ( r +s B ) \/ E. s e. S b = ( A +s s ) ) -> ( A +s B )
360	332 359	biimtrid	Could not format ( ph -> ( b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) -> ( A +s B ) ( b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) -> ( A +s B )
361	360	imp	Could not format ( ( ph /\ b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) ) -> ( A +s B ) ( A +s B )
362		breq1	Could not format ( a = ( A +s B ) -> ( a ( A +s B ) ( a ( A +s B )
363	361 362	syl5ibrcom	Could not format ( ( ph /\ b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) ) -> ( a = ( A +s B ) -> a ( a = ( A +s B ) -> a
364	363	ex	Could not format ( ph -> ( b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) -> ( a = ( A +s B ) -> a ( b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) -> ( a = ( A +s B ) -> a
365	364	com23	Could not format ( ph -> ( a = ( A +s B ) -> ( b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) -> a ( a = ( A +s B ) -> ( b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) -> a
366	326 365	biimtrid	Could not format ( ph -> ( a e. { ( A +s B ) } -> ( b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) -> a ( a e. { ( A +s B ) } -> ( b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) -> a
367	366	3imp	Could not format ( ( ph /\ a e. { ( A +s B ) } /\ b e. ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) ) -> a a
368	221 310 238 325 367	ssltd	Could not format ( ph -> { ( A +s B ) } < { ( A +s B ) } <
369	292 368	eqbrtrrd	Could not format ( ph -> { ( ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) |s ( { c | E. e e. ( _Right ` A ) c = ( e +s B ) } u. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } ) ) } < { ( ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) |s ( { c | E. e e. ( _Right ` A ) c = ( e +s B ) } u. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } ) ) } <
370	18 110 202 293 369	cofcut1d	Could not format ( ph -> ( ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) |s ( { c | E. e e. ( _Right ` A ) c = ( e +s B ) } u. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } ) ) = ( ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) |s ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) ) ) : No typesetting found for |- ( ph -> ( ( { a | E. p e. ( _Left ` A ) a = ( p +s B ) } u. { b | E. q e. ( _Left ` B ) b = ( A +s q ) } ) |s ( { c | E. e e. ( _Right ` A ) c = ( e +s B ) } u. { d | E. f e. ( _Right ` B ) d = ( A +s f ) } ) ) = ( ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) |s ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) ) ) with typecode |-
371	10 370	eqtrd	Could not format ( ph -> ( A +s B ) = ( ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) |s ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) ) ) : No typesetting found for |- ( ph -> ( A +s B ) = ( ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) |s ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) ) ) with typecode |-