Theorem negsid

Description: Surreal addition of a number and its negative. Theorem 4(iii) of Conway p. 17. (Contributed by Scott Fenton, 3-Feb-2025)

	Ref	Expression
Assertion	negsid	⊢ ( 𝐴 ∈ No → ( 𝐴 +s ( -us ‘ 𝐴 ) ) = 0s )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝑥 = 𝑥𝑂 → 𝑥 = 𝑥𝑂 )
2		fveq2	⊢ ( 𝑥 = 𝑥𝑂 → ( -us ‘ 𝑥 ) = ( -us ‘ 𝑥𝑂 ) )
3	1 2	oveq12d	⊢ ( 𝑥 = 𝑥𝑂 → ( 𝑥 +s ( -us ‘ 𝑥 ) ) = ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) )
4	3	eqeq1d	⊢ ( 𝑥 = 𝑥𝑂 → ( ( 𝑥 +s ( -us ‘ 𝑥 ) ) = 0s ↔ ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) )
5		id	⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
6		fveq2	⊢ ( 𝑥 = 𝐴 → ( -us ‘ 𝑥 ) = ( -us ‘ 𝐴 ) )
7	5 6	oveq12d	⊢ ( 𝑥 = 𝐴 → ( 𝑥 +s ( -us ‘ 𝑥 ) ) = ( 𝐴 +s ( -us ‘ 𝐴 ) ) )
8	7	eqeq1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 +s ( -us ‘ 𝑥 ) ) = 0s ↔ ( 𝐴 +s ( -us ‘ 𝐴 ) ) = 0s ) )
9		lltr	⊢ ( L ‘ 𝑥 ) <<s ( R ‘ 𝑥 )
10	9	a1i	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( L ‘ 𝑥 ) <<s ( R ‘ 𝑥 ) )
11		negcut2	⊢ ( 𝑥 ∈ No → ( -us “ ( R ‘ 𝑥 ) ) <<s ( -us “ ( L ‘ 𝑥 ) ) )
12	11	adantr	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( -us “ ( R ‘ 𝑥 ) ) <<s ( -us “ ( L ‘ 𝑥 ) ) )
13		lrcut	⊢ ( 𝑥 ∈ No → ( ( L ‘ 𝑥 ) |s ( R ‘ 𝑥 ) ) = 𝑥 )
14	13	adantr	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( ( L ‘ 𝑥 ) |s ( R ‘ 𝑥 ) ) = 𝑥 )
15	14	eqcomd	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → 𝑥 = ( ( L ‘ 𝑥 ) |s ( R ‘ 𝑥 ) ) )
16		negsval	⊢ ( 𝑥 ∈ No → ( -us ‘ 𝑥 ) = ( ( -us “ ( R ‘ 𝑥 ) ) |s ( -us “ ( L ‘ 𝑥 ) ) ) )
17	16	adantr	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( -us ‘ 𝑥 ) = ( ( -us “ ( R ‘ 𝑥 ) ) |s ( -us “ ( L ‘ 𝑥 ) ) ) )
18	10 12 15 17	addsunif	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( 𝑥 +s ( -us ‘ 𝑥 ) ) = ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑏 ∣ ∃ 𝑝 ∈ ( -us “ ( R ‘ 𝑥 ) ) 𝑏 = ( 𝑥 +s 𝑝 ) } ) |s ( { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑑 ∣ ∃ 𝑞 ∈ ( -us “ ( L ‘ 𝑥 ) ) 𝑑 = ( 𝑥 +s 𝑞 ) } ) ) )
19		negsfn	⊢ -us Fn No
20		rightssno	⊢ ( R ‘ 𝑥 ) ⊆ No
21		oveq2	⊢ ( 𝑝 = ( -us ‘ 𝑥𝑅 ) → ( 𝑥 +s 𝑝 ) = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) )
22	21	eqeq2d	⊢ ( 𝑝 = ( -us ‘ 𝑥𝑅 ) → ( 𝑏 = ( 𝑥 +s 𝑝 ) ↔ 𝑏 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) ) )
23	22	rexima	⊢ ( ( -us Fn No ∧ ( R ‘ 𝑥 ) ⊆ No ) → ( ∃ 𝑝 ∈ ( -us “ ( R ‘ 𝑥 ) ) 𝑏 = ( 𝑥 +s 𝑝 ) ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑏 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) ) )
24	19 20 23	mp2an	⊢ ( ∃ 𝑝 ∈ ( -us “ ( R ‘ 𝑥 ) ) 𝑏 = ( 𝑥 +s 𝑝 ) ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑏 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) )
25	24	abbii	⊢ { 𝑏 ∣ ∃ 𝑝 ∈ ( -us “ ( R ‘ 𝑥 ) ) 𝑏 = ( 𝑥 +s 𝑝 ) } = { 𝑏 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑏 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) }
26	25	uneq2i	⊢ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑏 ∣ ∃ 𝑝 ∈ ( -us “ ( R ‘ 𝑥 ) ) 𝑏 = ( 𝑥 +s 𝑝 ) } ) = ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑏 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑏 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) } )
27		leftssno	⊢ ( L ‘ 𝑥 ) ⊆ No
28		oveq2	⊢ ( 𝑞 = ( -us ‘ 𝑥𝐿 ) → ( 𝑥 +s 𝑞 ) = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) )
29	28	eqeq2d	⊢ ( 𝑞 = ( -us ‘ 𝑥𝐿 ) → ( 𝑑 = ( 𝑥 +s 𝑞 ) ↔ 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) ) )
30	29	rexima	⊢ ( ( -us Fn No ∧ ( L ‘ 𝑥 ) ⊆ No ) → ( ∃ 𝑞 ∈ ( -us “ ( L ‘ 𝑥 ) ) 𝑑 = ( 𝑥 +s 𝑞 ) ↔ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) ) )
31	19 27 30	mp2an	⊢ ( ∃ 𝑞 ∈ ( -us “ ( L ‘ 𝑥 ) ) 𝑑 = ( 𝑥 +s 𝑞 ) ↔ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) )
32	31	abbii	⊢ { 𝑑 ∣ ∃ 𝑞 ∈ ( -us “ ( L ‘ 𝑥 ) ) 𝑑 = ( 𝑥 +s 𝑞 ) } = { 𝑑 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) }
33	32	uneq2i	⊢ ( { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑑 ∣ ∃ 𝑞 ∈ ( -us “ ( L ‘ 𝑥 ) ) 𝑑 = ( 𝑥 +s 𝑞 ) } ) = ( { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑑 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) } )
34	26 33	oveq12i	⊢ ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑏 ∣ ∃ 𝑝 ∈ ( -us “ ( R ‘ 𝑥 ) ) 𝑏 = ( 𝑥 +s 𝑝 ) } ) |s ( { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑑 ∣ ∃ 𝑞 ∈ ( -us “ ( L ‘ 𝑥 ) ) 𝑑 = ( 𝑥 +s 𝑞 ) } ) ) = ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑏 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑏 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) } ) |s ( { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑑 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) } ) )
35		fvex	⊢ ( L ‘ 𝑥 ) ∈ V
36	35	abrexex	⊢ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) } ∈ V
37		fvex	⊢ ( R ‘ 𝑥 ) ∈ V
38	37	abrexex	⊢ { 𝑏 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑏 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) } ∈ V
39	36 38	unex	⊢ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑏 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑏 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) } ) ∈ V
40	39	a1i	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑏 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑏 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) } ) ∈ V )
41		snex	⊢ { 0s } ∈ V
42	41	a1i	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → { 0s } ∈ V )
43	27	sseli	⊢ ( 𝑥𝐿 ∈ ( L ‘ 𝑥 ) → 𝑥𝐿 ∈ No )
44	43	adantl	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → 𝑥𝐿 ∈ No )
45		simpll	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → 𝑥 ∈ No )
46	45	negscld	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ( -us ‘ 𝑥 ) ∈ No )
47	44 46	addscld	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) ∈ No )
48		eleq1	⊢ ( 𝑎 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) → ( 𝑎 ∈ No ↔ ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) ∈ No ) )
49	47 48	syl5ibrcom	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ( 𝑎 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) → 𝑎 ∈ No ) )
50	49	rexlimdva	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) → 𝑎 ∈ No ) )
51	50	abssdv	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) } ⊆ No )
52		simpll	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → 𝑥 ∈ No )
53	20	sseli	⊢ ( 𝑥𝑅 ∈ ( R ‘ 𝑥 ) → 𝑥𝑅 ∈ No )
54	53	adantl	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → 𝑥𝑅 ∈ No )
55	54	negscld	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ( -us ‘ 𝑥𝑅 ) ∈ No )
56	52 55	addscld	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) ∈ No )
57		eleq1	⊢ ( 𝑏 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) → ( 𝑏 ∈ No ↔ ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) ∈ No ) )
58	56 57	syl5ibrcom	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ( 𝑏 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) → 𝑏 ∈ No ) )
59	58	rexlimdva	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑏 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) → 𝑏 ∈ No ) )
60	59	abssdv	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → { 𝑏 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑏 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) } ⊆ No )
61	51 60	unssd	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑏 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑏 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) } ) ⊆ No )
62		0no	⊢ 0s ∈ No
63		snssi	⊢ ( 0s ∈ No → { 0s } ⊆ No )
64	62 63	mp1i	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → { 0s } ⊆ No )
65		elun	⊢ ( 𝑝 ∈ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑏 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑏 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) } ) ↔ ( 𝑝 ∈ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) } ∨ 𝑝 ∈ { 𝑏 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑏 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) } ) )
66		vex	⊢ 𝑝 ∈ V
67		eqeq1	⊢ ( 𝑎 = 𝑝 → ( 𝑎 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) ↔ 𝑝 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) ) )
68	67	rexbidv	⊢ ( 𝑎 = 𝑝 → ( ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) ↔ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑝 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) ) )
69	66 68	elab	⊢ ( 𝑝 ∈ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) } ↔ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑝 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) )
70		eqeq1	⊢ ( 𝑏 = 𝑝 → ( 𝑏 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) ↔ 𝑝 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) ) )
71	70	rexbidv	⊢ ( 𝑏 = 𝑝 → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑏 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑝 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) ) )
72	66 71	elab	⊢ ( 𝑝 ∈ { 𝑏 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑏 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) } ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑝 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) )
73	69 72	orbi12i	⊢ ( ( 𝑝 ∈ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) } ∨ 𝑝 ∈ { 𝑏 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑏 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) } ) ↔ ( ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑝 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) ∨ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑝 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) ) )
74	65 73	bitri	⊢ ( 𝑝 ∈ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑏 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑏 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) } ) ↔ ( ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑝 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) ∨ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑝 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) ) )
75		velsn	⊢ ( 𝑞 ∈ { 0s } ↔ 𝑞 = 0s )
76	74 75	anbi12i	⊢ ( ( 𝑝 ∈ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑏 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑏 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) } ) ∧ 𝑞 ∈ { 0s } ) ↔ ( ( ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑝 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) ∨ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑝 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) ) ∧ 𝑞 = 0s ) )
77		leftlt	⊢ ( 𝑥𝐿 ∈ ( L ‘ 𝑥 ) → 𝑥𝐿 <s 𝑥 )
78	77	adantl	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → 𝑥𝐿 <s 𝑥 )
79		ltnegsim	⊢ ( ( 𝑥𝐿 ∈ No ∧ 𝑥 ∈ No ) → ( 𝑥𝐿 <s 𝑥 → ( -us ‘ 𝑥 ) <s ( -us ‘ 𝑥𝐿 ) ) )
80	44 45 79	syl2anc	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ( 𝑥𝐿 <s 𝑥 → ( -us ‘ 𝑥 ) <s ( -us ‘ 𝑥𝐿 ) ) )
81	78 80	mpd	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ( -us ‘ 𝑥 ) <s ( -us ‘ 𝑥𝐿 ) )
82	44	negscld	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ( -us ‘ 𝑥𝐿 ) ∈ No )
83	46 82 44	ltadds2d	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ( ( -us ‘ 𝑥 ) <s ( -us ‘ 𝑥𝐿 ) ↔ ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) <s ( 𝑥𝐿 +s ( -us ‘ 𝑥𝐿 ) ) ) )
84	81 83	mpbid	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) <s ( 𝑥𝐿 +s ( -us ‘ 𝑥𝐿 ) ) )
85		id	⊢ ( 𝑥𝑂 = 𝑥𝐿 → 𝑥𝑂 = 𝑥𝐿 )
86		fveq2	⊢ ( 𝑥𝑂 = 𝑥𝐿 → ( -us ‘ 𝑥𝑂 ) = ( -us ‘ 𝑥𝐿 ) )
87	85 86	oveq12d	⊢ ( 𝑥𝑂 = 𝑥𝐿 → ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = ( 𝑥𝐿 +s ( -us ‘ 𝑥𝐿 ) ) )
88	87	eqeq1d	⊢ ( 𝑥𝑂 = 𝑥𝐿 → ( ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ↔ ( 𝑥𝐿 +s ( -us ‘ 𝑥𝐿 ) ) = 0s ) )
89		simplr	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s )
90		elun1	⊢ ( 𝑥𝐿 ∈ ( L ‘ 𝑥 ) → 𝑥𝐿 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
91	90	adantl	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → 𝑥𝐿 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
92	88 89 91	rspcdva	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ( 𝑥𝐿 +s ( -us ‘ 𝑥𝐿 ) ) = 0s )
93	84 92	breqtrd	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) <s 0s )
94		breq1	⊢ ( 𝑝 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) → ( 𝑝 <s 0s ↔ ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) <s 0s ) )
95	93 94	syl5ibrcom	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ( 𝑝 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) → 𝑝 <s 0s ) )
96	95	rexlimdva	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑝 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) → 𝑝 <s 0s ) )
97	96	imp	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑝 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) ) → 𝑝 <s 0s )
98		rightgt	⊢ ( 𝑥𝑅 ∈ ( R ‘ 𝑥 ) → 𝑥 <s 𝑥𝑅 )
99	98	adantl	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → 𝑥 <s 𝑥𝑅 )
100	52 54 55	ltadds1d	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ( 𝑥 <s 𝑥𝑅 ↔ ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) <s ( 𝑥𝑅 +s ( -us ‘ 𝑥𝑅 ) ) ) )
101	99 100	mpbid	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) <s ( 𝑥𝑅 +s ( -us ‘ 𝑥𝑅 ) ) )
102		id	⊢ ( 𝑥𝑂 = 𝑥𝑅 → 𝑥𝑂 = 𝑥𝑅 )
103		fveq2	⊢ ( 𝑥𝑂 = 𝑥𝑅 → ( -us ‘ 𝑥𝑂 ) = ( -us ‘ 𝑥𝑅 ) )
104	102 103	oveq12d	⊢ ( 𝑥𝑂 = 𝑥𝑅 → ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = ( 𝑥𝑅 +s ( -us ‘ 𝑥𝑅 ) ) )
105	104	eqeq1d	⊢ ( 𝑥𝑂 = 𝑥𝑅 → ( ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ↔ ( 𝑥𝑅 +s ( -us ‘ 𝑥𝑅 ) ) = 0s ) )
106		simplr	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s )
107		elun2	⊢ ( 𝑥𝑅 ∈ ( R ‘ 𝑥 ) → 𝑥𝑅 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
108	107	adantl	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → 𝑥𝑅 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
109	105 106 108	rspcdva	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ( 𝑥𝑅 +s ( -us ‘ 𝑥𝑅 ) ) = 0s )
110	101 109	breqtrd	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) <s 0s )
111		breq1	⊢ ( 𝑝 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) → ( 𝑝 <s 0s ↔ ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) <s 0s ) )
112	110 111	syl5ibrcom	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ( 𝑝 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) → 𝑝 <s 0s ) )
113	112	rexlimdva	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑝 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) → 𝑝 <s 0s ) )
114	113	imp	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑝 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) ) → 𝑝 <s 0s )
115	97 114	jaodan	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ ( ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑝 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) ∨ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑝 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) ) ) → 𝑝 <s 0s )
116		breq2	⊢ ( 𝑞 = 0s → ( 𝑝 <s 𝑞 ↔ 𝑝 <s 0s ) )
117	115 116	syl5ibrcom	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ ( ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑝 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) ∨ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑝 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) ) ) → ( 𝑞 = 0s → 𝑝 <s 𝑞 ) )
118	117	expimpd	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( ( ( ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑝 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) ∨ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑝 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) ) ∧ 𝑞 = 0s ) → 𝑝 <s 𝑞 ) )
119	76 118	biimtrid	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( ( 𝑝 ∈ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑏 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑏 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) } ) ∧ 𝑞 ∈ { 0s } ) → 𝑝 <s 𝑞 ) )
120	119	3impib	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑝 ∈ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑏 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑏 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) } ) ∧ 𝑞 ∈ { 0s } ) → 𝑝 <s 𝑞 )
121	40 42 61 64 120	sltsd	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑏 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑏 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) } ) <<s { 0s } )
122	37	abrexex	⊢ { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ∈ V
123	35	abrexex	⊢ { 𝑑 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) } ∈ V
124	122 123	unex	⊢ ( { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑑 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) } ) ∈ V
125	124	a1i	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑑 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) } ) ∈ V )
126	52	negscld	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ( -us ‘ 𝑥 ) ∈ No )
127	54 126	addscld	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) ∈ No )
128		eleq1	⊢ ( 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) → ( 𝑐 ∈ No ↔ ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) ∈ No ) )
129	127 128	syl5ibrcom	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ( 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) → 𝑐 ∈ No ) )
130	129	rexlimdva	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) → 𝑐 ∈ No ) )
131	130	abssdv	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ⊆ No )
132	45 82	addscld	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) ∈ No )
133		eleq1	⊢ ( 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) → ( 𝑑 ∈ No ↔ ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) ∈ No ) )
134	132 133	syl5ibrcom	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ( 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) → 𝑑 ∈ No ) )
135	134	rexlimdva	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) → 𝑑 ∈ No ) )
136	135	abssdv	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → { 𝑑 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) } ⊆ No )
137	131 136	unssd	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑑 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) } ) ⊆ No )
138		velsn	⊢ ( 𝑝 ∈ { 0s } ↔ 𝑝 = 0s )
139		elun	⊢ ( 𝑞 ∈ ( { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑑 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) } ) ↔ ( 𝑞 ∈ { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ∨ 𝑞 ∈ { 𝑑 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) } ) )
140		vex	⊢ 𝑞 ∈ V
141		eqeq1	⊢ ( 𝑐 = 𝑞 → ( 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) ↔ 𝑞 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) ) )
142	141	rexbidv	⊢ ( 𝑐 = 𝑞 → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑞 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) ) )
143	140 142	elab	⊢ ( 𝑞 ∈ { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑞 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) )
144		eqeq1	⊢ ( 𝑑 = 𝑞 → ( 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) ↔ 𝑞 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) ) )
145	144	rexbidv	⊢ ( 𝑑 = 𝑞 → ( ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) ↔ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑞 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) ) )
146	140 145	elab	⊢ ( 𝑞 ∈ { 𝑑 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) } ↔ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑞 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) )
147	143 146	orbi12i	⊢ ( ( 𝑞 ∈ { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ∨ 𝑞 ∈ { 𝑑 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) } ) ↔ ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑞 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) ∨ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑞 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) ) )
148	139 147	bitri	⊢ ( 𝑞 ∈ ( { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑑 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) } ) ↔ ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑞 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) ∨ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑞 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) ) )
149	138 148	anbi12i	⊢ ( ( 𝑝 ∈ { 0s } ∧ 𝑞 ∈ ( { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑑 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) } ) ) ↔ ( 𝑝 = 0s ∧ ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑞 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) ∨ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑞 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) ) ) )
150		ltnegsim	⊢ ( ( 𝑥 ∈ No ∧ 𝑥𝑅 ∈ No ) → ( 𝑥 <s 𝑥𝑅 → ( -us ‘ 𝑥𝑅 ) <s ( -us ‘ 𝑥 ) ) )
151	52 54 150	syl2anc	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ( 𝑥 <s 𝑥𝑅 → ( -us ‘ 𝑥𝑅 ) <s ( -us ‘ 𝑥 ) ) )
152	99 151	mpd	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ( -us ‘ 𝑥𝑅 ) <s ( -us ‘ 𝑥 ) )
153	55 126 54	ltadds2d	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ( ( -us ‘ 𝑥𝑅 ) <s ( -us ‘ 𝑥 ) ↔ ( 𝑥𝑅 +s ( -us ‘ 𝑥𝑅 ) ) <s ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) ) )
154	152 153	mpbid	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ( 𝑥𝑅 +s ( -us ‘ 𝑥𝑅 ) ) <s ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) )
155	109 154	eqbrtrrd	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → 0s <s ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) )
156		breq2	⊢ ( 𝑞 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) → ( 0s <s 𝑞 ↔ 0s <s ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) ) )
157	155 156	syl5ibrcom	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ( 𝑞 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) → 0s <s 𝑞 ) )
158	157	rexlimdva	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑞 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) → 0s <s 𝑞 ) )
159	158	imp	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑞 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) ) → 0s <s 𝑞 )
160	44 45 82	ltadds1d	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ( 𝑥𝐿 <s 𝑥 ↔ ( 𝑥𝐿 +s ( -us ‘ 𝑥𝐿 ) ) <s ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) ) )
161	78 160	mpbid	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ( 𝑥𝐿 +s ( -us ‘ 𝑥𝐿 ) ) <s ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) )
162	92 161	eqbrtrrd	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → 0s <s ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) )
163		breq2	⊢ ( 𝑞 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) → ( 0s <s 𝑞 ↔ 0s <s ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) ) )
164	162 163	syl5ibrcom	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ( 𝑞 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) → 0s <s 𝑞 ) )
165	164	rexlimdva	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑞 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) → 0s <s 𝑞 ) )
166	165	imp	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑞 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) ) → 0s <s 𝑞 )
167	159 166	jaodan	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑞 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) ∨ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑞 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) ) ) → 0s <s 𝑞 )
168		breq1	⊢ ( 𝑝 = 0s → ( 𝑝 <s 𝑞 ↔ 0s <s 𝑞 ) )
169	167 168	syl5ibrcom	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑞 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) ∨ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑞 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) ) ) → ( 𝑝 = 0s → 𝑝 <s 𝑞 ) )
170	169	ex	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑞 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) ∨ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑞 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) ) → ( 𝑝 = 0s → 𝑝 <s 𝑞 ) ) )
171	170	impcomd	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( ( 𝑝 = 0s ∧ ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑞 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) ∨ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑞 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) ) ) → 𝑝 <s 𝑞 ) )
172	149 171	biimtrid	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( ( 𝑝 ∈ { 0s } ∧ 𝑞 ∈ ( { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑑 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) } ) ) → 𝑝 <s 𝑞 ) )
173	172	3impib	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑝 ∈ { 0s } ∧ 𝑞 ∈ ( { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑑 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) } ) ) → 𝑝 <s 𝑞 )
174	42 125 64 137 173	sltsd	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → { 0s } <<s ( { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑑 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) } ) )
175	121 174	cuteq0	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑏 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑏 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) } ) |s ( { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑑 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) } ) ) = 0s )
176	34 175	eqtrid	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑏 ∣ ∃ 𝑝 ∈ ( -us “ ( R ‘ 𝑥 ) ) 𝑏 = ( 𝑥 +s 𝑝 ) } ) |s ( { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑑 ∣ ∃ 𝑞 ∈ ( -us “ ( L ‘ 𝑥 ) ) 𝑑 = ( 𝑥 +s 𝑞 ) } ) ) = 0s )
177	18 176	eqtrd	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( 𝑥 +s ( -us ‘ 𝑥 ) ) = 0s )
178	177	ex	⊢ ( 𝑥 ∈ No → ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s → ( 𝑥 +s ( -us ‘ 𝑥 ) ) = 0s ) )
179	4 8 178	noinds	⊢ ( 𝐴 ∈ No → ( 𝐴 +s ( -us ‘ 𝐴 ) ) = 0s )