Theorem negsunif

Description: Uniformity property for surreal negation. If L and R are any cut that represents A , then they may be used instead of (LeftA ) and ( RightA ) in the definition of negation. (Contributed by Scott Fenton, 14-Feb-2025)

	Ref	Expression
Hypotheses	negsunif.1	$$⊢\phi \to L{\ll }_{s}R$$
	negsunif.2	$$⊢\phi \to A=L{|}_{s}R$$
Assertion	negsunif	Could not format assertion : No typesetting found for |- ( ph -> ( -us ` A ) = ( ( -us " R ) |s ( -us " L ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		negsunif.1	$$⊢\phi \to L{\ll }_{s}R$$
2		negsunif.2	$$⊢\phi \to A=L{|}_{s}R$$
3	1	scutcld	$$⊢\phi \to L{|}_{s}R\in \mathrm{No}$$
4	2 3	eqeltrd	$$⊢\phi \to A\in \mathrm{No}$$
5		negsval	Could not format ( A e. No -> ( -us ` A ) = ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) ) : No typesetting found for |- ( A e. No -> ( -us ` A ) = ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) ) with typecode |-
6	4 5	syl	Could not format ( ph -> ( -us ` A ) = ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) ) : No typesetting found for |- ( ph -> ( -us ` A ) = ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) ) with typecode |-
7		negscut2	Could not format ( A e. No -> ( -us " ( _Right ` A ) ) < ( -us " ( _Right ` A ) ) <
8	4 7	syl	Could not format ( ph -> ( -us " ( _Right ` A ) ) < ( -us " ( _Right ` A ) ) <
9	1 2	cofcutr2d	Could not format ( ph -> A. c e. ( _Right ` A ) E. d e. R d <_s c ) : No typesetting found for |- ( ph -> A. c e. ( _Right ` A ) E. d e. R d <_s c ) with typecode |-
10		negsfn	Could not format -us Fn No : No typesetting found for |- -us Fn No with typecode |-
11		ssltss2	$$⊢L{\ll }_{s}R\to R\subseteq \mathrm{No}$$
12	1 11	syl	$$⊢\phi \to R\subseteq \mathrm{No}$$
13		breq2	Could not format ( b = ( -us ` d ) -> ( ( -us ` c ) <_s b <-> ( -us ` c ) <_s ( -us ` d ) ) ) : No typesetting found for |- ( b = ( -us ` d ) -> ( ( -us ` c ) <_s b <-> ( -us ` c ) <_s ( -us ` d ) ) ) with typecode |-
14	13	imaeqsexv	Could not format ( ( -us Fn No /\ R C_ No ) -> ( E. b e. ( -us " R ) ( -us ` c ) <_s b <-> E. d e. R ( -us ` c ) <_s ( -us ` d ) ) ) : No typesetting found for |- ( ( -us Fn No /\ R C_ No ) -> ( E. b e. ( -us " R ) ( -us ` c ) <_s b <-> E. d e. R ( -us ` c ) <_s ( -us ` d ) ) ) with typecode |-
15	10 12 14	sylancr	Could not format ( ph -> ( E. b e. ( -us " R ) ( -us ` c ) <_s b <-> E. d e. R ( -us ` c ) <_s ( -us ` d ) ) ) : No typesetting found for |- ( ph -> ( E. b e. ( -us " R ) ( -us ` c ) <_s b <-> E. d e. R ( -us ` c ) <_s ( -us ` d ) ) ) with typecode |-
16	15	ralbidv	Could not format ( ph -> ( A. c e. ( _Right ` A ) E. b e. ( -us " R ) ( -us ` c ) <_s b <-> A. c e. ( _Right ` A ) E. d e. R ( -us ` c ) <_s ( -us ` d ) ) ) : No typesetting found for |- ( ph -> ( A. c e. ( _Right ` A ) E. b e. ( -us " R ) ( -us ` c ) <_s b <-> A. c e. ( _Right ` A ) E. d e. R ( -us ` c ) <_s ( -us ` d ) ) ) with typecode |-
17	12	adantr	Could not format ( ( ph /\ c e. ( _Right ` A ) ) -> R C_ No ) : No typesetting found for |- ( ( ph /\ c e. ( _Right ` A ) ) -> R C_ No ) with typecode |-
18	17	sselda	Could not format ( ( ( ph /\ c e. ( _Right ` A ) ) /\ d e. R ) -> d e. No ) : No typesetting found for |- ( ( ( ph /\ c e. ( _Right ` A ) ) /\ d e. R ) -> d e. No ) with typecode |-
19		rightssno	Could not format ( _Right ` A ) C_ No : No typesetting found for |- ( _Right ` A ) C_ No with typecode |-
20	19	sseli	Could not format ( c e. ( _Right ` A ) -> c e. No ) : No typesetting found for |- ( c e. ( _Right ` A ) -> c e. No ) with typecode |-
21	20	ad2antlr	Could not format ( ( ( ph /\ c e. ( _Right ` A ) ) /\ d e. R ) -> c e. No ) : No typesetting found for |- ( ( ( ph /\ c e. ( _Right ` A ) ) /\ d e. R ) -> c e. No ) with typecode |-
22	18 21	slenegd	Could not format ( ( ( ph /\ c e. ( _Right ` A ) ) /\ d e. R ) -> ( d <_s c <-> ( -us ` c ) <_s ( -us ` d ) ) ) : No typesetting found for |- ( ( ( ph /\ c e. ( _Right ` A ) ) /\ d e. R ) -> ( d <_s c <-> ( -us ` c ) <_s ( -us ` d ) ) ) with typecode |-
23	22	rexbidva	Could not format ( ( ph /\ c e. ( _Right ` A ) ) -> ( E. d e. R d <_s c <-> E. d e. R ( -us ` c ) <_s ( -us ` d ) ) ) : No typesetting found for |- ( ( ph /\ c e. ( _Right ` A ) ) -> ( E. d e. R d <_s c <-> E. d e. R ( -us ` c ) <_s ( -us ` d ) ) ) with typecode |-
24	23	ralbidva	Could not format ( ph -> ( A. c e. ( _Right ` A ) E. d e. R d <_s c <-> A. c e. ( _Right ` A ) E. d e. R ( -us ` c ) <_s ( -us ` d ) ) ) : No typesetting found for |- ( ph -> ( A. c e. ( _Right ` A ) E. d e. R d <_s c <-> A. c e. ( _Right ` A ) E. d e. R ( -us ` c ) <_s ( -us ` d ) ) ) with typecode |-
25	16 24	bitr4d	Could not format ( ph -> ( A. c e. ( _Right ` A ) E. b e. ( -us " R ) ( -us ` c ) <_s b <-> A. c e. ( _Right ` A ) E. d e. R d <_s c ) ) : No typesetting found for |- ( ph -> ( A. c e. ( _Right ` A ) E. b e. ( -us " R ) ( -us ` c ) <_s b <-> A. c e. ( _Right ` A ) E. d e. R d <_s c ) ) with typecode |-
26	9 25	mpbird	Could not format ( ph -> A. c e. ( _Right ` A ) E. b e. ( -us " R ) ( -us ` c ) <_s b ) : No typesetting found for |- ( ph -> A. c e. ( _Right ` A ) E. b e. ( -us " R ) ( -us ` c ) <_s b ) with typecode |-
27		breq1	Could not format ( a = ( -us ` c ) -> ( a <_s b <-> ( -us ` c ) <_s b ) ) : No typesetting found for |- ( a = ( -us ` c ) -> ( a <_s b <-> ( -us ` c ) <_s b ) ) with typecode |-
28	27	rexbidv	Could not format ( a = ( -us ` c ) -> ( E. b e. ( -us " R ) a <_s b <-> E. b e. ( -us " R ) ( -us ` c ) <_s b ) ) : No typesetting found for |- ( a = ( -us ` c ) -> ( E. b e. ( -us " R ) a <_s b <-> E. b e. ( -us " R ) ( -us ` c ) <_s b ) ) with typecode |-
29	28	imaeqsalv	Could not format ( ( -us Fn No /\ ( _Right ` A ) C_ No ) -> ( A. a e. ( -us " ( _Right ` A ) ) E. b e. ( -us " R ) a <_s b <-> A. c e. ( _Right ` A ) E. b e. ( -us " R ) ( -us ` c ) <_s b ) ) : No typesetting found for |- ( ( -us Fn No /\ ( _Right ` A ) C_ No ) -> ( A. a e. ( -us " ( _Right ` A ) ) E. b e. ( -us " R ) a <_s b <-> A. c e. ( _Right ` A ) E. b e. ( -us " R ) ( -us ` c ) <_s b ) ) with typecode |-
30	10 19 29	mp2an	Could not format ( A. a e. ( -us " ( _Right ` A ) ) E. b e. ( -us " R ) a <_s b <-> A. c e. ( _Right ` A ) E. b e. ( -us " R ) ( -us ` c ) <_s b ) : No typesetting found for |- ( A. a e. ( -us " ( _Right ` A ) ) E. b e. ( -us " R ) a <_s b <-> A. c e. ( _Right ` A ) E. b e. ( -us " R ) ( -us ` c ) <_s b ) with typecode |-
31	26 30	sylibr	Could not format ( ph -> A. a e. ( -us " ( _Right ` A ) ) E. b e. ( -us " R ) a <_s b ) : No typesetting found for |- ( ph -> A. a e. ( -us " ( _Right ` A ) ) E. b e. ( -us " R ) a <_s b ) with typecode |-
32	1 2	cofcutr1d	Could not format ( ph -> A. c e. ( _Left ` A ) E. d e. L c <_s d ) : No typesetting found for |- ( ph -> A. c e. ( _Left ` A ) E. d e. L c <_s d ) with typecode |-
33		ssltss1	$$⊢L{\ll }_{s}R\to L\subseteq \mathrm{No}$$
34	1 33	syl	$$⊢\phi \to L\subseteq \mathrm{No}$$
35		breq1	Could not format ( b = ( -us ` d ) -> ( b <_s ( -us ` c ) <-> ( -us ` d ) <_s ( -us ` c ) ) ) : No typesetting found for |- ( b = ( -us ` d ) -> ( b <_s ( -us ` c ) <-> ( -us ` d ) <_s ( -us ` c ) ) ) with typecode |-
36	35	imaeqsexv	Could not format ( ( -us Fn No /\ L C_ No ) -> ( E. b e. ( -us " L ) b <_s ( -us ` c ) <-> E. d e. L ( -us ` d ) <_s ( -us ` c ) ) ) : No typesetting found for |- ( ( -us Fn No /\ L C_ No ) -> ( E. b e. ( -us " L ) b <_s ( -us ` c ) <-> E. d e. L ( -us ` d ) <_s ( -us ` c ) ) ) with typecode |-
37	10 34 36	sylancr	Could not format ( ph -> ( E. b e. ( -us " L ) b <_s ( -us ` c ) <-> E. d e. L ( -us ` d ) <_s ( -us ` c ) ) ) : No typesetting found for |- ( ph -> ( E. b e. ( -us " L ) b <_s ( -us ` c ) <-> E. d e. L ( -us ` d ) <_s ( -us ` c ) ) ) with typecode |-
38	37	ralbidv	Could not format ( ph -> ( A. c e. ( _Left ` A ) E. b e. ( -us " L ) b <_s ( -us ` c ) <-> A. c e. ( _Left ` A ) E. d e. L ( -us ` d ) <_s ( -us ` c ) ) ) : No typesetting found for |- ( ph -> ( A. c e. ( _Left ` A ) E. b e. ( -us " L ) b <_s ( -us ` c ) <-> A. c e. ( _Left ` A ) E. d e. L ( -us ` d ) <_s ( -us ` c ) ) ) with typecode |-
39		leftssno	Could not format ( _Left ` A ) C_ No : No typesetting found for |- ( _Left ` A ) C_ No with typecode |-
40	39	sseli	Could not format ( c e. ( _Left ` A ) -> c e. No ) : No typesetting found for |- ( c e. ( _Left ` A ) -> c e. No ) with typecode |-
41	40	ad2antlr	Could not format ( ( ( ph /\ c e. ( _Left ` A ) ) /\ d e. L ) -> c e. No ) : No typesetting found for |- ( ( ( ph /\ c e. ( _Left ` A ) ) /\ d e. L ) -> c e. No ) with typecode |-
42	34	adantr	Could not format ( ( ph /\ c e. ( _Left ` A ) ) -> L C_ No ) : No typesetting found for |- ( ( ph /\ c e. ( _Left ` A ) ) -> L C_ No ) with typecode |-
43	42	sselda	Could not format ( ( ( ph /\ c e. ( _Left ` A ) ) /\ d e. L ) -> d e. No ) : No typesetting found for |- ( ( ( ph /\ c e. ( _Left ` A ) ) /\ d e. L ) -> d e. No ) with typecode |-
44	41 43	slenegd	Could not format ( ( ( ph /\ c e. ( _Left ` A ) ) /\ d e. L ) -> ( c <_s d <-> ( -us ` d ) <_s ( -us ` c ) ) ) : No typesetting found for |- ( ( ( ph /\ c e. ( _Left ` A ) ) /\ d e. L ) -> ( c <_s d <-> ( -us ` d ) <_s ( -us ` c ) ) ) with typecode |-
45	44	rexbidva	Could not format ( ( ph /\ c e. ( _Left ` A ) ) -> ( E. d e. L c <_s d <-> E. d e. L ( -us ` d ) <_s ( -us ` c ) ) ) : No typesetting found for |- ( ( ph /\ c e. ( _Left ` A ) ) -> ( E. d e. L c <_s d <-> E. d e. L ( -us ` d ) <_s ( -us ` c ) ) ) with typecode |-
46	45	ralbidva	Could not format ( ph -> ( A. c e. ( _Left ` A ) E. d e. L c <_s d <-> A. c e. ( _Left ` A ) E. d e. L ( -us ` d ) <_s ( -us ` c ) ) ) : No typesetting found for |- ( ph -> ( A. c e. ( _Left ` A ) E. d e. L c <_s d <-> A. c e. ( _Left ` A ) E. d e. L ( -us ` d ) <_s ( -us ` c ) ) ) with typecode |-
47	38 46	bitr4d	Could not format ( ph -> ( A. c e. ( _Left ` A ) E. b e. ( -us " L ) b <_s ( -us ` c ) <-> A. c e. ( _Left ` A ) E. d e. L c <_s d ) ) : No typesetting found for |- ( ph -> ( A. c e. ( _Left ` A ) E. b e. ( -us " L ) b <_s ( -us ` c ) <-> A. c e. ( _Left ` A ) E. d e. L c <_s d ) ) with typecode |-
48	32 47	mpbird	Could not format ( ph -> A. c e. ( _Left ` A ) E. b e. ( -us " L ) b <_s ( -us ` c ) ) : No typesetting found for |- ( ph -> A. c e. ( _Left ` A ) E. b e. ( -us " L ) b <_s ( -us ` c ) ) with typecode |-
49		breq2	Could not format ( a = ( -us ` c ) -> ( b <_s a <-> b <_s ( -us ` c ) ) ) : No typesetting found for |- ( a = ( -us ` c ) -> ( b <_s a <-> b <_s ( -us ` c ) ) ) with typecode |-
50	49	rexbidv	Could not format ( a = ( -us ` c ) -> ( E. b e. ( -us " L ) b <_s a <-> E. b e. ( -us " L ) b <_s ( -us ` c ) ) ) : No typesetting found for |- ( a = ( -us ` c ) -> ( E. b e. ( -us " L ) b <_s a <-> E. b e. ( -us " L ) b <_s ( -us ` c ) ) ) with typecode |-
51	50	imaeqsalv	Could not format ( ( -us Fn No /\ ( _Left ` A ) C_ No ) -> ( A. a e. ( -us " ( _Left ` A ) ) E. b e. ( -us " L ) b <_s a <-> A. c e. ( _Left ` A ) E. b e. ( -us " L ) b <_s ( -us ` c ) ) ) : No typesetting found for |- ( ( -us Fn No /\ ( _Left ` A ) C_ No ) -> ( A. a e. ( -us " ( _Left ` A ) ) E. b e. ( -us " L ) b <_s a <-> A. c e. ( _Left ` A ) E. b e. ( -us " L ) b <_s ( -us ` c ) ) ) with typecode |-
52	10 39 51	mp2an	Could not format ( A. a e. ( -us " ( _Left ` A ) ) E. b e. ( -us " L ) b <_s a <-> A. c e. ( _Left ` A ) E. b e. ( -us " L ) b <_s ( -us ` c ) ) : No typesetting found for |- ( A. a e. ( -us " ( _Left ` A ) ) E. b e. ( -us " L ) b <_s a <-> A. c e. ( _Left ` A ) E. b e. ( -us " L ) b <_s ( -us ` c ) ) with typecode |-
53	48 52	sylibr	Could not format ( ph -> A. a e. ( -us " ( _Left ` A ) ) E. b e. ( -us " L ) b <_s a ) : No typesetting found for |- ( ph -> A. a e. ( -us " ( _Left ` A ) ) E. b e. ( -us " L ) b <_s a ) with typecode |-
54		fnfun	Could not format ( -us Fn No -> Fun -us ) : No typesetting found for |- ( -us Fn No -> Fun -us ) with typecode |-
55	10 54	ax-mp	Could not format Fun -us : No typesetting found for |- Fun -us with typecode |-
56		ssltex2	$$⊢L{\ll }_{s}R\to R\in \mathrm{V}$$
57	1 56	syl	$$⊢\phi \to R\in \mathrm{V}$$
58		funimaexg	Could not format ( ( Fun -us /\ R e. _V ) -> ( -us " R ) e. _V ) : No typesetting found for |- ( ( Fun -us /\ R e. _V ) -> ( -us " R ) e. _V ) with typecode |-
59	55 57 58	sylancr	Could not format ( ph -> ( -us " R ) e. _V ) : No typesetting found for |- ( ph -> ( -us " R ) e. _V ) with typecode |-
60		snex	Could not format { ( -us ` A ) } e. _V : No typesetting found for |- { ( -us ` A ) } e. _V with typecode |-
61	60	a1i	Could not format ( ph -> { ( -us ` A ) } e. _V ) : No typesetting found for |- ( ph -> { ( -us ` A ) } e. _V ) with typecode |-
62		imassrn	Could not format ( -us " R ) C_ ran -us : No typesetting found for |- ( -us " R ) C_ ran -us with typecode |-
63		negsfo	Could not format -us : No -onto-> No : No typesetting found for |- -us : No -onto-> No with typecode |-
64		forn	Could not format ( -us : No -onto-> No -> ran -us = No ) : No typesetting found for |- ( -us : No -onto-> No -> ran -us = No ) with typecode |-
65	63 64	ax-mp	Could not format ran -us = No : No typesetting found for |- ran -us = No with typecode |-
66	62 65	sseqtri	Could not format ( -us " R ) C_ No : No typesetting found for |- ( -us " R ) C_ No with typecode |-
67	66	a1i	Could not format ( ph -> ( -us " R ) C_ No ) : No typesetting found for |- ( ph -> ( -us " R ) C_ No ) with typecode |-
68	4	negscld	Could not format ( ph -> ( -us ` A ) e. No ) : No typesetting found for |- ( ph -> ( -us ` A ) e. No ) with typecode |-
69	68	snssd	Could not format ( ph -> { ( -us ` A ) } C_ No ) : No typesetting found for |- ( ph -> { ( -us ` A ) } C_ No ) with typecode |-
70		velsn	Could not format ( a e. { ( -us ` A ) } <-> a = ( -us ` A ) ) : No typesetting found for |- ( a e. { ( -us ` A ) } <-> a = ( -us ` A ) ) with typecode |-
71		fvelimab	Could not format ( ( -us Fn No /\ R C_ No ) -> ( b e. ( -us " R ) <-> E. d e. R ( -us ` d ) = b ) ) : No typesetting found for |- ( ( -us Fn No /\ R C_ No ) -> ( b e. ( -us " R ) <-> E. d e. R ( -us ` d ) = b ) ) with typecode |-
72	10 12 71	sylancr	Could not format ( ph -> ( b e. ( -us " R ) <-> E. d e. R ( -us ` d ) = b ) ) : No typesetting found for |- ( ph -> ( b e. ( -us " R ) <-> E. d e. R ( -us ` d ) = b ) ) with typecode |-
73	2	sneqd	$$⊢\phi \to \left\{A\right\}=\left\{L{|}_{s}R\right\}$$
74	73	adantr	$$⊢\left(\phi \wedge d\in R\right)\to \left\{A\right\}=\left\{L{|}_{s}R\right\}$$
75		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)$$
76	1 75	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)$$
77	76	simp3d	$$⊢\phi \to \left\{L{|}_{s}R\right\}{\ll }_{s}R$$
78	77	adantr	$$⊢\left(\phi \wedge d\in R\right)\to \left\{L{|}_{s}R\right\}{\ll }_{s}R$$
79	74 78	eqbrtrd	$$⊢\left(\phi \wedge d\in R\right)\to \left\{A\right\}{\ll }_{s}R$$
80		snidg	$$⊢A\in \mathrm{No}\to A\in \left\{A\right\}$$
81	4 80	syl	$$⊢\phi \to A\in \left\{A\right\}$$
82	81	adantr	$$⊢\left(\phi \wedge d\in R\right)\to A\in \left\{A\right\}$$
83		simpr	$$⊢\left(\phi \wedge d\in R\right)\to d\in R$$
84	79 82 83	ssltsepcd	$$⊢\left(\phi \wedge d\in R\right)\to A{<}_{s}d$$
85	4	adantr	$$⊢\left(\phi \wedge d\in R\right)\to A\in \mathrm{No}$$
86	12	sselda	$$⊢\left(\phi \wedge d\in R\right)\to d\in \mathrm{No}$$
87	85 86	sltnegd	Could not format ( ( ph /\ d e. R ) -> ( A ( -us ` d ) ( A ( -us ` d )
88	84 87	mpbid	Could not format ( ( ph /\ d e. R ) -> ( -us ` d ) ( -us ` d )
89		breq1	Could not format ( ( -us ` d ) = b -> ( ( -us ` d ) b ( ( -us ` d ) b
90	88 89	syl5ibcom	Could not format ( ( ph /\ d e. R ) -> ( ( -us ` d ) = b -> b ( ( -us ` d ) = b -> b
91	90	rexlimdva	Could not format ( ph -> ( E. d e. R ( -us ` d ) = b -> b ( E. d e. R ( -us ` d ) = b -> b
92	72 91	sylbid	Could not format ( ph -> ( b e. ( -us " R ) -> b ( b e. ( -us " R ) -> b
93		breq2	Could not format ( a = ( -us ` A ) -> ( b b ( b b
94	93	imbi2d	Could not format ( a = ( -us ` A ) -> ( ( b e. ( -us " R ) -> b ( b e. ( -us " R ) -> b ( ( b e. ( -us " R ) -> b ( b e. ( -us " R ) -> b
95	92 94	syl5ibrcom	Could not format ( ph -> ( a = ( -us ` A ) -> ( b e. ( -us " R ) -> b ( a = ( -us ` A ) -> ( b e. ( -us " R ) -> b
96	70 95	biimtrid	Could not format ( ph -> ( a e. { ( -us ` A ) } -> ( b e. ( -us " R ) -> b ( a e. { ( -us ` A ) } -> ( b e. ( -us " R ) -> b
97	96	3imp	Could not format ( ( ph /\ a e. { ( -us ` A ) } /\ b e. ( -us " R ) ) -> b b
98	97	3com23	Could not format ( ( ph /\ b e. ( -us " R ) /\ a e. { ( -us ` A ) } ) -> b b
99	59 61 67 69 98	ssltd	Could not format ( ph -> ( -us " R ) < ( -us " R ) <
100	6	sneqd	Could not format ( ph -> { ( -us ` A ) } = { ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) } ) : No typesetting found for |- ( ph -> { ( -us ` A ) } = { ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) } ) with typecode |-
101	99 100	breqtrd	Could not format ( ph -> ( -us " R ) < ( -us " R ) <
102		ssltex1	$$⊢L{\ll }_{s}R\to L\in \mathrm{V}$$
103	1 102	syl	$$⊢\phi \to L\in \mathrm{V}$$
104		funimaexg	Could not format ( ( Fun -us /\ L e. _V ) -> ( -us " L ) e. _V ) : No typesetting found for |- ( ( Fun -us /\ L e. _V ) -> ( -us " L ) e. _V ) with typecode |-
105	55 103 104	sylancr	Could not format ( ph -> ( -us " L ) e. _V ) : No typesetting found for |- ( ph -> ( -us " L ) e. _V ) with typecode |-
106		imassrn	Could not format ( -us " L ) C_ ran -us : No typesetting found for |- ( -us " L ) C_ ran -us with typecode |-
107	106 65	sseqtri	Could not format ( -us " L ) C_ No : No typesetting found for |- ( -us " L ) C_ No with typecode |-
108	107	a1i	Could not format ( ph -> ( -us " L ) C_ No ) : No typesetting found for |- ( ph -> ( -us " L ) C_ No ) with typecode |-
109		fvelimab	Could not format ( ( -us Fn No /\ L C_ No ) -> ( b e. ( -us " L ) <-> E. c e. L ( -us ` c ) = b ) ) : No typesetting found for |- ( ( -us Fn No /\ L C_ No ) -> ( b e. ( -us " L ) <-> E. c e. L ( -us ` c ) = b ) ) with typecode |-
110	10 34 109	sylancr	Could not format ( ph -> ( b e. ( -us " L ) <-> E. c e. L ( -us ` c ) = b ) ) : No typesetting found for |- ( ph -> ( b e. ( -us " L ) <-> E. c e. L ( -us ` c ) = b ) ) with typecode |-
111	1	adantr	$$⊢\left(\phi \wedge c\in L\right)\to L{\ll }_{s}R$$
112	111 75	syl	$$⊢\left(\phi \wedge c\in L\right)\to \left(L{|}_{s}R\in \mathrm{No}\wedge L{\ll }_s\left\{L{|}_{s}R\right\}\wedge \left\{L{|}_{s}R\right\}{\ll }_{s}R\right)$$
113	112	simp2d	$$⊢\left(\phi \wedge c\in L\right)\to L{\ll }_s\left\{L{|}_{s}R\right\}$$
114	73	adantr	$$⊢\left(\phi \wedge c\in L\right)\to \left\{A\right\}=\left\{L{|}_{s}R\right\}$$
115	113 114	breqtrrd	$$⊢\left(\phi \wedge c\in L\right)\to L{\ll }_s\left\{A\right\}$$
116		simpr	$$⊢\left(\phi \wedge c\in L\right)\to c\in L$$
117	81	adantr	$$⊢\left(\phi \wedge c\in L\right)\to A\in \left\{A\right\}$$
118	115 116 117	ssltsepcd	$$⊢\left(\phi \wedge c\in L\right)\to c{<}_{s}A$$
119	34	sselda	$$⊢\left(\phi \wedge c\in L\right)\to c\in \mathrm{No}$$
120	4	adantr	$$⊢\left(\phi \wedge c\in L\right)\to A\in \mathrm{No}$$
121	119 120	sltnegd	Could not format ( ( ph /\ c e. L ) -> ( c ( -us ` A ) ( c ( -us ` A )
122	118 121	mpbid	Could not format ( ( ph /\ c e. L ) -> ( -us ` A ) ( -us ` A )
123		breq2	Could not format ( ( -us ` c ) = b -> ( ( -us ` A ) ( -us ` A ) ( ( -us ` A ) ( -us ` A )
124	122 123	syl5ibcom	Could not format ( ( ph /\ c e. L ) -> ( ( -us ` c ) = b -> ( -us ` A ) ( ( -us ` c ) = b -> ( -us ` A )
125	124	rexlimdva	Could not format ( ph -> ( E. c e. L ( -us ` c ) = b -> ( -us ` A ) ( E. c e. L ( -us ` c ) = b -> ( -us ` A )
126	110 125	sylbid	Could not format ( ph -> ( b e. ( -us " L ) -> ( -us ` A ) ( b e. ( -us " L ) -> ( -us ` A )
127		breq1	Could not format ( a = ( -us ` A ) -> ( a ( -us ` A ) ( a ( -us ` A )
128	127	imbi2d	Could not format ( a = ( -us ` A ) -> ( ( b e. ( -us " L ) -> a ( b e. ( -us " L ) -> ( -us ` A ) ( ( b e. ( -us " L ) -> a ( b e. ( -us " L ) -> ( -us ` A )
129	126 128	syl5ibrcom	Could not format ( ph -> ( a = ( -us ` A ) -> ( b e. ( -us " L ) -> a ( a = ( -us ` A ) -> ( b e. ( -us " L ) -> a
130	70 129	biimtrid	Could not format ( ph -> ( a e. { ( -us ` A ) } -> ( b e. ( -us " L ) -> a ( a e. { ( -us ` A ) } -> ( b e. ( -us " L ) -> a
131	130	3imp	Could not format ( ( ph /\ a e. { ( -us ` A ) } /\ b e. ( -us " L ) ) -> a a
132	61 105 69 108 131	ssltd	Could not format ( ph -> { ( -us ` A ) } < { ( -us ` A ) } <
133	100 132	eqbrtrrd	Could not format ( ph -> { ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) } < { ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) } <
134	8 31 53 101 133	cofcut1d	Could not format ( ph -> ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) = ( ( -us " R ) |s ( -us " L ) ) ) : No typesetting found for |- ( ph -> ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) = ( ( -us " R ) |s ( -us " L ) ) ) with typecode |-
135	6 134	eqtrd	Could not format ( ph -> ( -us ` A ) = ( ( -us " R ) |s ( -us " L ) ) ) : No typesetting found for |- ( ph -> ( -us ` A ) = ( ( -us " R ) |s ( -us " L ) ) ) with typecode |-