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		lltropt	⊢ ( L ‘ 𝑥 ) <<s ( R ‘ 𝑥 )
10	9	a1i	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( L ‘ 𝑥 ) <<s ( R ‘ 𝑥 ) )
11		negscut2	⊢ ( 𝑥 ∈ 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	imaeqsexv	⊢ ( ( -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	imaeqsexv	⊢ ( ( -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		0sno	⊢ 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		leftval	⊢ ( L ‘ 𝑥 ) = { 𝑥𝐿 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ∣ 𝑥𝐿 <s 𝑥 }
78	77	reqabi	⊢ ( 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ↔ ( 𝑥𝐿 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ∧ 𝑥𝐿 <s 𝑥 ) )
79	78	simprbi	⊢ ( 𝑥𝐿 ∈ ( L ‘ 𝑥 ) → 𝑥𝐿 <s 𝑥 )
80	79	adantl	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → 𝑥𝐿 <s 𝑥 )
81		sltnegim	⊢ ( ( 𝑥𝐿 ∈ No ∧ 𝑥 ∈ No ) → ( 𝑥𝐿 <s 𝑥 → ( -us ‘ 𝑥 ) <s ( -us ‘ 𝑥𝐿 ) ) )
82	44 45 81	syl2anc	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ( 𝑥𝐿 <s 𝑥 → ( -us ‘ 𝑥 ) <s ( -us ‘ 𝑥𝐿 ) ) )
83	80 82	mpd	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ( -us ‘ 𝑥 ) <s ( -us ‘ 𝑥𝐿 ) )
84	44	negscld	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ( -us ‘ 𝑥𝐿 ) ∈ No )
85	46 84 44	sltadd2d	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ( ( -us ‘ 𝑥 ) <s ( -us ‘ 𝑥𝐿 ) ↔ ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) <s ( 𝑥𝐿 +s ( -us ‘ 𝑥𝐿 ) ) ) )
86	83 85	mpbid	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) <s ( 𝑥𝐿 +s ( -us ‘ 𝑥𝐿 ) ) )
87		id	⊢ ( 𝑥𝑂 = 𝑥𝐿 → 𝑥𝑂 = 𝑥𝐿 )
88		fveq2	⊢ ( 𝑥𝑂 = 𝑥𝐿 → ( -us ‘ 𝑥𝑂 ) = ( -us ‘ 𝑥𝐿 ) )
89	87 88	oveq12d	⊢ ( 𝑥𝑂 = 𝑥𝐿 → ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = ( 𝑥𝐿 +s ( -us ‘ 𝑥𝐿 ) ) )
90	89	eqeq1d	⊢ ( 𝑥𝑂 = 𝑥𝐿 → ( ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ↔ ( 𝑥𝐿 +s ( -us ‘ 𝑥𝐿 ) ) = 0s ) )
91		simplr	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s )
92		elun1	⊢ ( 𝑥𝐿 ∈ ( L ‘ 𝑥 ) → 𝑥𝐿 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
93	92	adantl	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → 𝑥𝐿 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
94	90 91 93	rspcdva	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ( 𝑥𝐿 +s ( -us ‘ 𝑥𝐿 ) ) = 0s )
95	86 94	breqtrd	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) <s 0s )
96		breq1	⊢ ( 𝑝 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) → ( 𝑝 <s 0s ↔ ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) <s 0s ) )
97	95 96	syl5ibrcom	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ( 𝑝 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) → 𝑝 <s 0s ) )
98	97	rexlimdva	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑝 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) → 𝑝 <s 0s ) )
99	98	imp	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑝 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) ) → 𝑝 <s 0s )
100		rightval	⊢ ( R ‘ 𝑥 ) = { 𝑥𝑅 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ∣ 𝑥 <s 𝑥𝑅 }
101	100	reqabi	⊢ ( 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ↔ ( 𝑥𝑅 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ∧ 𝑥 <s 𝑥𝑅 ) )
102	101	simprbi	⊢ ( 𝑥𝑅 ∈ ( R ‘ 𝑥 ) → 𝑥 <s 𝑥𝑅 )
103	102	adantl	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → 𝑥 <s 𝑥𝑅 )
104	52 54 55	sltadd1d	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ( 𝑥 <s 𝑥𝑅 ↔ ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) <s ( 𝑥𝑅 +s ( -us ‘ 𝑥𝑅 ) ) ) )
105	103 104	mpbid	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) <s ( 𝑥𝑅 +s ( -us ‘ 𝑥𝑅 ) ) )
106		id	⊢ ( 𝑥𝑂 = 𝑥𝑅 → 𝑥𝑂 = 𝑥𝑅 )
107		fveq2	⊢ ( 𝑥𝑂 = 𝑥𝑅 → ( -us ‘ 𝑥𝑂 ) = ( -us ‘ 𝑥𝑅 ) )
108	106 107	oveq12d	⊢ ( 𝑥𝑂 = 𝑥𝑅 → ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = ( 𝑥𝑅 +s ( -us ‘ 𝑥𝑅 ) ) )
109	108	eqeq1d	⊢ ( 𝑥𝑂 = 𝑥𝑅 → ( ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ↔ ( 𝑥𝑅 +s ( -us ‘ 𝑥𝑅 ) ) = 0s ) )
110		simplr	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s )
111		elun2	⊢ ( 𝑥𝑅 ∈ ( R ‘ 𝑥 ) → 𝑥𝑅 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
112	111	adantl	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → 𝑥𝑅 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
113	109 110 112	rspcdva	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ( 𝑥𝑅 +s ( -us ‘ 𝑥𝑅 ) ) = 0s )
114	105 113	breqtrd	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) <s 0s )
115		breq1	⊢ ( 𝑝 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) → ( 𝑝 <s 0s ↔ ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) <s 0s ) )
116	114 115	syl5ibrcom	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ( 𝑝 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) → 𝑝 <s 0s ) )
117	116	rexlimdva	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑝 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) → 𝑝 <s 0s ) )
118	117	imp	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑝 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) ) → 𝑝 <s 0s )
119	99 118	jaodan	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ ( ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑝 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) ∨ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑝 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) ) ) → 𝑝 <s 0s )
120		breq2	⊢ ( 𝑞 = 0s → ( 𝑝 <s 𝑞 ↔ 𝑝 <s 0s ) )
121	119 120	syl5ibrcom	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ ( ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑝 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) ∨ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑝 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) ) ) → ( 𝑞 = 0s → 𝑝 <s 𝑞 ) )
122	121	expimpd	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( ( ( ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑝 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) ∨ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑝 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) ) ∧ 𝑞 = 0s ) → 𝑝 <s 𝑞 ) )
123	76 122	biimtrid	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( ( 𝑝 ∈ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑏 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑏 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) } ) ∧ 𝑞 ∈ { 0s } ) → 𝑝 <s 𝑞 ) )
124	123	3impib	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑝 ∈ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑏 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑏 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) } ) ∧ 𝑞 ∈ { 0s } ) → 𝑝 <s 𝑞 )
125	40 42 61 64 124	ssltd	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑏 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑏 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) } ) <<s { 0s } )
126	37	abrexex	⊢ { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ∈ V
127	35	abrexex	⊢ { 𝑑 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) } ∈ V
128	126 127	unex	⊢ ( { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑑 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) } ) ∈ V
129	128	a1i	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑑 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) } ) ∈ V )
130	52	negscld	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ( -us ‘ 𝑥 ) ∈ No )
131	54 130	addscld	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) ∈ No )
132		eleq1	⊢ ( 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) → ( 𝑐 ∈ No ↔ ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) ∈ No ) )
133	131 132	syl5ibrcom	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ( 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) → 𝑐 ∈ No ) )
134	133	rexlimdva	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) → 𝑐 ∈ No ) )
135	134	abssdv	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ⊆ No )
136	45 84	addscld	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) ∈ No )
137		eleq1	⊢ ( 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) → ( 𝑑 ∈ No ↔ ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) ∈ No ) )
138	136 137	syl5ibrcom	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ( 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) → 𝑑 ∈ No ) )
139	138	rexlimdva	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) → 𝑑 ∈ No ) )
140	139	abssdv	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → { 𝑑 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) } ⊆ No )
141	135 140	unssd	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑑 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) } ) ⊆ No )
142		velsn	⊢ ( 𝑝 ∈ { 0s } ↔ 𝑝 = 0s )
143		elun	⊢ ( 𝑞 ∈ ( { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑑 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) } ) ↔ ( 𝑞 ∈ { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ∨ 𝑞 ∈ { 𝑑 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) } ) )
144		vex	⊢ 𝑞 ∈ V
145		eqeq1	⊢ ( 𝑐 = 𝑞 → ( 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) ↔ 𝑞 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) ) )
146	145	rexbidv	⊢ ( 𝑐 = 𝑞 → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑞 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) ) )
147	144 146	elab	⊢ ( 𝑞 ∈ { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑞 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) )
148		eqeq1	⊢ ( 𝑑 = 𝑞 → ( 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) ↔ 𝑞 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) ) )
149	148	rexbidv	⊢ ( 𝑑 = 𝑞 → ( ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) ↔ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑞 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) ) )
150	144 149	elab	⊢ ( 𝑞 ∈ { 𝑑 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) } ↔ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑞 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) )
151	147 150	orbi12i	⊢ ( ( 𝑞 ∈ { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ∨ 𝑞 ∈ { 𝑑 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) } ) ↔ ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑞 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) ∨ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑞 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) ) )
152	143 151	bitri	⊢ ( 𝑞 ∈ ( { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑑 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) } ) ↔ ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑞 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) ∨ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑞 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) ) )
153	142 152	anbi12i	⊢ ( ( 𝑝 ∈ { 0s } ∧ 𝑞 ∈ ( { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑑 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) } ) ) ↔ ( 𝑝 = 0s ∧ ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑞 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) ∨ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑞 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) ) ) )
154		sltnegim	⊢ ( ( 𝑥 ∈ No ∧ 𝑥𝑅 ∈ No ) → ( 𝑥 <s 𝑥𝑅 → ( -us ‘ 𝑥𝑅 ) <s ( -us ‘ 𝑥 ) ) )
155	52 54 154	syl2anc	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ( 𝑥 <s 𝑥𝑅 → ( -us ‘ 𝑥𝑅 ) <s ( -us ‘ 𝑥 ) ) )
156	103 155	mpd	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ( -us ‘ 𝑥𝑅 ) <s ( -us ‘ 𝑥 ) )
157	55 130 54	sltadd2d	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ( ( -us ‘ 𝑥𝑅 ) <s ( -us ‘ 𝑥 ) ↔ ( 𝑥𝑅 +s ( -us ‘ 𝑥𝑅 ) ) <s ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) ) )
158	156 157	mpbid	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ( 𝑥𝑅 +s ( -us ‘ 𝑥𝑅 ) ) <s ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) )
159	113 158	eqbrtrrd	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → 0s <s ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) )
160		breq2	⊢ ( 𝑞 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) → ( 0s <s 𝑞 ↔ 0s <s ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) ) )
161	159 160	syl5ibrcom	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ( 𝑞 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) → 0s <s 𝑞 ) )
162	161	rexlimdva	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑞 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) → 0s <s 𝑞 ) )
163	162	imp	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑞 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) ) → 0s <s 𝑞 )
164	44 45 84	sltadd1d	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ( 𝑥𝐿 <s 𝑥 ↔ ( 𝑥𝐿 +s ( -us ‘ 𝑥𝐿 ) ) <s ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) ) )
165	80 164	mpbid	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ( 𝑥𝐿 +s ( -us ‘ 𝑥𝐿 ) ) <s ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) )
166	94 165	eqbrtrrd	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → 0s <s ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) )
167		breq2	⊢ ( 𝑞 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) → ( 0s <s 𝑞 ↔ 0s <s ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) ) )
168	166 167	syl5ibrcom	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ( 𝑞 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) → 0s <s 𝑞 ) )
169	168	rexlimdva	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑞 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) → 0s <s 𝑞 ) )
170	169	imp	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑞 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) ) → 0s <s 𝑞 )
171	163 170	jaodan	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑞 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) ∨ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑞 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) ) ) → 0s <s 𝑞 )
172		breq1	⊢ ( 𝑝 = 0s → ( 𝑝 <s 𝑞 ↔ 0s <s 𝑞 ) )
173	171 172	syl5ibrcom	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑞 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) ∨ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑞 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) ) ) → ( 𝑝 = 0s → 𝑝 <s 𝑞 ) )
174	173	ex	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑞 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) ∨ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑞 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) ) → ( 𝑝 = 0s → 𝑝 <s 𝑞 ) ) )
175	174	impcomd	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( ( 𝑝 = 0s ∧ ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑞 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) ∨ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑞 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) ) ) → 𝑝 <s 𝑞 ) )
176	153 175	biimtrid	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( ( 𝑝 ∈ { 0s } ∧ 𝑞 ∈ ( { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑑 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) } ) ) → 𝑝 <s 𝑞 ) )
177	176	3impib	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) ∧ 𝑝 ∈ { 0s } ∧ 𝑞 ∈ ( { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑑 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) } ) ) → 𝑝 <s 𝑞 )
178	42 129 64 141 177	ssltd	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → { 0s } <<s ( { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑑 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) } ) )
179	125 178	cuteq0	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑏 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑏 = ( 𝑥 +s ( -us ‘ 𝑥𝑅 ) ) } ) |s ( { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑑 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑑 = ( 𝑥 +s ( -us ‘ 𝑥𝐿 ) ) } ) ) = 0s )
180	34 179	eqtrid	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( 𝑥𝐿 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑏 ∣ ∃ 𝑝 ∈ ( -us “ ( R ‘ 𝑥 ) ) 𝑏 = ( 𝑥 +s 𝑝 ) } ) |s ( { 𝑐 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑐 = ( 𝑥𝑅 +s ( -us ‘ 𝑥 ) ) } ∪ { 𝑑 ∣ ∃ 𝑞 ∈ ( -us “ ( L ‘ 𝑥 ) ) 𝑑 = ( 𝑥 +s 𝑞 ) } ) ) = 0s )
181	18 180	eqtrd	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s ) → ( 𝑥 +s ( -us ‘ 𝑥 ) ) = 0s )
182	181	ex	⊢ ( 𝑥 ∈ No → ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 +s ( -us ‘ 𝑥𝑂 ) ) = 0s → ( 𝑥 +s ( -us ‘ 𝑥 ) ) = 0s ) )
183	4 8 182	noinds	⊢ ( 𝐴 ∈ No → ( 𝐴 +s ( -us ‘ 𝐴 ) ) = 0s )