Theorem elreno2 28760

Description: Alternate characterization of the surreal reals. Theorem 4.4(b) of [Gonshor] p. 39. (Contributed by Scott Fenton, 29-Jan-2026.)

Assertion

Ref	Expression
elreno2	⊢ (𝐴 ∈ ℝs ↔ (𝐴 ∈ No ∧ (∃𝑛 ∈ ℕs (( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∃𝑛 ∈ ℕs ( 1s /su 𝑛) ≤s (abss‘(𝐴 -s 𝑥𝑂)))))

Distinct variable group:   𝐴,𝑛,𝑥_𝑂

Proof of Theorem elreno2

Dummy variables 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elreno 28756	. 2 ⊢ (𝐴 ∈ ℝs ↔ (𝐴 ∈ No ∧ (∃𝑛 ∈ ℕs (( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ 𝐴 = ({𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))} |s {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))}))))
2		recut 28759	. . . . . . . . . 10 ⊢ (𝐴 ∈ No → {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))} <<s {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))})
3	2	adantr 486	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ 𝐴 = ({𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))} |s {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))})) → {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))} <<s {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))})
4		simpr 490	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ 𝐴 = ({𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))} |s {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))})) → 𝐴 = ({𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))} |s {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))}))
5	3, 4	cofcutr1d 28190	. . . . . . . 8 ⊢ ((𝐴 ∈ No ∧ 𝐴 = ({𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))} |s {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))})) → ∀𝑥𝑂 ∈ ( L ‘𝐴)∃𝑦 ∈ {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))}𝑥𝑂 ≤s 𝑦)
6		eqeq1 2764	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑦 → (𝑤 = (𝐴 -s ( 1s /su 𝑛)) ↔ 𝑦 = (𝐴 -s ( 1s /su 𝑛))))
7	6	rexbidv 3186	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑦 → (∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛)) ↔ ∃𝑛 ∈ ℕs 𝑦 = (𝐴 -s ( 1s /su 𝑛))))
8	7	rexab 3653	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))}𝑥𝑂 ≤s 𝑦 ↔ ∃𝑦(∃𝑛 ∈ ℕs 𝑦 = (𝐴 -s ( 1s /su 𝑛)) ∧ 𝑥𝑂 ≤s 𝑦))
9		rexcom4 3289	. . . . . . . . . . . 12 ⊢ (∃𝑛 ∈ ℕs ∃𝑦(𝑦 = (𝐴 -s ( 1s /su 𝑛)) ∧ 𝑥𝑂 ≤s 𝑦) ↔ ∃𝑦∃𝑛 ∈ ℕs (𝑦 = (𝐴 -s ( 1s /su 𝑛)) ∧ 𝑥𝑂 ≤s 𝑦))
10		ovex 7446	. . . . . . . . . . . . . 14 ⊢ (𝐴 -s ( 1s /su 𝑛)) ∈ V
11		breq2 5107	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝐴 -s ( 1s /su 𝑛)) → (𝑥𝑂 ≤s 𝑦 ↔ 𝑥𝑂 ≤s (𝐴 -s ( 1s /su 𝑛))))
12	10, 11	ceqsexv 3498	. . . . . . . . . . . . 13 ⊢ (∃𝑦(𝑦 = (𝐴 -s ( 1s /su 𝑛)) ∧ 𝑥𝑂 ≤s 𝑦) ↔ 𝑥𝑂 ≤s (𝐴 -s ( 1s /su 𝑛)))
13	12	rexbii 3109	. . . . . . . . . . . 12 ⊢ (∃𝑛 ∈ ℕs ∃𝑦(𝑦 = (𝐴 -s ( 1s /su 𝑛)) ∧ 𝑥𝑂 ≤s 𝑦) ↔ ∃𝑛 ∈ ℕs 𝑥𝑂 ≤s (𝐴 -s ( 1s /su 𝑛)))
14		r19.41v 3192	. . . . . . . . . . . . 13 ⊢ (∃𝑛 ∈ ℕs (𝑦 = (𝐴 -s ( 1s /su 𝑛)) ∧ 𝑥𝑂 ≤s 𝑦) ↔ (∃𝑛 ∈ ℕs 𝑦 = (𝐴 -s ( 1s /su 𝑛)) ∧ 𝑥𝑂 ≤s 𝑦))
15	14	exbii 1881	. . . . . . . . . . . 12 ⊢ (∃𝑦∃𝑛 ∈ ℕs (𝑦 = (𝐴 -s ( 1s /su 𝑛)) ∧ 𝑥𝑂 ≤s 𝑦) ↔ ∃𝑦(∃𝑛 ∈ ℕs 𝑦 = (𝐴 -s ( 1s /su 𝑛)) ∧ 𝑥𝑂 ≤s 𝑦))
16	9, 13, 15	3bitr3ri 305	. . . . . . . . . . 11 ⊢ (∃𝑦(∃𝑛 ∈ ℕs 𝑦 = (𝐴 -s ( 1s /su 𝑛)) ∧ 𝑥𝑂 ≤s 𝑦) ↔ ∃𝑛 ∈ ℕs 𝑥𝑂 ≤s (𝐴 -s ( 1s /su 𝑛)))
17	8, 16	bitri 278	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))}𝑥𝑂 ≤s 𝑦 ↔ ∃𝑛 ∈ ℕs 𝑥𝑂 ≤s (𝐴 -s ( 1s /su 𝑛)))
18		leftno 28142	. . . . . . . . . . . . . . . 16 ⊢ (𝑥𝑂 ∈ ( L ‘𝐴) → 𝑥𝑂 ∈ No )
19	18	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( L ‘𝐴)) → 𝑥𝑂 ∈ No )
20	19	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( L ‘𝐴)) ∧ 𝑛 ∈ ℕs) → 𝑥𝑂 ∈ No )
21		simpll 779	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( L ‘𝐴)) ∧ 𝑛 ∈ ℕs) → 𝐴 ∈ No )
22		1no 28075	. . . . . . . . . . . . . . . . . 18 ⊢ 1s ∈ No
23	22	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕs → 1s ∈ No )
24		nnno 28589	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕs → 𝑛 ∈ No )
25		nnne0s 28602	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕs → 𝑛 ≠ 0s )
26	23, 24, 25	divscld 28489	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕs → ( 1s /su 𝑛) ∈ No )
27	26	adantl 487	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( L ‘𝐴)) ∧ 𝑛 ∈ ℕs) → ( 1s /su 𝑛) ∈ No )
28	21, 27	subscld 28328	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( L ‘𝐴)) ∧ 𝑛 ∈ ℕs) → (𝐴 -s ( 1s /su 𝑛)) ∈ No )
29	20, 28, 27	leadds1d 28260	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( L ‘𝐴)) ∧ 𝑛 ∈ ℕs) → (𝑥𝑂 ≤s (𝐴 -s ( 1s /su 𝑛)) ↔ (𝑥𝑂 +s ( 1s /su 𝑛)) ≤s ((𝐴 -s ( 1s /su 𝑛)) +s ( 1s /su 𝑛))))
30		npcans 28340	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ No ∧ ( 1s /su 𝑛) ∈ No ) → ((𝐴 -s ( 1s /su 𝑛)) +s ( 1s /su 𝑛)) = 𝐴)
31	21, 27, 30	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( L ‘𝐴)) ∧ 𝑛 ∈ ℕs) → ((𝐴 -s ( 1s /su 𝑛)) +s ( 1s /su 𝑛)) = 𝐴)
32	31	breq2d 5115	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( L ‘𝐴)) ∧ 𝑛 ∈ ℕs) → ((𝑥𝑂 +s ( 1s /su 𝑛)) ≤s ((𝐴 -s ( 1s /su 𝑛)) +s ( 1s /su 𝑛)) ↔ (𝑥𝑂 +s ( 1s /su 𝑛)) ≤s 𝐴))
33	29, 32	bitrd 282	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( L ‘𝐴)) ∧ 𝑛 ∈ ℕs) → (𝑥𝑂 ≤s (𝐴 -s ( 1s /su 𝑛)) ↔ (𝑥𝑂 +s ( 1s /su 𝑛)) ≤s 𝐴))
34	33	rexbidva 3184	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( L ‘𝐴)) → (∃𝑛 ∈ ℕs 𝑥𝑂 ≤s (𝐴 -s ( 1s /su 𝑛)) ↔ ∃𝑛 ∈ ℕs (𝑥𝑂 +s ( 1s /su 𝑛)) ≤s 𝐴))
35	34	adantlr 728	. . . . . . . . . 10 ⊢ (((𝐴 ∈ No ∧ 𝐴 = ({𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))} |s {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))})) ∧ 𝑥𝑂 ∈ ( L ‘𝐴)) → (∃𝑛 ∈ ℕs 𝑥𝑂 ≤s (𝐴 -s ( 1s /su 𝑛)) ↔ ∃𝑛 ∈ ℕs (𝑥𝑂 +s ( 1s /su 𝑛)) ≤s 𝐴))
36	17, 35	bitrid 286	. . . . . . . . 9 ⊢ (((𝐴 ∈ No ∧ 𝐴 = ({𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))} |s {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))})) ∧ 𝑥𝑂 ∈ ( L ‘𝐴)) → (∃𝑦 ∈ {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))}𝑥𝑂 ≤s 𝑦 ↔ ∃𝑛 ∈ ℕs (𝑥𝑂 +s ( 1s /su 𝑛)) ≤s 𝐴))
37	36	ralbidva 3183	. . . . . . . 8 ⊢ ((𝐴 ∈ No ∧ 𝐴 = ({𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))} |s {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))})) → (∀𝑥𝑂 ∈ ( L ‘𝐴)∃𝑦 ∈ {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))}𝑥𝑂 ≤s 𝑦 ↔ ∀𝑥𝑂 ∈ ( L ‘𝐴)∃𝑛 ∈ ℕs (𝑥𝑂 +s ( 1s /su 𝑛)) ≤s 𝐴))
38	5, 37	mpbid 235	. . . . . . 7 ⊢ ((𝐴 ∈ No ∧ 𝐴 = ({𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))} |s {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))})) → ∀𝑥𝑂 ∈ ( L ‘𝐴)∃𝑛 ∈ ℕs (𝑥𝑂 +s ( 1s /su 𝑛)) ≤s 𝐴)
39	3, 4	cofcutr2d 28191	. . . . . . . 8 ⊢ ((𝐴 ∈ No ∧ 𝐴 = ({𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))} |s {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))})) → ∀𝑥𝑂 ∈ ( R ‘𝐴)∃𝑦 ∈ {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))}𝑦 ≤s 𝑥𝑂)
40		eqeq1 2764	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑦 → (𝑤 = (𝐴 +s ( 1s /su 𝑛)) ↔ 𝑦 = (𝐴 +s ( 1s /su 𝑛))))
41	40	rexbidv 3186	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑦 → (∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛)) ↔ ∃𝑛 ∈ ℕs 𝑦 = (𝐴 +s ( 1s /su 𝑛))))
42	41	rexab 3653	. . . . . . . . . . . 12 ⊢ (∃𝑦 ∈ {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))}𝑦 ≤s 𝑥𝑂 ↔ ∃𝑦(∃𝑛 ∈ ℕs 𝑦 = (𝐴 +s ( 1s /su 𝑛)) ∧ 𝑦 ≤s 𝑥𝑂))
43		rexcom4 3289	. . . . . . . . . . . . 13 ⊢ (∃𝑛 ∈ ℕs ∃𝑦(𝑦 = (𝐴 +s ( 1s /su 𝑛)) ∧ 𝑦 ≤s 𝑥𝑂) ↔ ∃𝑦∃𝑛 ∈ ℕs (𝑦 = (𝐴 +s ( 1s /su 𝑛)) ∧ 𝑦 ≤s 𝑥𝑂))
44		ovex 7446	. . . . . . . . . . . . . . 15 ⊢ (𝐴 +s ( 1s /su 𝑛)) ∈ V
45		breq1 5106	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝐴 +s ( 1s /su 𝑛)) → (𝑦 ≤s 𝑥𝑂 ↔ (𝐴 +s ( 1s /su 𝑛)) ≤s 𝑥𝑂))
46	44, 45	ceqsexv 3498	. . . . . . . . . . . . . 14 ⊢ (∃𝑦(𝑦 = (𝐴 +s ( 1s /su 𝑛)) ∧ 𝑦 ≤s 𝑥𝑂) ↔ (𝐴 +s ( 1s /su 𝑛)) ≤s 𝑥𝑂)
47	46	rexbii 3109	. . . . . . . . . . . . 13 ⊢ (∃𝑛 ∈ ℕs ∃𝑦(𝑦 = (𝐴 +s ( 1s /su 𝑛)) ∧ 𝑦 ≤s 𝑥𝑂) ↔ ∃𝑛 ∈ ℕs (𝐴 +s ( 1s /su 𝑛)) ≤s 𝑥𝑂)
48		r19.41v 3192	. . . . . . . . . . . . . 14 ⊢ (∃𝑛 ∈ ℕs (𝑦 = (𝐴 +s ( 1s /su 𝑛)) ∧ 𝑦 ≤s 𝑥𝑂) ↔ (∃𝑛 ∈ ℕs 𝑦 = (𝐴 +s ( 1s /su 𝑛)) ∧ 𝑦 ≤s 𝑥𝑂))
49	48	exbii 1881	. . . . . . . . . . . . 13 ⊢ (∃𝑦∃𝑛 ∈ ℕs (𝑦 = (𝐴 +s ( 1s /su 𝑛)) ∧ 𝑦 ≤s 𝑥𝑂) ↔ ∃𝑦(∃𝑛 ∈ ℕs 𝑦 = (𝐴 +s ( 1s /su 𝑛)) ∧ 𝑦 ≤s 𝑥𝑂))
50	43, 47, 49	3bitr3ri 305	. . . . . . . . . . . 12 ⊢ (∃𝑦(∃𝑛 ∈ ℕs 𝑦 = (𝐴 +s ( 1s /su 𝑛)) ∧ 𝑦 ≤s 𝑥𝑂) ↔ ∃𝑛 ∈ ℕs (𝐴 +s ( 1s /su 𝑛)) ≤s 𝑥𝑂)
51	42, 50	bitri 278	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))}𝑦 ≤s 𝑥𝑂 ↔ ∃𝑛 ∈ ℕs (𝐴 +s ( 1s /su 𝑛)) ≤s 𝑥𝑂)
52		simpll 779	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( R ‘𝐴)) ∧ 𝑛 ∈ ℕs) → 𝐴 ∈ No )
53		rightno 28143	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥𝑂 ∈ ( R ‘𝐴) → 𝑥𝑂 ∈ No )
54	53	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( R ‘𝐴)) → 𝑥𝑂 ∈ No )
55	54	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( R ‘𝐴)) ∧ 𝑛 ∈ ℕs) → 𝑥𝑂 ∈ No )
56	26	adantl 487	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( R ‘𝐴)) ∧ 𝑛 ∈ ℕs) → ( 1s /su 𝑛) ∈ No )
57	55, 56	subscld 28328	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( R ‘𝐴)) ∧ 𝑛 ∈ ℕs) → (𝑥𝑂 -s ( 1s /su 𝑛)) ∈ No )
58	52, 57, 56	leadds1d 28260	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( R ‘𝐴)) ∧ 𝑛 ∈ ℕs) → (𝐴 ≤s (𝑥𝑂 -s ( 1s /su 𝑛)) ↔ (𝐴 +s ( 1s /su 𝑛)) ≤s ((𝑥𝑂 -s ( 1s /su 𝑛)) +s ( 1s /su 𝑛))))
59		npcans 28340	. . . . . . . . . . . . . . 15 ⊢ ((𝑥𝑂 ∈ No ∧ ( 1s /su 𝑛) ∈ No ) → ((𝑥𝑂 -s ( 1s /su 𝑛)) +s ( 1s /su 𝑛)) = 𝑥𝑂)
60	55, 56, 59	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( R ‘𝐴)) ∧ 𝑛 ∈ ℕs) → ((𝑥𝑂 -s ( 1s /su 𝑛)) +s ( 1s /su 𝑛)) = 𝑥𝑂)
61	60	breq2d 5115	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( R ‘𝐴)) ∧ 𝑛 ∈ ℕs) → ((𝐴 +s ( 1s /su 𝑛)) ≤s ((𝑥𝑂 -s ( 1s /su 𝑛)) +s ( 1s /su 𝑛)) ↔ (𝐴 +s ( 1s /su 𝑛)) ≤s 𝑥𝑂))
62	58, 61	bitr2d 283	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( R ‘𝐴)) ∧ 𝑛 ∈ ℕs) → ((𝐴 +s ( 1s /su 𝑛)) ≤s 𝑥𝑂 ↔ 𝐴 ≤s (𝑥𝑂 -s ( 1s /su 𝑛))))
63	62	rexbidva 3184	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( R ‘𝐴)) → (∃𝑛 ∈ ℕs (𝐴 +s ( 1s /su 𝑛)) ≤s 𝑥𝑂 ↔ ∃𝑛 ∈ ℕs 𝐴 ≤s (𝑥𝑂 -s ( 1s /su 𝑛))))
64	51, 63	bitrid 286	. . . . . . . . . 10 ⊢ ((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( R ‘𝐴)) → (∃𝑦 ∈ {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))}𝑦 ≤s 𝑥𝑂 ↔ ∃𝑛 ∈ ℕs 𝐴 ≤s (𝑥𝑂 -s ( 1s /su 𝑛))))
65	64	ralbidva 3183	. . . . . . . . 9 ⊢ (𝐴 ∈ No → (∀𝑥𝑂 ∈ ( R ‘𝐴)∃𝑦 ∈ {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))}𝑦 ≤s 𝑥𝑂 ↔ ∀𝑥𝑂 ∈ ( R ‘𝐴)∃𝑛 ∈ ℕs 𝐴 ≤s (𝑥𝑂 -s ( 1s /su 𝑛))))
66	65	adantr 486	. . . . . . . 8 ⊢ ((𝐴 ∈ No ∧ 𝐴 = ({𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))} |s {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))})) → (∀𝑥𝑂 ∈ ( R ‘𝐴)∃𝑦 ∈ {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))}𝑦 ≤s 𝑥𝑂 ↔ ∀𝑥𝑂 ∈ ( R ‘𝐴)∃𝑛 ∈ ℕs 𝐴 ≤s (𝑥𝑂 -s ( 1s /su 𝑛))))
67	39, 66	mpbid 235	. . . . . . 7 ⊢ ((𝐴 ∈ No ∧ 𝐴 = ({𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))} |s {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))})) → ∀𝑥𝑂 ∈ ( R ‘𝐴)∃𝑛 ∈ ℕs 𝐴 ≤s (𝑥𝑂 -s ( 1s /su 𝑛)))
68	38, 67	jca 521	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ 𝐴 = ({𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))} |s {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))})) → (∀𝑥𝑂 ∈ ( L ‘𝐴)∃𝑛 ∈ ℕs (𝑥𝑂 +s ( 1s /su 𝑛)) ≤s 𝐴 ∧ ∀𝑥𝑂 ∈ ( R ‘𝐴)∃𝑛 ∈ ℕs 𝐴 ≤s (𝑥𝑂 -s ( 1s /su 𝑛))))
69		lrcut 28169	. . . . . . . 8 ⊢ (𝐴 ∈ No → (( L ‘𝐴) |s ( R ‘𝐴)) = 𝐴)
70	69	adantr 486	. . . . . . 7 ⊢ ((𝐴 ∈ No ∧ (∀𝑥𝑂 ∈ ( L ‘𝐴)∃𝑛 ∈ ℕs (𝑥𝑂 +s ( 1s /su 𝑛)) ≤s 𝐴 ∧ ∀𝑥𝑂 ∈ ( R ‘𝐴)∃𝑛 ∈ ℕs 𝐴 ≤s (𝑥𝑂 -s ( 1s /su 𝑛)))) → (( L ‘𝐴) |s ( R ‘𝐴)) = 𝐴)
71		lltr 28127	. . . . . . . . 9 ⊢ ( L ‘𝐴) <<s ( R ‘𝐴)
72	71	a1i 11	. . . . . . . 8 ⊢ ((𝐴 ∈ No ∧ (∀𝑥𝑂 ∈ ( L ‘𝐴)∃𝑛 ∈ ℕs (𝑥𝑂 +s ( 1s /su 𝑛)) ≤s 𝐴 ∧ ∀𝑥𝑂 ∈ ( R ‘𝐴)∃𝑛 ∈ ℕs 𝐴 ≤s (𝑥𝑂 -s ( 1s /su 𝑛)))) → ( L ‘𝐴) <<s ( R ‘𝐴))
73	34	biimpar 483	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( L ‘𝐴)) ∧ ∃𝑛 ∈ ℕs (𝑥𝑂 +s ( 1s /su 𝑛)) ≤s 𝐴) → ∃𝑛 ∈ ℕs 𝑥𝑂 ≤s (𝐴 -s ( 1s /su 𝑛)))
74	73, 17	sylibr 237	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( L ‘𝐴)) ∧ ∃𝑛 ∈ ℕs (𝑥𝑂 +s ( 1s /su 𝑛)) ≤s 𝐴) → ∃𝑦 ∈ {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))}𝑥𝑂 ≤s 𝑦)
75	74	ex 418	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( L ‘𝐴)) → (∃𝑛 ∈ ℕs (𝑥𝑂 +s ( 1s /su 𝑛)) ≤s 𝐴 → ∃𝑦 ∈ {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))}𝑥𝑂 ≤s 𝑦))
76	75	ralimdva 3174	. . . . . . . . . 10 ⊢ (𝐴 ∈ No → (∀𝑥𝑂 ∈ ( L ‘𝐴)∃𝑛 ∈ ℕs (𝑥𝑂 +s ( 1s /su 𝑛)) ≤s 𝐴 → ∀𝑥𝑂 ∈ ( L ‘𝐴)∃𝑦 ∈ {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))}𝑥𝑂 ≤s 𝑦))
77	76	imp 412	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ ∀𝑥𝑂 ∈ ( L ‘𝐴)∃𝑛 ∈ ℕs (𝑥𝑂 +s ( 1s /su 𝑛)) ≤s 𝐴) → ∀𝑥𝑂 ∈ ( L ‘𝐴)∃𝑦 ∈ {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))}𝑥𝑂 ≤s 𝑦)
78	77	adantrr 730	. . . . . . . 8 ⊢ ((𝐴 ∈ No ∧ (∀𝑥𝑂 ∈ ( L ‘𝐴)∃𝑛 ∈ ℕs (𝑥𝑂 +s ( 1s /su 𝑛)) ≤s 𝐴 ∧ ∀𝑥𝑂 ∈ ( R ‘𝐴)∃𝑛 ∈ ℕs 𝐴 ≤s (𝑥𝑂 -s ( 1s /su 𝑛)))) → ∀𝑥𝑂 ∈ ( L ‘𝐴)∃𝑦 ∈ {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))}𝑥𝑂 ≤s 𝑦)
79	63	biimpar 483	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( R ‘𝐴)) ∧ ∃𝑛 ∈ ℕs 𝐴 ≤s (𝑥𝑂 -s ( 1s /su 𝑛))) → ∃𝑛 ∈ ℕs (𝐴 +s ( 1s /su 𝑛)) ≤s 𝑥𝑂)
80	79, 51	sylibr 237	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( R ‘𝐴)) ∧ ∃𝑛 ∈ ℕs 𝐴 ≤s (𝑥𝑂 -s ( 1s /su 𝑛))) → ∃𝑦 ∈ {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))}𝑦 ≤s 𝑥𝑂)
81	80	ex 418	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( R ‘𝐴)) → (∃𝑛 ∈ ℕs 𝐴 ≤s (𝑥𝑂 -s ( 1s /su 𝑛)) → ∃𝑦 ∈ {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))}𝑦 ≤s 𝑥𝑂))
82	81	ralimdva 3174	. . . . . . . . . 10 ⊢ (𝐴 ∈ No → (∀𝑥𝑂 ∈ ( R ‘𝐴)∃𝑛 ∈ ℕs 𝐴 ≤s (𝑥𝑂 -s ( 1s /su 𝑛)) → ∀𝑥𝑂 ∈ ( R ‘𝐴)∃𝑦 ∈ {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))}𝑦 ≤s 𝑥𝑂))
83	82	imp 412	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ ∀𝑥𝑂 ∈ ( R ‘𝐴)∃𝑛 ∈ ℕs 𝐴 ≤s (𝑥𝑂 -s ( 1s /su 𝑛))) → ∀𝑥𝑂 ∈ ( R ‘𝐴)∃𝑦 ∈ {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))}𝑦 ≤s 𝑥𝑂)
84	83	adantrl 729	. . . . . . . 8 ⊢ ((𝐴 ∈ No ∧ (∀𝑥𝑂 ∈ ( L ‘𝐴)∃𝑛 ∈ ℕs (𝑥𝑂 +s ( 1s /su 𝑛)) ≤s 𝐴 ∧ ∀𝑥𝑂 ∈ ( R ‘𝐴)∃𝑛 ∈ ℕs 𝐴 ≤s (𝑥𝑂 -s ( 1s /su 𝑛)))) → ∀𝑥𝑂 ∈ ( R ‘𝐴)∃𝑦 ∈ {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))}𝑦 ≤s 𝑥𝑂)
85		nnsex 28583	. . . . . . . . . . . . 13 ⊢ ℕs ∈ V
86	85	abrexex 7959	. . . . . . . . . . . 12 ⊢ {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))} ∈ V
87	86	a1i 11	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))} ∈ V)
88		snexg 5405	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → {𝐴} ∈ V)
89		simpl 488	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ No ∧ 𝑛 ∈ ℕs) → 𝐴 ∈ No )
90	26	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ No ∧ 𝑛 ∈ ℕs) → ( 1s /su 𝑛) ∈ No )
91	89, 90	subscld 28328	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ No ∧ 𝑛 ∈ ℕs) → (𝐴 -s ( 1s /su 𝑛)) ∈ No )
92		eleq1 2848	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝐴 -s ( 1s /su 𝑛)) → (𝑤 ∈ No ↔ (𝐴 -s ( 1s /su 𝑛)) ∈ No ))
93	91, 92	syl5ibrcom 250	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ No ∧ 𝑛 ∈ ℕs) → (𝑤 = (𝐴 -s ( 1s /su 𝑛)) → 𝑤 ∈ No ))
94	93	rexlimdva 3163	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ No → (∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛)) → 𝑤 ∈ No ))
95	94	abssdv 4015	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))} ⊆ No )
96		snssi 4746	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → {𝐴} ⊆ No )
97		biid 264	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ No ↔ 𝐴 ∈ No )
98		vex 3454	. . . . . . . . . . . . 13 ⊢ 𝑦 ∈ V
99	98, 7	elab 3633	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))} ↔ ∃𝑛 ∈ ℕs 𝑦 = (𝐴 -s ( 1s /su 𝑛)))
100		velsn 4600	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ {𝐴} ↔ 𝑧 = 𝐴)
101		id 23	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕs → 𝑛 ∈ ℕs)
102	101	nnsrecgt0d 28616	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕs → 0s <s ( 1s /su 𝑛))
103	102	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ No ∧ 𝑛 ∈ ℕs) → 0s <s ( 1s /su 𝑛))
104	90, 89	ltsubsposd 28364	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ No ∧ 𝑛 ∈ ℕs) → ( 0s <s ( 1s /su 𝑛) ↔ (𝐴 -s ( 1s /su 𝑛)) <s 𝐴))
105	103, 104	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ No ∧ 𝑛 ∈ ℕs) → (𝐴 -s ( 1s /su 𝑛)) <s 𝐴)
106		breq12 5108	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 = (𝐴 -s ( 1s /su 𝑛)) ∧ 𝑧 = 𝐴) → (𝑦 <s 𝑧 ↔ (𝐴 -s ( 1s /su 𝑛)) <s 𝐴))
107	105, 106	syl5ibrcom 250	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ No ∧ 𝑛 ∈ ℕs) → ((𝑦 = (𝐴 -s ( 1s /su 𝑛)) ∧ 𝑧 = 𝐴) → 𝑦 <s 𝑧))
108	107	expd 421	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ No ∧ 𝑛 ∈ ℕs) → (𝑦 = (𝐴 -s ( 1s /su 𝑛)) → (𝑧 = 𝐴 → 𝑦 <s 𝑧)))
109	108	rexlimdva 3163	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ No → (∃𝑛 ∈ ℕs 𝑦 = (𝐴 -s ( 1s /su 𝑛)) → (𝑧 = 𝐴 → 𝑦 <s 𝑧)))
110	109	3imp 1128	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ No ∧ ∃𝑛 ∈ ℕs 𝑦 = (𝐴 -s ( 1s /su 𝑛)) ∧ 𝑧 = 𝐴) → 𝑦 <s 𝑧)
111	97, 99, 100, 110	syl3anb 1179	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ No ∧ 𝑦 ∈ {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))} ∧ 𝑧 ∈ {𝐴}) → 𝑦 <s 𝑧)
112	87, 88, 95, 96, 111	sltsd 28033	. . . . . . . . . 10 ⊢ (𝐴 ∈ No → {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))} <<s {𝐴})
113	69	sneqd 4596	. . . . . . . . . 10 ⊢ (𝐴 ∈ No → {(( L ‘𝐴) |s ( R ‘𝐴))} = {𝐴})
114	112, 113	breqtrrd 5133	. . . . . . . . 9 ⊢ (𝐴 ∈ No → {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))} <<s {(( L ‘𝐴) |s ( R ‘𝐴))})
115	114	adantr 486	. . . . . . . 8 ⊢ ((𝐴 ∈ No ∧ (∀𝑥𝑂 ∈ ( L ‘𝐴)∃𝑛 ∈ ℕs (𝑥𝑂 +s ( 1s /su 𝑛)) ≤s 𝐴 ∧ ∀𝑥𝑂 ∈ ( R ‘𝐴)∃𝑛 ∈ ℕs 𝐴 ≤s (𝑥𝑂 -s ( 1s /su 𝑛)))) → {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))} <<s {(( L ‘𝐴) |s ( R ‘𝐴))})
116	70	sneqd 4596	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ (∀𝑥𝑂 ∈ ( L ‘𝐴)∃𝑛 ∈ ℕs (𝑥𝑂 +s ( 1s /su 𝑛)) ≤s 𝐴 ∧ ∀𝑥𝑂 ∈ ( R ‘𝐴)∃𝑛 ∈ ℕs 𝐴 ≤s (𝑥𝑂 -s ( 1s /su 𝑛)))) → {(( L ‘𝐴) |s ( R ‘𝐴))} = {𝐴})
117	85	abrexex 7959	. . . . . . . . . . . 12 ⊢ {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))} ∈ V
118	117	a1i 11	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))} ∈ V)
119	89, 90	addscld 28245	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ No ∧ 𝑛 ∈ ℕs) → (𝐴 +s ( 1s /su 𝑛)) ∈ No )
120		eleq1 2848	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝐴 +s ( 1s /su 𝑛)) → (𝑤 ∈ No ↔ (𝐴 +s ( 1s /su 𝑛)) ∈ No ))
121	119, 120	syl5ibrcom 250	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ No ∧ 𝑛 ∈ ℕs) → (𝑤 = (𝐴 +s ( 1s /su 𝑛)) → 𝑤 ∈ No ))
122	121	rexlimdva 3163	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ No → (∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛)) → 𝑤 ∈ No ))
123	122	abssdv 4015	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))} ⊆ No )
124	98, 41	elab 3633	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))} ↔ ∃𝑛 ∈ ℕs 𝑦 = (𝐴 +s ( 1s /su 𝑛)))
125	90, 89	ltaddspos1d 28276	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ No ∧ 𝑛 ∈ ℕs) → ( 0s <s ( 1s /su 𝑛) ↔ 𝐴 <s (𝐴 +s ( 1s /su 𝑛))))
126	103, 125	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ No ∧ 𝑛 ∈ ℕs) → 𝐴 <s (𝐴 +s ( 1s /su 𝑛)))
127		breq12 5108	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 = 𝐴 ∧ 𝑦 = (𝐴 +s ( 1s /su 𝑛))) → (𝑧 <s 𝑦 ↔ 𝐴 <s (𝐴 +s ( 1s /su 𝑛))))
128	126, 127	syl5ibrcom 250	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ No ∧ 𝑛 ∈ ℕs) → ((𝑧 = 𝐴 ∧ 𝑦 = (𝐴 +s ( 1s /su 𝑛))) → 𝑧 <s 𝑦))
129	128	expcomd 422	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ No ∧ 𝑛 ∈ ℕs) → (𝑦 = (𝐴 +s ( 1s /su 𝑛)) → (𝑧 = 𝐴 → 𝑧 <s 𝑦)))
130	129	rexlimdva 3163	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ No → (∃𝑛 ∈ ℕs 𝑦 = (𝐴 +s ( 1s /su 𝑛)) → (𝑧 = 𝐴 → 𝑧 <s 𝑦)))
131	130	com23 87	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ No → (𝑧 = 𝐴 → (∃𝑛 ∈ ℕs 𝑦 = (𝐴 +s ( 1s /su 𝑛)) → 𝑧 <s 𝑦)))
132	131	3imp 1128	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ No ∧ 𝑧 = 𝐴 ∧ ∃𝑛 ∈ ℕs 𝑦 = (𝐴 +s ( 1s /su 𝑛))) → 𝑧 <s 𝑦)
133	97, 100, 124, 132	syl3anb 1179	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ No ∧ 𝑧 ∈ {𝐴} ∧ 𝑦 ∈ {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))}) → 𝑧 <s 𝑦)
134	88, 118, 96, 123, 133	sltsd 28033	. . . . . . . . . 10 ⊢ (𝐴 ∈ No → {𝐴} <<s {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))})
135	134	adantr 486	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ (∀𝑥𝑂 ∈ ( L ‘𝐴)∃𝑛 ∈ ℕs (𝑥𝑂 +s ( 1s /su 𝑛)) ≤s 𝐴 ∧ ∀𝑥𝑂 ∈ ( R ‘𝐴)∃𝑛 ∈ ℕs 𝐴 ≤s (𝑥𝑂 -s ( 1s /su 𝑛)))) → {𝐴} <<s {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))})
136	116, 135	eqbrtrd 5127	. . . . . . . 8 ⊢ ((𝐴 ∈ No ∧ (∀𝑥𝑂 ∈ ( L ‘𝐴)∃𝑛 ∈ ℕs (𝑥𝑂 +s ( 1s /su 𝑛)) ≤s 𝐴 ∧ ∀𝑥𝑂 ∈ ( R ‘𝐴)∃𝑛 ∈ ℕs 𝐴 ≤s (𝑥𝑂 -s ( 1s /su 𝑛)))) → {(( L ‘𝐴) |s ( R ‘𝐴))} <<s {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))})
137	72, 78, 84, 115, 136	cofcut1d 28186	. . . . . . 7 ⊢ ((𝐴 ∈ No ∧ (∀𝑥𝑂 ∈ ( L ‘𝐴)∃𝑛 ∈ ℕs (𝑥𝑂 +s ( 1s /su 𝑛)) ≤s 𝐴 ∧ ∀𝑥𝑂 ∈ ( R ‘𝐴)∃𝑛 ∈ ℕs 𝐴 ≤s (𝑥𝑂 -s ( 1s /su 𝑛)))) → (( L ‘𝐴) |s ( R ‘𝐴)) = ({𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))} |s {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))}))
138	70, 137	eqtr3d 2797	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ (∀𝑥𝑂 ∈ ( L ‘𝐴)∃𝑛 ∈ ℕs (𝑥𝑂 +s ( 1s /su 𝑛)) ≤s 𝐴 ∧ ∀𝑥𝑂 ∈ ( R ‘𝐴)∃𝑛 ∈ ℕs 𝐴 ≤s (𝑥𝑂 -s ( 1s /su 𝑛)))) → 𝐴 = ({𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))} |s {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))}))
139	68, 138	impbida 813	. . . . 5 ⊢ (𝐴 ∈ No → (𝐴 = ({𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))} |s {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))}) ↔ (∀𝑥𝑂 ∈ ( L ‘𝐴)∃𝑛 ∈ ℕs (𝑥𝑂 +s ( 1s /su 𝑛)) ≤s 𝐴 ∧ ∀𝑥𝑂 ∈ ( R ‘𝐴)∃𝑛 ∈ ℕs 𝐴 ≤s (𝑥𝑂 -s ( 1s /su 𝑛)))))
140		ralunb 4143	. . . . . 6 ⊢ (∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∃𝑛 ∈ ℕs ( 1s /su 𝑛) ≤s (abss‘(𝐴 -s 𝑥𝑂)) ↔ (∀𝑥𝑂 ∈ ( L ‘𝐴)∃𝑛 ∈ ℕs ( 1s /su 𝑛) ≤s (abss‘(𝐴 -s 𝑥𝑂)) ∧ ∀𝑥𝑂 ∈ ( R ‘𝐴)∃𝑛 ∈ ℕs ( 1s /su 𝑛) ≤s (abss‘(𝐴 -s 𝑥𝑂))))
141		simpl 488	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( L ‘𝐴)) → 𝐴 ∈ No )
142	141, 19	subscld 28328	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( L ‘𝐴)) → (𝐴 -s 𝑥𝑂) ∈ No )
143		0no 28074	. . . . . . . . . . . . . . 15 ⊢ 0s ∈ No
144	143	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( L ‘𝐴)) → 0s ∈ No )
145		leftlt 28118	. . . . . . . . . . . . . . . 16 ⊢ (𝑥𝑂 ∈ ( L ‘𝐴) → 𝑥𝑂 <s 𝐴)
146	145	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( L ‘𝐴)) → 𝑥𝑂 <s 𝐴)
147	19, 141	posdifsd 28363	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( L ‘𝐴)) → (𝑥𝑂 <s 𝐴 ↔ 0s <s (𝐴 -s 𝑥𝑂)))
148	146, 147	mpbid 235	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( L ‘𝐴)) → 0s <s (𝐴 -s 𝑥𝑂))
149	144, 142, 148	ltlesd 28009	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( L ‘𝐴)) → 0s ≤s (𝐴 -s 𝑥𝑂))
150		abssid 28506	. . . . . . . . . . . . 13 ⊢ (((𝐴 -s 𝑥𝑂) ∈ No ∧ 0s ≤s (𝐴 -s 𝑥𝑂)) → (abss‘(𝐴 -s 𝑥𝑂)) = (𝐴 -s 𝑥𝑂))
151	142, 149, 150	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( L ‘𝐴)) → (abss‘(𝐴 -s 𝑥𝑂)) = (𝐴 -s 𝑥𝑂))
152	151	breq2d 5115	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( L ‘𝐴)) → (( 1s /su 𝑛) ≤s (abss‘(𝐴 -s 𝑥𝑂)) ↔ ( 1s /su 𝑛) ≤s (𝐴 -s 𝑥𝑂)))
153	152	adantr 486	. . . . . . . . . 10 ⊢ (((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( L ‘𝐴)) ∧ 𝑛 ∈ ℕs) → (( 1s /su 𝑛) ≤s (abss‘(𝐴 -s 𝑥𝑂)) ↔ ( 1s /su 𝑛) ≤s (𝐴 -s 𝑥𝑂)))
154	142	adantr 486	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( L ‘𝐴)) ∧ 𝑛 ∈ ℕs) → (𝐴 -s 𝑥𝑂) ∈ No )
155	27, 154, 20	leadds2d 28261	. . . . . . . . . 10 ⊢ (((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( L ‘𝐴)) ∧ 𝑛 ∈ ℕs) → (( 1s /su 𝑛) ≤s (𝐴 -s 𝑥𝑂) ↔ (𝑥𝑂 +s ( 1s /su 𝑛)) ≤s (𝑥𝑂 +s (𝐴 -s 𝑥𝑂))))
156		pncan3s 28338	. . . . . . . . . . . . 13 ⊢ ((𝑥𝑂 ∈ No ∧ 𝐴 ∈ No ) → (𝑥𝑂 +s (𝐴 -s 𝑥𝑂)) = 𝐴)
157	19, 141, 156	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( L ‘𝐴)) → (𝑥𝑂 +s (𝐴 -s 𝑥𝑂)) = 𝐴)
158	157	adantr 486	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( L ‘𝐴)) ∧ 𝑛 ∈ ℕs) → (𝑥𝑂 +s (𝐴 -s 𝑥𝑂)) = 𝐴)
159	158	breq2d 5115	. . . . . . . . . 10 ⊢ (((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( L ‘𝐴)) ∧ 𝑛 ∈ ℕs) → ((𝑥𝑂 +s ( 1s /su 𝑛)) ≤s (𝑥𝑂 +s (𝐴 -s 𝑥𝑂)) ↔ (𝑥𝑂 +s ( 1s /su 𝑛)) ≤s 𝐴))
160	153, 155, 159	3bitrd 308	. . . . . . . . 9 ⊢ (((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( L ‘𝐴)) ∧ 𝑛 ∈ ℕs) → (( 1s /su 𝑛) ≤s (abss‘(𝐴 -s 𝑥𝑂)) ↔ (𝑥𝑂 +s ( 1s /su 𝑛)) ≤s 𝐴))
161	160	rexbidva 3184	. . . . . . . 8 ⊢ ((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( L ‘𝐴)) → (∃𝑛 ∈ ℕs ( 1s /su 𝑛) ≤s (abss‘(𝐴 -s 𝑥𝑂)) ↔ ∃𝑛 ∈ ℕs (𝑥𝑂 +s ( 1s /su 𝑛)) ≤s 𝐴))
162	161	ralbidva 3183	. . . . . . 7 ⊢ (𝐴 ∈ No → (∀𝑥𝑂 ∈ ( L ‘𝐴)∃𝑛 ∈ ℕs ( 1s /su 𝑛) ≤s (abss‘(𝐴 -s 𝑥𝑂)) ↔ ∀𝑥𝑂 ∈ ( L ‘𝐴)∃𝑛 ∈ ℕs (𝑥𝑂 +s ( 1s /su 𝑛)) ≤s 𝐴))
163		abssubs 28515	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ No ∧ 𝑥𝑂 ∈ No ) → (abss‘(𝐴 -s 𝑥𝑂)) = (abss‘(𝑥𝑂 -s 𝐴)))
164	53, 163	sylan2 605	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( R ‘𝐴)) → (abss‘(𝐴 -s 𝑥𝑂)) = (abss‘(𝑥𝑂 -s 𝐴)))
165	164	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( R ‘𝐴)) ∧ 𝑛 ∈ ℕs) → (abss‘(𝐴 -s 𝑥𝑂)) = (abss‘(𝑥𝑂 -s 𝐴)))
166		simpl 488	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( R ‘𝐴)) → 𝐴 ∈ No )
167	54, 166	subscld 28328	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( R ‘𝐴)) → (𝑥𝑂 -s 𝐴) ∈ No )
168	143	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( R ‘𝐴)) → 0s ∈ No )
169		rightgt 28119	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥𝑂 ∈ ( R ‘𝐴) → 𝐴 <s 𝑥𝑂)
170	169	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( R ‘𝐴)) → 𝐴 <s 𝑥𝑂)
171	166, 54	posdifsd 28363	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( R ‘𝐴)) → (𝐴 <s 𝑥𝑂 ↔ 0s <s (𝑥𝑂 -s 𝐴)))
172	170, 171	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( R ‘𝐴)) → 0s <s (𝑥𝑂 -s 𝐴))
173	168, 167, 172	ltlesd 28009	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( R ‘𝐴)) → 0s ≤s (𝑥𝑂 -s 𝐴))
174		abssid 28506	. . . . . . . . . . . . . 14 ⊢ (((𝑥𝑂 -s 𝐴) ∈ No ∧ 0s ≤s (𝑥𝑂 -s 𝐴)) → (abss‘(𝑥𝑂 -s 𝐴)) = (𝑥𝑂 -s 𝐴))
175	167, 173, 174	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( R ‘𝐴)) → (abss‘(𝑥𝑂 -s 𝐴)) = (𝑥𝑂 -s 𝐴))
176	175	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( R ‘𝐴)) ∧ 𝑛 ∈ ℕs) → (abss‘(𝑥𝑂 -s 𝐴)) = (𝑥𝑂 -s 𝐴))
177	165, 176	eqtrd 2795	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( R ‘𝐴)) ∧ 𝑛 ∈ ℕs) → (abss‘(𝐴 -s 𝑥𝑂)) = (𝑥𝑂 -s 𝐴))
178	177	breq2d 5115	. . . . . . . . . 10 ⊢ (((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( R ‘𝐴)) ∧ 𝑛 ∈ ℕs) → (( 1s /su 𝑛) ≤s (abss‘(𝐴 -s 𝑥𝑂)) ↔ ( 1s /su 𝑛) ≤s (𝑥𝑂 -s 𝐴)))
179	56, 55, 52	lesubsd 28361	. . . . . . . . . 10 ⊢ (((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( R ‘𝐴)) ∧ 𝑛 ∈ ℕs) → (( 1s /su 𝑛) ≤s (𝑥𝑂 -s 𝐴) ↔ 𝐴 ≤s (𝑥𝑂 -s ( 1s /su 𝑛))))
180	178, 179	bitrd 282	. . . . . . . . 9 ⊢ (((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( R ‘𝐴)) ∧ 𝑛 ∈ ℕs) → (( 1s /su 𝑛) ≤s (abss‘(𝐴 -s 𝑥𝑂)) ↔ 𝐴 ≤s (𝑥𝑂 -s ( 1s /su 𝑛))))
181	180	rexbidva 3184	. . . . . . . 8 ⊢ ((𝐴 ∈ No ∧ 𝑥𝑂 ∈ ( R ‘𝐴)) → (∃𝑛 ∈ ℕs ( 1s /su 𝑛) ≤s (abss‘(𝐴 -s 𝑥𝑂)) ↔ ∃𝑛 ∈ ℕs 𝐴 ≤s (𝑥𝑂 -s ( 1s /su 𝑛))))
182	181	ralbidva 3183	. . . . . . 7 ⊢ (𝐴 ∈ No → (∀𝑥𝑂 ∈ ( R ‘𝐴)∃𝑛 ∈ ℕs ( 1s /su 𝑛) ≤s (abss‘(𝐴 -s 𝑥𝑂)) ↔ ∀𝑥𝑂 ∈ ( R ‘𝐴)∃𝑛 ∈ ℕs 𝐴 ≤s (𝑥𝑂 -s ( 1s /su 𝑛))))
183	162, 182	anbi12d 644	. . . . . 6 ⊢ (𝐴 ∈ No → ((∀𝑥𝑂 ∈ ( L ‘𝐴)∃𝑛 ∈ ℕs ( 1s /su 𝑛) ≤s (abss‘(𝐴 -s 𝑥𝑂)) ∧ ∀𝑥𝑂 ∈ ( R ‘𝐴)∃𝑛 ∈ ℕs ( 1s /su 𝑛) ≤s (abss‘(𝐴 -s 𝑥𝑂))) ↔ (∀𝑥𝑂 ∈ ( L ‘𝐴)∃𝑛 ∈ ℕs (𝑥𝑂 +s ( 1s /su 𝑛)) ≤s 𝐴 ∧ ∀𝑥𝑂 ∈ ( R ‘𝐴)∃𝑛 ∈ ℕs 𝐴 ≤s (𝑥𝑂 -s ( 1s /su 𝑛)))))
184	140, 183	bitrid 286	. . . . 5 ⊢ (𝐴 ∈ No → (∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∃𝑛 ∈ ℕs ( 1s /su 𝑛) ≤s (abss‘(𝐴 -s 𝑥𝑂)) ↔ (∀𝑥𝑂 ∈ ( L ‘𝐴)∃𝑛 ∈ ℕs (𝑥𝑂 +s ( 1s /su 𝑛)) ≤s 𝐴 ∧ ∀𝑥𝑂 ∈ ( R ‘𝐴)∃𝑛 ∈ ℕs 𝐴 ≤s (𝑥𝑂 -s ( 1s /su 𝑛)))))
185	139, 184	bitr4d 285	. . . 4 ⊢ (𝐴 ∈ No → (𝐴 = ({𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))} |s {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))}) ↔ ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∃𝑛 ∈ ℕs ( 1s /su 𝑛) ≤s (abss‘(𝐴 -s 𝑥𝑂))))
186	185	anbi2d 642	. . 3 ⊢ (𝐴 ∈ No → ((∃𝑛 ∈ ℕs (( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ 𝐴 = ({𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))} |s {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))})) ↔ (∃𝑛 ∈ ℕs (( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∃𝑛 ∈ ℕs ( 1s /su 𝑛) ≤s (abss‘(𝐴 -s 𝑥𝑂)))))
187	186	pm5.32i 585	. 2 ⊢ ((𝐴 ∈ No ∧ (∃𝑛 ∈ ℕs (( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ 𝐴 = ({𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 -s ( 1s /su 𝑛))} |s {𝑤 ∣ ∃𝑛 ∈ ℕs 𝑤 = (𝐴 +s ( 1s /su 𝑛))}))) ↔ (𝐴 ∈ No ∧ (∃𝑛 ∈ ℕs (( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∃𝑛 ∈ ℕs ( 1s /su 𝑛) ≤s (abss‘(𝐴 -s 𝑥𝑂)))))
188	1, 187	bitri 278	1 ⊢ (𝐴 ∈ ℝs ↔ (𝐴 ∈ No ∧ (∃𝑛 ∈ ℕs (( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))∃𝑛 ∈ ℕs ( 1s /su 𝑛) ≤s (abss‘(𝐴 -s 𝑥𝑂)))))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2145  {cab 2738  ∀wral 3076  ∃wrex 3086  Vcvv 3450   ∪ cun 3897  {csn 4584   class class class wbr 5103  ‘cfv 6533  (class class class)co 7413   No csur 27876   <s clts 27877   ≤s cles 27980   <<s cslts 28022   |s ccuts 28024   0_s c0s 28070   1_s c1s 28071   L cleft 28090   R cright 28091   +_s cadds 28224   -u_s cnegs 28284   -_s csubs 28285   /_su cdivs 28452  abs_scabss 28502  ℕ_scnns 28578  ℝ_screno 28754

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7736  ax-inf2 9620  ax-dc 10448

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-ot 4593  df-uni 4868  df-int 4908  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-se 5609  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7863  df-1st 7986  df-2nd 7987  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-1o 8455  df-2o 8456  df-oadd 8459  df-nadd 8654  df-no 27879  df-lts 27880  df-bday 27881  df-les 27981  df-slts 28023  df-cuts 28025  df-0s 28072  df-1s 28073  df-made 28092  df-old 28093  df-left 28095  df-right 28096  df-norec 28203  df-norec2 28214  df-adds 28225  df-negs 28286  df-subs 28287  df-muls 28372  df-divs 28453  df-abss 28503  df-n0s 28579  df-nns 28580  df-reno 28755

This theorem is used by:  0reno  28761  1reno  28762