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	⊢ ( 𝜑 → 𝐿 <<s 𝑅 )
	negsunif.2	⊢ ( 𝜑 → 𝐴 = ( 𝐿 |s 𝑅 ) )
Assertion	negsunif	⊢ ( 𝜑 → ( -us ‘ 𝐴 ) = ( ( -us “ 𝑅 ) |s ( -us “ 𝐿 ) ) )

Proof

Step	Hyp	Ref	Expression
1		negsunif.1	⊢ ( 𝜑 → 𝐿 <<s 𝑅 )
2		negsunif.2	⊢ ( 𝜑 → 𝐴 = ( 𝐿 |s 𝑅 ) )
3	1	scutcld	⊢ ( 𝜑 → ( 𝐿 |s 𝑅 ) ∈ No )
4	2 3	eqeltrd	⊢ ( 𝜑 → 𝐴 ∈ No )
5		negsval	⊢ ( 𝐴 ∈ No → ( -us ‘ 𝐴 ) = ( ( -us “ ( R ‘ 𝐴 ) ) |s ( -us “ ( L ‘ 𝐴 ) ) ) )
6	4 5	syl	⊢ ( 𝜑 → ( -us ‘ 𝐴 ) = ( ( -us “ ( R ‘ 𝐴 ) ) |s ( -us “ ( L ‘ 𝐴 ) ) ) )
7		negscut2	⊢ ( 𝐴 ∈ No → ( -us “ ( R ‘ 𝐴 ) ) <<s ( -us “ ( L ‘ 𝐴 ) ) )
8	4 7	syl	⊢ ( 𝜑 → ( -us “ ( R ‘ 𝐴 ) ) <<s ( -us “ ( L ‘ 𝐴 ) ) )
9	1 2	cofcutr2d	⊢ ( 𝜑 → ∀ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ 𝑅 𝑑 ≤s 𝑐 )
10		negsfn	⊢ -us Fn No
11		ssltss2	⊢ ( 𝐿 <<s 𝑅 → 𝑅 ⊆ No )
12	1 11	syl	⊢ ( 𝜑 → 𝑅 ⊆ No )
13		breq2	⊢ ( 𝑏 = ( -us ‘ 𝑑 ) → ( ( -us ‘ 𝑐 ) ≤s 𝑏 ↔ ( -us ‘ 𝑐 ) ≤s ( -us ‘ 𝑑 ) ) )
14	13	imaeqsexv	⊢ ( ( -us Fn No ∧ 𝑅 ⊆ No ) → ( ∃ 𝑏 ∈ ( -us “ 𝑅 ) ( -us ‘ 𝑐 ) ≤s 𝑏 ↔ ∃ 𝑑 ∈ 𝑅 ( -us ‘ 𝑐 ) ≤s ( -us ‘ 𝑑 ) ) )
15	10 12 14	sylancr	⊢ ( 𝜑 → ( ∃ 𝑏 ∈ ( -us “ 𝑅 ) ( -us ‘ 𝑐 ) ≤s 𝑏 ↔ ∃ 𝑑 ∈ 𝑅 ( -us ‘ 𝑐 ) ≤s ( -us ‘ 𝑑 ) ) )
16	15	ralbidv	⊢ ( 𝜑 → ( ∀ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑏 ∈ ( -us “ 𝑅 ) ( -us ‘ 𝑐 ) ≤s 𝑏 ↔ ∀ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ 𝑅 ( -us ‘ 𝑐 ) ≤s ( -us ‘ 𝑑 ) ) )
17	12	adantr	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) → 𝑅 ⊆ No )
18	17	sselda	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) ∧ 𝑑 ∈ 𝑅 ) → 𝑑 ∈ No )
19		rightssno	⊢ ( R ‘ 𝐴 ) ⊆ No
20	19	sseli	⊢ ( 𝑐 ∈ ( R ‘ 𝐴 ) → 𝑐 ∈ No )
21	20	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) ∧ 𝑑 ∈ 𝑅 ) → 𝑐 ∈ No )
22	18 21	slenegd	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) ∧ 𝑑 ∈ 𝑅 ) → ( 𝑑 ≤s 𝑐 ↔ ( -us ‘ 𝑐 ) ≤s ( -us ‘ 𝑑 ) ) )
23	22	rexbidva	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) → ( ∃ 𝑑 ∈ 𝑅 𝑑 ≤s 𝑐 ↔ ∃ 𝑑 ∈ 𝑅 ( -us ‘ 𝑐 ) ≤s ( -us ‘ 𝑑 ) ) )
24	23	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ 𝑅 𝑑 ≤s 𝑐 ↔ ∀ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ 𝑅 ( -us ‘ 𝑐 ) ≤s ( -us ‘ 𝑑 ) ) )
25	16 24	bitr4d	⊢ ( 𝜑 → ( ∀ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑏 ∈ ( -us “ 𝑅 ) ( -us ‘ 𝑐 ) ≤s 𝑏 ↔ ∀ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ 𝑅 𝑑 ≤s 𝑐 ) )
26	9 25	mpbird	⊢ ( 𝜑 → ∀ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑏 ∈ ( -us “ 𝑅 ) ( -us ‘ 𝑐 ) ≤s 𝑏 )
27		breq1	⊢ ( 𝑎 = ( -us ‘ 𝑐 ) → ( 𝑎 ≤s 𝑏 ↔ ( -us ‘ 𝑐 ) ≤s 𝑏 ) )
28	27	rexbidv	⊢ ( 𝑎 = ( -us ‘ 𝑐 ) → ( ∃ 𝑏 ∈ ( -us “ 𝑅 ) 𝑎 ≤s 𝑏 ↔ ∃ 𝑏 ∈ ( -us “ 𝑅 ) ( -us ‘ 𝑐 ) ≤s 𝑏 ) )
29	28	imaeqsalv	⊢ ( ( -us Fn No ∧ ( R ‘ 𝐴 ) ⊆ No ) → ( ∀ 𝑎 ∈ ( -us “ ( R ‘ 𝐴 ) ) ∃ 𝑏 ∈ ( -us “ 𝑅 ) 𝑎 ≤s 𝑏 ↔ ∀ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑏 ∈ ( -us “ 𝑅 ) ( -us ‘ 𝑐 ) ≤s 𝑏 ) )
30	10 19 29	mp2an	⊢ ( ∀ 𝑎 ∈ ( -us “ ( R ‘ 𝐴 ) ) ∃ 𝑏 ∈ ( -us “ 𝑅 ) 𝑎 ≤s 𝑏 ↔ ∀ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑏 ∈ ( -us “ 𝑅 ) ( -us ‘ 𝑐 ) ≤s 𝑏 )
31	26 30	sylibr	⊢ ( 𝜑 → ∀ 𝑎 ∈ ( -us “ ( R ‘ 𝐴 ) ) ∃ 𝑏 ∈ ( -us “ 𝑅 ) 𝑎 ≤s 𝑏 )
32	1 2	cofcutr1d	⊢ ( 𝜑 → ∀ 𝑐 ∈ ( L ‘ 𝐴 ) ∃ 𝑑 ∈ 𝐿 𝑐 ≤s 𝑑 )
33		ssltss1	⊢ ( 𝐿 <<s 𝑅 → 𝐿 ⊆ No )
34	1 33	syl	⊢ ( 𝜑 → 𝐿 ⊆ No )
35		breq1	⊢ ( 𝑏 = ( -us ‘ 𝑑 ) → ( 𝑏 ≤s ( -us ‘ 𝑐 ) ↔ ( -us ‘ 𝑑 ) ≤s ( -us ‘ 𝑐 ) ) )
36	35	imaeqsexv	⊢ ( ( -us Fn No ∧ 𝐿 ⊆ No ) → ( ∃ 𝑏 ∈ ( -us “ 𝐿 ) 𝑏 ≤s ( -us ‘ 𝑐 ) ↔ ∃ 𝑑 ∈ 𝐿 ( -us ‘ 𝑑 ) ≤s ( -us ‘ 𝑐 ) ) )
37	10 34 36	sylancr	⊢ ( 𝜑 → ( ∃ 𝑏 ∈ ( -us “ 𝐿 ) 𝑏 ≤s ( -us ‘ 𝑐 ) ↔ ∃ 𝑑 ∈ 𝐿 ( -us ‘ 𝑑 ) ≤s ( -us ‘ 𝑐 ) ) )
38	37	ralbidv	⊢ ( 𝜑 → ( ∀ 𝑐 ∈ ( L ‘ 𝐴 ) ∃ 𝑏 ∈ ( -us “ 𝐿 ) 𝑏 ≤s ( -us ‘ 𝑐 ) ↔ ∀ 𝑐 ∈ ( L ‘ 𝐴 ) ∃ 𝑑 ∈ 𝐿 ( -us ‘ 𝑑 ) ≤s ( -us ‘ 𝑐 ) ) )
39		leftssno	⊢ ( L ‘ 𝐴 ) ⊆ No
40	39	sseli	⊢ ( 𝑐 ∈ ( L ‘ 𝐴 ) → 𝑐 ∈ No )
41	40	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( L ‘ 𝐴 ) ) ∧ 𝑑 ∈ 𝐿 ) → 𝑐 ∈ No )
42	34	adantr	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( L ‘ 𝐴 ) ) → 𝐿 ⊆ No )
43	42	sselda	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( L ‘ 𝐴 ) ) ∧ 𝑑 ∈ 𝐿 ) → 𝑑 ∈ No )
44	41 43	slenegd	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( L ‘ 𝐴 ) ) ∧ 𝑑 ∈ 𝐿 ) → ( 𝑐 ≤s 𝑑 ↔ ( -us ‘ 𝑑 ) ≤s ( -us ‘ 𝑐 ) ) )
45	44	rexbidva	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( L ‘ 𝐴 ) ) → ( ∃ 𝑑 ∈ 𝐿 𝑐 ≤s 𝑑 ↔ ∃ 𝑑 ∈ 𝐿 ( -us ‘ 𝑑 ) ≤s ( -us ‘ 𝑐 ) ) )
46	45	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑐 ∈ ( L ‘ 𝐴 ) ∃ 𝑑 ∈ 𝐿 𝑐 ≤s 𝑑 ↔ ∀ 𝑐 ∈ ( L ‘ 𝐴 ) ∃ 𝑑 ∈ 𝐿 ( -us ‘ 𝑑 ) ≤s ( -us ‘ 𝑐 ) ) )
47	38 46	bitr4d	⊢ ( 𝜑 → ( ∀ 𝑐 ∈ ( L ‘ 𝐴 ) ∃ 𝑏 ∈ ( -us “ 𝐿 ) 𝑏 ≤s ( -us ‘ 𝑐 ) ↔ ∀ 𝑐 ∈ ( L ‘ 𝐴 ) ∃ 𝑑 ∈ 𝐿 𝑐 ≤s 𝑑 ) )
48	32 47	mpbird	⊢ ( 𝜑 → ∀ 𝑐 ∈ ( L ‘ 𝐴 ) ∃ 𝑏 ∈ ( -us “ 𝐿 ) 𝑏 ≤s ( -us ‘ 𝑐 ) )
49		breq2	⊢ ( 𝑎 = ( -us ‘ 𝑐 ) → ( 𝑏 ≤s 𝑎 ↔ 𝑏 ≤s ( -us ‘ 𝑐 ) ) )
50	49	rexbidv	⊢ ( 𝑎 = ( -us ‘ 𝑐 ) → ( ∃ 𝑏 ∈ ( -us “ 𝐿 ) 𝑏 ≤s 𝑎 ↔ ∃ 𝑏 ∈ ( -us “ 𝐿 ) 𝑏 ≤s ( -us ‘ 𝑐 ) ) )
51	50	imaeqsalv	⊢ ( ( -us Fn No ∧ ( L ‘ 𝐴 ) ⊆ No ) → ( ∀ 𝑎 ∈ ( -us “ ( L ‘ 𝐴 ) ) ∃ 𝑏 ∈ ( -us “ 𝐿 ) 𝑏 ≤s 𝑎 ↔ ∀ 𝑐 ∈ ( L ‘ 𝐴 ) ∃ 𝑏 ∈ ( -us “ 𝐿 ) 𝑏 ≤s ( -us ‘ 𝑐 ) ) )
52	10 39 51	mp2an	⊢ ( ∀ 𝑎 ∈ ( -us “ ( L ‘ 𝐴 ) ) ∃ 𝑏 ∈ ( -us “ 𝐿 ) 𝑏 ≤s 𝑎 ↔ ∀ 𝑐 ∈ ( L ‘ 𝐴 ) ∃ 𝑏 ∈ ( -us “ 𝐿 ) 𝑏 ≤s ( -us ‘ 𝑐 ) )
53	48 52	sylibr	⊢ ( 𝜑 → ∀ 𝑎 ∈ ( -us “ ( L ‘ 𝐴 ) ) ∃ 𝑏 ∈ ( -us “ 𝐿 ) 𝑏 ≤s 𝑎 )
54		fnfun	⊢ ( -us Fn No → Fun -us )
55	10 54	ax-mp	⊢ Fun -us
56		ssltex2	⊢ ( 𝐿 <<s 𝑅 → 𝑅 ∈ V )
57	1 56	syl	⊢ ( 𝜑 → 𝑅 ∈ V )
58		funimaexg	⊢ ( ( Fun -us ∧ 𝑅 ∈ V ) → ( -us “ 𝑅 ) ∈ V )
59	55 57 58	sylancr	⊢ ( 𝜑 → ( -us “ 𝑅 ) ∈ V )
60		snex	⊢ { ( -us ‘ 𝐴 ) } ∈ V
61	60	a1i	⊢ ( 𝜑 → { ( -us ‘ 𝐴 ) } ∈ V )
62		imassrn	⊢ ( -us “ 𝑅 ) ⊆ ran -us
63		negsfo	⊢ -us : No –onto→ No
64		forn	⊢ ( -us : No –onto→ No → ran -us = No )
65	63 64	ax-mp	⊢ ran -us = No
66	62 65	sseqtri	⊢ ( -us “ 𝑅 ) ⊆ No
67	66	a1i	⊢ ( 𝜑 → ( -us “ 𝑅 ) ⊆ No )
68	4	negscld	⊢ ( 𝜑 → ( -us ‘ 𝐴 ) ∈ No )
69	68	snssd	⊢ ( 𝜑 → { ( -us ‘ 𝐴 ) } ⊆ No )
70		velsn	⊢ ( 𝑎 ∈ { ( -us ‘ 𝐴 ) } ↔ 𝑎 = ( -us ‘ 𝐴 ) )
71		fvelimab	⊢ ( ( -us Fn No ∧ 𝑅 ⊆ No ) → ( 𝑏 ∈ ( -us “ 𝑅 ) ↔ ∃ 𝑑 ∈ 𝑅 ( -us ‘ 𝑑 ) = 𝑏 ) )
72	10 12 71	sylancr	⊢ ( 𝜑 → ( 𝑏 ∈ ( -us “ 𝑅 ) ↔ ∃ 𝑑 ∈ 𝑅 ( -us ‘ 𝑑 ) = 𝑏 ) )
73	2	sneqd	⊢ ( 𝜑 → { 𝐴 } = { ( 𝐿 |s 𝑅 ) } )
74	73	adantr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝑅 ) → { 𝐴 } = { ( 𝐿 |s 𝑅 ) } )
75		scutcut	⊢ ( 𝐿 <<s 𝑅 → ( ( 𝐿 |s 𝑅 ) ∈ No ∧ 𝐿 <<s { ( 𝐿 |s 𝑅 ) } ∧ { ( 𝐿 |s 𝑅 ) } <<s 𝑅 ) )
76	1 75	syl	⊢ ( 𝜑 → ( ( 𝐿 |s 𝑅 ) ∈ No ∧ 𝐿 <<s { ( 𝐿 |s 𝑅 ) } ∧ { ( 𝐿 |s 𝑅 ) } <<s 𝑅 ) )
77	76	simp3d	⊢ ( 𝜑 → { ( 𝐿 |s 𝑅 ) } <<s 𝑅 )
78	77	adantr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝑅 ) → { ( 𝐿 |s 𝑅 ) } <<s 𝑅 )
79	74 78	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝑅 ) → { 𝐴 } <<s 𝑅 )
80		snidg	⊢ ( 𝐴 ∈ No → 𝐴 ∈ { 𝐴 } )
81	4 80	syl	⊢ ( 𝜑 → 𝐴 ∈ { 𝐴 } )
82	81	adantr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝑅 ) → 𝐴 ∈ { 𝐴 } )
83		simpr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝑅 ) → 𝑑 ∈ 𝑅 )
84	79 82 83	ssltsepcd	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝑅 ) → 𝐴 <s 𝑑 )
85	4	adantr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝑅 ) → 𝐴 ∈ No )
86	12	sselda	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝑅 ) → 𝑑 ∈ No )
87	85 86	sltnegd	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝑅 ) → ( 𝐴 <s 𝑑 ↔ ( -us ‘ 𝑑 ) <s ( -us ‘ 𝐴 ) ) )
88	84 87	mpbid	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝑅 ) → ( -us ‘ 𝑑 ) <s ( -us ‘ 𝐴 ) )
89		breq1	⊢ ( ( -us ‘ 𝑑 ) = 𝑏 → ( ( -us ‘ 𝑑 ) <s ( -us ‘ 𝐴 ) ↔ 𝑏 <s ( -us ‘ 𝐴 ) ) )
90	88 89	syl5ibcom	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝑅 ) → ( ( -us ‘ 𝑑 ) = 𝑏 → 𝑏 <s ( -us ‘ 𝐴 ) ) )
91	90	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑑 ∈ 𝑅 ( -us ‘ 𝑑 ) = 𝑏 → 𝑏 <s ( -us ‘ 𝐴 ) ) )
92	72 91	sylbid	⊢ ( 𝜑 → ( 𝑏 ∈ ( -us “ 𝑅 ) → 𝑏 <s ( -us ‘ 𝐴 ) ) )
93		breq2	⊢ ( 𝑎 = ( -us ‘ 𝐴 ) → ( 𝑏 <s 𝑎 ↔ 𝑏 <s ( -us ‘ 𝐴 ) ) )
94	93	imbi2d	⊢ ( 𝑎 = ( -us ‘ 𝐴 ) → ( ( 𝑏 ∈ ( -us “ 𝑅 ) → 𝑏 <s 𝑎 ) ↔ ( 𝑏 ∈ ( -us “ 𝑅 ) → 𝑏 <s ( -us ‘ 𝐴 ) ) ) )
95	92 94	syl5ibrcom	⊢ ( 𝜑 → ( 𝑎 = ( -us ‘ 𝐴 ) → ( 𝑏 ∈ ( -us “ 𝑅 ) → 𝑏 <s 𝑎 ) ) )
96	70 95	biimtrid	⊢ ( 𝜑 → ( 𝑎 ∈ { ( -us ‘ 𝐴 ) } → ( 𝑏 ∈ ( -us “ 𝑅 ) → 𝑏 <s 𝑎 ) ) )
97	96	3imp	⊢ ( ( 𝜑 ∧ 𝑎 ∈ { ( -us ‘ 𝐴 ) } ∧ 𝑏 ∈ ( -us “ 𝑅 ) ) → 𝑏 <s 𝑎 )
98	97	3com23	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( -us “ 𝑅 ) ∧ 𝑎 ∈ { ( -us ‘ 𝐴 ) } ) → 𝑏 <s 𝑎 )
99	59 61 67 69 98	ssltd	⊢ ( 𝜑 → ( -us “ 𝑅 ) <<s { ( -us ‘ 𝐴 ) } )
100	6	sneqd	⊢ ( 𝜑 → { ( -us ‘ 𝐴 ) } = { ( ( -us “ ( R ‘ 𝐴 ) ) |s ( -us “ ( L ‘ 𝐴 ) ) ) } )
101	99 100	breqtrd	⊢ ( 𝜑 → ( -us “ 𝑅 ) <<s { ( ( -us “ ( R ‘ 𝐴 ) ) |s ( -us “ ( L ‘ 𝐴 ) ) ) } )
102		ssltex1	⊢ ( 𝐿 <<s 𝑅 → 𝐿 ∈ V )
103	1 102	syl	⊢ ( 𝜑 → 𝐿 ∈ V )
104		funimaexg	⊢ ( ( Fun -us ∧ 𝐿 ∈ V ) → ( -us “ 𝐿 ) ∈ V )
105	55 103 104	sylancr	⊢ ( 𝜑 → ( -us “ 𝐿 ) ∈ V )
106		imassrn	⊢ ( -us “ 𝐿 ) ⊆ ran -us
107	106 65	sseqtri	⊢ ( -us “ 𝐿 ) ⊆ No
108	107	a1i	⊢ ( 𝜑 → ( -us “ 𝐿 ) ⊆ No )
109		fvelimab	⊢ ( ( -us Fn No ∧ 𝐿 ⊆ No ) → ( 𝑏 ∈ ( -us “ 𝐿 ) ↔ ∃ 𝑐 ∈ 𝐿 ( -us ‘ 𝑐 ) = 𝑏 ) )
110	10 34 109	sylancr	⊢ ( 𝜑 → ( 𝑏 ∈ ( -us “ 𝐿 ) ↔ ∃ 𝑐 ∈ 𝐿 ( -us ‘ 𝑐 ) = 𝑏 ) )
111	1	adantr	⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐿 ) → 𝐿 <<s 𝑅 )
112	111 75	syl	⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐿 ) → ( ( 𝐿 |s 𝑅 ) ∈ No ∧ 𝐿 <<s { ( 𝐿 |s 𝑅 ) } ∧ { ( 𝐿 |s 𝑅 ) } <<s 𝑅 ) )
113	112	simp2d	⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐿 ) → 𝐿 <<s { ( 𝐿 |s 𝑅 ) } )
114	73	adantr	⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐿 ) → { 𝐴 } = { ( 𝐿 |s 𝑅 ) } )
115	113 114	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐿 ) → 𝐿 <<s { 𝐴 } )
116		simpr	⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐿 ) → 𝑐 ∈ 𝐿 )
117	81	adantr	⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐿 ) → 𝐴 ∈ { 𝐴 } )
118	115 116 117	ssltsepcd	⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐿 ) → 𝑐 <s 𝐴 )
119	34	sselda	⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐿 ) → 𝑐 ∈ No )
120	4	adantr	⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐿 ) → 𝐴 ∈ No )
121	119 120	sltnegd	⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐿 ) → ( 𝑐 <s 𝐴 ↔ ( -us ‘ 𝐴 ) <s ( -us ‘ 𝑐 ) ) )
122	118 121	mpbid	⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐿 ) → ( -us ‘ 𝐴 ) <s ( -us ‘ 𝑐 ) )
123		breq2	⊢ ( ( -us ‘ 𝑐 ) = 𝑏 → ( ( -us ‘ 𝐴 ) <s ( -us ‘ 𝑐 ) ↔ ( -us ‘ 𝐴 ) <s 𝑏 ) )
124	122 123	syl5ibcom	⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐿 ) → ( ( -us ‘ 𝑐 ) = 𝑏 → ( -us ‘ 𝐴 ) <s 𝑏 ) )
125	124	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑐 ∈ 𝐿 ( -us ‘ 𝑐 ) = 𝑏 → ( -us ‘ 𝐴 ) <s 𝑏 ) )
126	110 125	sylbid	⊢ ( 𝜑 → ( 𝑏 ∈ ( -us “ 𝐿 ) → ( -us ‘ 𝐴 ) <s 𝑏 ) )
127		breq1	⊢ ( 𝑎 = ( -us ‘ 𝐴 ) → ( 𝑎 <s 𝑏 ↔ ( -us ‘ 𝐴 ) <s 𝑏 ) )
128	127	imbi2d	⊢ ( 𝑎 = ( -us ‘ 𝐴 ) → ( ( 𝑏 ∈ ( -us “ 𝐿 ) → 𝑎 <s 𝑏 ) ↔ ( 𝑏 ∈ ( -us “ 𝐿 ) → ( -us ‘ 𝐴 ) <s 𝑏 ) ) )
129	126 128	syl5ibrcom	⊢ ( 𝜑 → ( 𝑎 = ( -us ‘ 𝐴 ) → ( 𝑏 ∈ ( -us “ 𝐿 ) → 𝑎 <s 𝑏 ) ) )
130	70 129	biimtrid	⊢ ( 𝜑 → ( 𝑎 ∈ { ( -us ‘ 𝐴 ) } → ( 𝑏 ∈ ( -us “ 𝐿 ) → 𝑎 <s 𝑏 ) ) )
131	130	3imp	⊢ ( ( 𝜑 ∧ 𝑎 ∈ { ( -us ‘ 𝐴 ) } ∧ 𝑏 ∈ ( -us “ 𝐿 ) ) → 𝑎 <s 𝑏 )
132	61 105 69 108 131	ssltd	⊢ ( 𝜑 → { ( -us ‘ 𝐴 ) } <<s ( -us “ 𝐿 ) )
133	100 132	eqbrtrrd	⊢ ( 𝜑 → { ( ( -us “ ( R ‘ 𝐴 ) ) |s ( -us “ ( L ‘ 𝐴 ) ) ) } <<s ( -us “ 𝐿 ) )
134	8 31 53 101 133	cofcut1d	⊢ ( 𝜑 → ( ( -us “ ( R ‘ 𝐴 ) ) |s ( -us “ ( L ‘ 𝐴 ) ) ) = ( ( -us “ 𝑅 ) |s ( -us “ 𝐿 ) ) )
135	6 134	eqtrd	⊢ ( 𝜑 → ( -us ‘ 𝐴 ) = ( ( -us “ 𝑅 ) |s ( -us “ 𝐿 ) ) )