Theorem supaddc 11595

Description: The supremum function distributes over addition in a sense similar to that in supmul1 11597. (Contributed by Brendan Leahy, 25-Sep-2017.)

Hypotheses

Ref	Expression
supadd.a1	⊢ (𝜑 → 𝐴 ⊆ ℝ)
supadd.a2	⊢ (𝜑 → 𝐴 ≠ ∅)
supadd.a3	⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)
supaddc.b	⊢ (𝜑 → 𝐵 ∈ ℝ)
supaddc.c	⊢ 𝐶 = {𝑧 ∣ ∃𝑣 ∈ 𝐴 𝑧 = (𝑣 + 𝐵)}

Assertion

Ref	Expression
supaddc	⊢ (𝜑 → (sup(𝐴, ℝ, < ) + 𝐵) = sup(𝐶, ℝ, < ))

Distinct variable groups:   𝑥,𝑦,𝑧,𝑣,𝐴   𝑥,𝐵,𝑦,𝑧,𝑣   𝑥,𝐶   𝜑,𝑧,𝑣

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐶(𝑦,𝑧,𝑣)

Proof of Theorem supaddc

Dummy variables 𝑤 𝑎 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3444	. . . . . . 7 ⊢ 𝑤 ∈ V
2		oveq1 7142	. . . . . . . . . 10 ⊢ (𝑣 = 𝑎 → (𝑣 + 𝐵) = (𝑎 + 𝐵))
3	2	eqeq2d 2809	. . . . . . . . 9 ⊢ (𝑣 = 𝑎 → (𝑧 = (𝑣 + 𝐵) ↔ 𝑧 = (𝑎 + 𝐵)))
4	3	cbvrexvw 3397	. . . . . . . 8 ⊢ (∃𝑣 ∈ 𝐴 𝑧 = (𝑣 + 𝐵) ↔ ∃𝑎 ∈ 𝐴 𝑧 = (𝑎 + 𝐵))
5		eqeq1 2802	. . . . . . . . 9 ⊢ (𝑧 = 𝑤 → (𝑧 = (𝑎 + 𝐵) ↔ 𝑤 = (𝑎 + 𝐵)))
6	5	rexbidv 3256	. . . . . . . 8 ⊢ (𝑧 = 𝑤 → (∃𝑎 ∈ 𝐴 𝑧 = (𝑎 + 𝐵) ↔ ∃𝑎 ∈ 𝐴 𝑤 = (𝑎 + 𝐵)))
7	4, 6	syl5bb 286	. . . . . . 7 ⊢ (𝑧 = 𝑤 → (∃𝑣 ∈ 𝐴 𝑧 = (𝑣 + 𝐵) ↔ ∃𝑎 ∈ 𝐴 𝑤 = (𝑎 + 𝐵)))
8		supaddc.c	. . . . . . 7 ⊢ 𝐶 = {𝑧 ∣ ∃𝑣 ∈ 𝐴 𝑧 = (𝑣 + 𝐵)}
9	1, 7, 8	elab2 3618	. . . . . 6 ⊢ (𝑤 ∈ 𝐶 ↔ ∃𝑎 ∈ 𝐴 𝑤 = (𝑎 + 𝐵))
10		supadd.a1	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
11	10	sselda 3915	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ ℝ)
12		supadd.a2	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ≠ ∅)
13		supadd.a3	. . . . . . . . . . 11 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)
14	10, 12, 13	suprcld 11591	. . . . . . . . . 10 ⊢ (𝜑 → sup(𝐴, ℝ, < ) ∈ ℝ)
15	14	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → sup(𝐴, ℝ, < ) ∈ ℝ)
16		supaddc.b	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ ℝ)
17	16	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝐵 ∈ ℝ)
18	10, 12, 13	3jca 1125	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥))
19		suprub 11589	. . . . . . . . . 10 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝑎 ∈ 𝐴) → 𝑎 ≤ sup(𝐴, ℝ, < ))
20	18, 19	sylan 583	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑎 ≤ sup(𝐴, ℝ, < ))
21	11, 15, 17, 20	leadd1dd 11243	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑎 + 𝐵) ≤ (sup(𝐴, ℝ, < ) + 𝐵))
22		breq1 5033	. . . . . . . 8 ⊢ (𝑤 = (𝑎 + 𝐵) → (𝑤 ≤ (sup(𝐴, ℝ, < ) + 𝐵) ↔ (𝑎 + 𝐵) ≤ (sup(𝐴, ℝ, < ) + 𝐵)))
23	21, 22	syl5ibrcom 250	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑤 = (𝑎 + 𝐵) → 𝑤 ≤ (sup(𝐴, ℝ, < ) + 𝐵)))
24	23	rexlimdva 3243	. . . . . 6 ⊢ (𝜑 → (∃𝑎 ∈ 𝐴 𝑤 = (𝑎 + 𝐵) → 𝑤 ≤ (sup(𝐴, ℝ, < ) + 𝐵)))
25	9, 24	syl5bi 245	. . . . 5 ⊢ (𝜑 → (𝑤 ∈ 𝐶 → 𝑤 ≤ (sup(𝐴, ℝ, < ) + 𝐵)))
26	25	ralrimiv 3148	. . . 4 ⊢ (𝜑 → ∀𝑤 ∈ 𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) + 𝐵))
27	11, 17	readdcld 10659	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑎 + 𝐵) ∈ ℝ)
28		eleq1a 2885	. . . . . . . . 9 ⊢ ((𝑎 + 𝐵) ∈ ℝ → (𝑤 = (𝑎 + 𝐵) → 𝑤 ∈ ℝ))
29	27, 28	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑤 = (𝑎 + 𝐵) → 𝑤 ∈ ℝ))
30	29	rexlimdva 3243	. . . . . . 7 ⊢ (𝜑 → (∃𝑎 ∈ 𝐴 𝑤 = (𝑎 + 𝐵) → 𝑤 ∈ ℝ))
31	9, 30	syl5bi 245	. . . . . 6 ⊢ (𝜑 → (𝑤 ∈ 𝐶 → 𝑤 ∈ ℝ))
32	31	ssrdv 3921	. . . . 5 ⊢ (𝜑 → 𝐶 ⊆ ℝ)
33		ovex 7168	. . . . . . . . 9 ⊢ (𝑎 + 𝐵) ∈ V
34	33	isseti 3455	. . . . . . . 8 ⊢ ∃𝑤 𝑤 = (𝑎 + 𝐵)
35	34	rgenw 3118	. . . . . . 7 ⊢ ∀𝑎 ∈ 𝐴 ∃𝑤 𝑤 = (𝑎 + 𝐵)
36		r19.2z 4398	. . . . . . 7 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑎 ∈ 𝐴 ∃𝑤 𝑤 = (𝑎 + 𝐵)) → ∃𝑎 ∈ 𝐴 ∃𝑤 𝑤 = (𝑎 + 𝐵))
37	12, 35, 36	sylancl 589	. . . . . 6 ⊢ (𝜑 → ∃𝑎 ∈ 𝐴 ∃𝑤 𝑤 = (𝑎 + 𝐵))
38	9	exbii 1849	. . . . . . 7 ⊢ (∃𝑤 𝑤 ∈ 𝐶 ↔ ∃𝑤∃𝑎 ∈ 𝐴 𝑤 = (𝑎 + 𝐵))
39		n0 4260	. . . . . . 7 ⊢ (𝐶 ≠ ∅ ↔ ∃𝑤 𝑤 ∈ 𝐶)
40		rexcom4 3212	. . . . . . 7 ⊢ (∃𝑎 ∈ 𝐴 ∃𝑤 𝑤 = (𝑎 + 𝐵) ↔ ∃𝑤∃𝑎 ∈ 𝐴 𝑤 = (𝑎 + 𝐵))
41	38, 39, 40	3bitr4i 306	. . . . . 6 ⊢ (𝐶 ≠ ∅ ↔ ∃𝑎 ∈ 𝐴 ∃𝑤 𝑤 = (𝑎 + 𝐵))
42	37, 41	sylibr 237	. . . . 5 ⊢ (𝜑 → 𝐶 ≠ ∅)
43	14, 16	readdcld 10659	. . . . . 6 ⊢ (𝜑 → (sup(𝐴, ℝ, < ) + 𝐵) ∈ ℝ)
44		brralrspcev 5090	. . . . . 6 ⊢ (((sup(𝐴, ℝ, < ) + 𝐵) ∈ ℝ ∧ ∀𝑤 ∈ 𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) + 𝐵)) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝐶 𝑤 ≤ 𝑥)
45	43, 26, 44	syl2anc 587	. . . . 5 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝐶 𝑤 ≤ 𝑥)
46		suprleub 11594	. . . . 5 ⊢ (((𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝐶 𝑤 ≤ 𝑥) ∧ (sup(𝐴, ℝ, < ) + 𝐵) ∈ ℝ) → (sup(𝐶, ℝ, < ) ≤ (sup(𝐴, ℝ, < ) + 𝐵) ↔ ∀𝑤 ∈ 𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) + 𝐵)))
47	32, 42, 45, 43, 46	syl31anc 1370	. . . 4 ⊢ (𝜑 → (sup(𝐶, ℝ, < ) ≤ (sup(𝐴, ℝ, < ) + 𝐵) ↔ ∀𝑤 ∈ 𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) + 𝐵)))
48	26, 47	mpbird 260	. . 3 ⊢ (𝜑 → sup(𝐶, ℝ, < ) ≤ (sup(𝐴, ℝ, < ) + 𝐵))
49	32, 42, 45	suprcld 11591	. . . . . . 7 ⊢ (𝜑 → sup(𝐶, ℝ, < ) ∈ ℝ)
50	49, 16, 14	ltsubaddd 11225	. . . . . 6 ⊢ (𝜑 → ((sup(𝐶, ℝ, < ) − 𝐵) < sup(𝐴, ℝ, < ) ↔ sup(𝐶, ℝ, < ) < (sup(𝐴, ℝ, < ) + 𝐵)))
51	50	biimpar 481	. . . . 5 ⊢ ((𝜑 ∧ sup(𝐶, ℝ, < ) < (sup(𝐴, ℝ, < ) + 𝐵)) → (sup(𝐶, ℝ, < ) − 𝐵) < sup(𝐴, ℝ, < ))
52	49, 16	resubcld 11057	. . . . . . 7 ⊢ (𝜑 → (sup(𝐶, ℝ, < ) − 𝐵) ∈ ℝ)
53		suprlub 11592	. . . . . . 7 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ (sup(𝐶, ℝ, < ) − 𝐵) ∈ ℝ) → ((sup(𝐶, ℝ, < ) − 𝐵) < sup(𝐴, ℝ, < ) ↔ ∃𝑎 ∈ 𝐴 (sup(𝐶, ℝ, < ) − 𝐵) < 𝑎))
54	10, 12, 13, 52, 53	syl31anc 1370	. . . . . 6 ⊢ (𝜑 → ((sup(𝐶, ℝ, < ) − 𝐵) < sup(𝐴, ℝ, < ) ↔ ∃𝑎 ∈ 𝐴 (sup(𝐶, ℝ, < ) − 𝐵) < 𝑎))
55	54	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ sup(𝐶, ℝ, < ) < (sup(𝐴, ℝ, < ) + 𝐵)) → ((sup(𝐶, ℝ, < ) − 𝐵) < sup(𝐴, ℝ, < ) ↔ ∃𝑎 ∈ 𝐴 (sup(𝐶, ℝ, < ) − 𝐵) < 𝑎))
56	51, 55	mpbid 235	. . . 4 ⊢ ((𝜑 ∧ sup(𝐶, ℝ, < ) < (sup(𝐴, ℝ, < ) + 𝐵)) → ∃𝑎 ∈ 𝐴 (sup(𝐶, ℝ, < ) − 𝐵) < 𝑎)
57	27	adantlr 714	. . . . . . 7 ⊢ (((𝜑 ∧ sup(𝐶, ℝ, < ) < (sup(𝐴, ℝ, < ) + 𝐵)) ∧ 𝑎 ∈ 𝐴) → (𝑎 + 𝐵) ∈ ℝ)
58	49	ad2antrr 725	. . . . . . 7 ⊢ (((𝜑 ∧ sup(𝐶, ℝ, < ) < (sup(𝐴, ℝ, < ) + 𝐵)) ∧ 𝑎 ∈ 𝐴) → sup(𝐶, ℝ, < ) ∈ ℝ)
59		rspe 3263	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑤 = (𝑎 + 𝐵)) → ∃𝑎 ∈ 𝐴 𝑤 = (𝑎 + 𝐵))
60	59, 9	sylibr 237	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑤 = (𝑎 + 𝐵)) → 𝑤 ∈ 𝐶)
61	60	adantl 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑤 = (𝑎 + 𝐵))) → 𝑤 ∈ 𝐶)
62		simplrr 777	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑤 = (𝑎 + 𝐵))) ∧ 𝑤 ∈ 𝐶) → 𝑤 = (𝑎 + 𝐵))
63	32, 42, 45	3jca 1125	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝐶 𝑤 ≤ 𝑥))
64		suprub 11589	. . . . . . . . . . . . . . 15 ⊢ (((𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝐶 𝑤 ≤ 𝑥) ∧ 𝑤 ∈ 𝐶) → 𝑤 ≤ sup(𝐶, ℝ, < ))
65	63, 64	sylan 583	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐶) → 𝑤 ≤ sup(𝐶, ℝ, < ))
66	65	adantlr 714	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑤 = (𝑎 + 𝐵))) ∧ 𝑤 ∈ 𝐶) → 𝑤 ≤ sup(𝐶, ℝ, < ))
67	62, 66	eqbrtrrd 5054	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑤 = (𝑎 + 𝐵))) ∧ 𝑤 ∈ 𝐶) → (𝑎 + 𝐵) ≤ sup(𝐶, ℝ, < ))
68	61, 67	mpdan 686	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑤 = (𝑎 + 𝐵))) → (𝑎 + 𝐵) ≤ sup(𝐶, ℝ, < ))
69	68	expr 460	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑤 = (𝑎 + 𝐵) → (𝑎 + 𝐵) ≤ sup(𝐶, ℝ, < )))
70	69	exlimdv 1934	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (∃𝑤 𝑤 = (𝑎 + 𝐵) → (𝑎 + 𝐵) ≤ sup(𝐶, ℝ, < )))
71	34, 70	mpi 20	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑎 + 𝐵) ≤ sup(𝐶, ℝ, < ))
72	71	adantlr 714	. . . . . . 7 ⊢ (((𝜑 ∧ sup(𝐶, ℝ, < ) < (sup(𝐴, ℝ, < ) + 𝐵)) ∧ 𝑎 ∈ 𝐴) → (𝑎 + 𝐵) ≤ sup(𝐶, ℝ, < ))
73	57, 58, 72	lensymd 10780	. . . . . 6 ⊢ (((𝜑 ∧ sup(𝐶, ℝ, < ) < (sup(𝐴, ℝ, < ) + 𝐵)) ∧ 𝑎 ∈ 𝐴) → ¬ sup(𝐶, ℝ, < ) < (𝑎 + 𝐵))
74	16	ad2antrr 725	. . . . . . 7 ⊢ (((𝜑 ∧ sup(𝐶, ℝ, < ) < (sup(𝐴, ℝ, < ) + 𝐵)) ∧ 𝑎 ∈ 𝐴) → 𝐵 ∈ ℝ)
75	11	adantlr 714	. . . . . . 7 ⊢ (((𝜑 ∧ sup(𝐶, ℝ, < ) < (sup(𝐴, ℝ, < ) + 𝐵)) ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ ℝ)
76	58, 74, 75	ltsubaddd 11225	. . . . . 6 ⊢ (((𝜑 ∧ sup(𝐶, ℝ, < ) < (sup(𝐴, ℝ, < ) + 𝐵)) ∧ 𝑎 ∈ 𝐴) → ((sup(𝐶, ℝ, < ) − 𝐵) < 𝑎 ↔ sup(𝐶, ℝ, < ) < (𝑎 + 𝐵)))
77	73, 76	mtbird 328	. . . . 5 ⊢ (((𝜑 ∧ sup(𝐶, ℝ, < ) < (sup(𝐴, ℝ, < ) + 𝐵)) ∧ 𝑎 ∈ 𝐴) → ¬ (sup(𝐶, ℝ, < ) − 𝐵) < 𝑎)
78	77	nrexdv 3229	. . . 4 ⊢ ((𝜑 ∧ sup(𝐶, ℝ, < ) < (sup(𝐴, ℝ, < ) + 𝐵)) → ¬ ∃𝑎 ∈ 𝐴 (sup(𝐶, ℝ, < ) − 𝐵) < 𝑎)
79	56, 78	pm2.65da 816	. . 3 ⊢ (𝜑 → ¬ sup(𝐶, ℝ, < ) < (sup(𝐴, ℝ, < ) + 𝐵))
80	49, 43	eqleltd 10773	. . 3 ⊢ (𝜑 → (sup(𝐶, ℝ, < ) = (sup(𝐴, ℝ, < ) + 𝐵) ↔ (sup(𝐶, ℝ, < ) ≤ (sup(𝐴, ℝ, < ) + 𝐵) ∧ ¬ sup(𝐶, ℝ, < ) < (sup(𝐴, ℝ, < ) + 𝐵))))
81	48, 79, 80	mpbir2and 712	. 2 ⊢ (𝜑 → sup(𝐶, ℝ, < ) = (sup(𝐴, ℝ, < ) + 𝐵))
82	81	eqcomd 2804	1 ⊢ (𝜑 → (sup(𝐴, ℝ, < ) + 𝐵) = sup(𝐶, ℝ, < ))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2111  {cab 2776   ≠ wne 2987  ∀wral 3106  ∃wrex 3107   ⊆ wss 3881  ∅c0 4243   class class class wbr 5030  (class class class)co 7135  supcsup 8888  ℝcr 10525   + caddc 10529   < clt 10664   ≤ cle 10665   − cmin 10859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-po 5438  df-so 5439  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-er 8272  df-en 8493  df-dom 8494  df-sdom 8495  df-sup 8890  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862

This theorem is referenced by:  supadd  11596  supsubc  41985