supminfxr - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > supminfxr		Structured version Visualization version GIF version

Theorem supminfxr 45439

Description: The extended real suprema of a set of reals is the extended real negative of the extended real infima of that set's image under negation. (Contributed by Glauco Siliprandi, 2-Jan-2022.)

**Hypothesis**
Ref	Expression
supminfxr.1	⊢ (𝜑 → 𝐴 ⊆ ℝ)

**Assertion**
Ref	Expression
supminfxr	⊢ (𝜑 → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))

Distinct variable group: 𝑥,𝐴 Allowed substitution hint: 𝜑(𝑥)

Proof of Theorem supminfxr Dummy variables 𝑣 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		supeq1 9455	. . . . 5 ⊢ (𝐴 = ∅ → sup(𝐴, ℝ^, < ) = sup(∅, ℝ^, < ))
2		xrsup0 13337	. . . . . 6 ⊢ sup(∅, ℝ^*, < ) = -∞
3	2	a1i 11	. . . . 5 ⊢ (𝐴 = ∅ → sup(∅, ℝ^*, < ) = -∞)
4	1, 3	eqtrd 2770	. . . 4 ⊢ (𝐴 = ∅ → sup(𝐴, ℝ^*, < ) = -∞)
5	4	adantl 481	. . 3 ⊢ ((𝜑 ∧ 𝐴 = ∅) → sup(𝐴, ℝ^*, < ) = -∞)
6		eleq2 2823	. . . . . . . . . 10 ⊢ (𝐴 = ∅ → (-𝑥 ∈ 𝐴 ↔ -𝑥 ∈ ∅))
7	6	rabbidv 3423	. . . . . . . . 9 ⊢ (𝐴 = ∅ → {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} = {𝑥 ∈ ℝ ∣ -𝑥 ∈ ∅})
8		noel 4313	. . . . . . . . . . . . 13 ⊢ ¬ -𝑥 ∈ ∅
9	8	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → ¬ -𝑥 ∈ ∅)
10	9	rgen 3053	. . . . . . . . . . 11 ⊢ ∀𝑥 ∈ ℝ ¬ -𝑥 ∈ ∅
11		rabeq0 4363	. . . . . . . . . . 11 ⊢ ({𝑥 ∈ ℝ ∣ -𝑥 ∈ ∅} = ∅ ↔ ∀𝑥 ∈ ℝ ¬ -𝑥 ∈ ∅)
12	10, 11	mpbir 231	. . . . . . . . . 10 ⊢ {𝑥 ∈ ℝ ∣ -𝑥 ∈ ∅} = ∅
13	12	a1i 11	. . . . . . . . 9 ⊢ (𝐴 = ∅ → {𝑥 ∈ ℝ ∣ -𝑥 ∈ ∅} = ∅)
14	7, 13	eqtrd 2770	. . . . . . . 8 ⊢ (𝐴 = ∅ → {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} = ∅)
15	14	infeq1d 9488	. . . . . . 7 ⊢ (𝐴 = ∅ → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ) = inf(∅, ℝ^, < ))
16		xrinf0 13353	. . . . . . . 8 ⊢ inf(∅, ℝ^*, < ) = +∞
17	16	a1i 11	. . . . . . 7 ⊢ (𝐴 = ∅ → inf(∅, ℝ^*, < ) = +∞)
18	15, 17	eqtrd 2770	. . . . . 6 ⊢ (𝐴 = ∅ → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = +∞)
19	18	xnegeqd 45412	. . . . 5 ⊢ (𝐴 = ∅ → -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -_𝑒+∞)
20		xnegpnf 13223	. . . . . 6 ⊢ -_𝑒+∞ = -∞
21	20	a1i 11	. . . . 5 ⊢ (𝐴 = ∅ → -_𝑒+∞ = -∞)
22	19, 21	eqtrd 2770	. . . 4 ⊢ (𝐴 = ∅ → -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -∞)
23	22	adantl 481	. . 3 ⊢ ((𝜑 ∧ 𝐴 = ∅) → -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -∞)
24	5, 23	eqtr4d 2773	. 2 ⊢ ((𝜑 ∧ 𝐴 = ∅) → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))
25		neqne 2940	. . 3 ⊢ (¬ 𝐴 = ∅ → 𝐴 ≠ ∅)
26		supminfxr.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
27	26	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → 𝐴 ⊆ ℝ)
28		simplr 768	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → 𝐴 ≠ ∅)
29		simpr 484	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦)
30		negn0 11664	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) → {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ≠ ∅)
31		ublbneg 12947	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑦 ≤ 𝑧)
32		ssrab2 4055	. . . . . . . . . . 11 ⊢ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ⊆ ℝ
33		infrenegsup 12223	. . . . . . . . . . 11 ⊢ (({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ⊆ ℝ ∧ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑦 ≤ 𝑧) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) = -sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}, ℝ, < ))
34	32, 33	mp3an1 1450	. . . . . . . . . 10 ⊢ (({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑦 ≤ 𝑧) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) = -sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}, ℝ, < ))
35	30, 31, 34	syl2an 596	. . . . . . . . 9 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) = -sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}, ℝ, < ))
36	35	3impa 1109	. . . . . . . 8 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) = -sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}, ℝ, < ))
37		elrabi 3666	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}} → 𝑦 ∈ ℝ)
38	37	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}) → 𝑦 ∈ ℝ)
39		ssel2 3953	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ)
40		negeq 11472	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑦 → -𝑤 = -𝑦)
41	40	eleq1d 2819	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑦 → (-𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ↔ -𝑦 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}))
42	41	elrab3 3672	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ → (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}} ↔ -𝑦 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}))
43		renegcl 11544	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℝ → -𝑦 ∈ ℝ)
44		negeq 11472	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = -𝑦 → -𝑥 = --𝑦)
45	44	eleq1d 2819	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = -𝑦 → (-𝑥 ∈ 𝐴 ↔ --𝑦 ∈ 𝐴))
46	45	elrab3 3672	. . . . . . . . . . . . . . 15 ⊢ (-𝑦 ∈ ℝ → (-𝑦 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ↔ --𝑦 ∈ 𝐴))
47	43, 46	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ → (-𝑦 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ↔ --𝑦 ∈ 𝐴))
48		recn 11217	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
49	48	negnegd 11583	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℝ → --𝑦 = 𝑦)
50	49	eleq1d 2819	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ → (--𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
51	42, 47, 50	3bitrd 305	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℝ → (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}} ↔ 𝑦 ∈ 𝐴))
52	51	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ) → (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}} ↔ 𝑦 ∈ 𝐴))
53	38, 39, 52	eqrdav 2734	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ ℝ → {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}} = 𝐴)
54	53	supeq1d 9456	. . . . . . . . . 10 ⊢ (𝐴 ⊆ ℝ → sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}, ℝ, < ) = sup(𝐴, ℝ, < ))
55	54	3ad2ant1 1133	. . . . . . . . 9 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}, ℝ, < ) = sup(𝐴, ℝ, < ))
56	55	negeqd 11474	. . . . . . . 8 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → -sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}, ℝ, < ) = -sup(𝐴, ℝ, < ))
57	36, 56	eqtrd 2770	. . . . . . 7 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) = -sup(𝐴, ℝ, < ))
58		infrecl 12222	. . . . . . . . . . 11 ⊢ (({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ⊆ ℝ ∧ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑦 ≤ 𝑧) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℝ)
59	32, 58	mp3an1 1450	. . . . . . . . . 10 ⊢ (({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑦 ≤ 𝑧) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℝ)
60	30, 31, 59	syl2an 596	. . . . . . . . 9 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℝ)
61	60	3impa 1109	. . . . . . . 8 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℝ)
62		suprcl 12200	. . . . . . . 8 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ, < ) ∈ ℝ)
63		recn 11217	. . . . . . . . 9 ⊢ (inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℝ → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℂ)
64		recn 11217	. . . . . . . . 9 ⊢ (sup(𝐴, ℝ, < ) ∈ ℝ → sup(𝐴, ℝ, < ) ∈ ℂ)
65		negcon2 11534	. . . . . . . . 9 ⊢ ((inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℂ ∧ sup(𝐴, ℝ, < ) ∈ ℂ) → (inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) = -sup(𝐴, ℝ, < ) ↔ sup(𝐴, ℝ, < ) = -inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < )))
66	63, 64, 65	syl2an 596	. . . . . . . 8 ⊢ ((inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℝ ∧ sup(𝐴, ℝ, < ) ∈ ℝ) → (inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) = -sup(𝐴, ℝ, < ) ↔ sup(𝐴, ℝ, < ) = -inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < )))
67	61, 62, 66	syl2anc 584	. . . . . . 7 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → (inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) = -sup(𝐴, ℝ, < ) ↔ sup(𝐴, ℝ, < ) = -inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < )))
68	57, 67	mpbid 232	. . . . . 6 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ, < ) = -inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ))
69	27, 28, 29, 68	syl3anc 1373	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ, < ) = -inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ))
70		supxrre 13341	. . . . . 6 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ^*, < ) = sup(𝐴, ℝ, < ))
71	27, 28, 29, 70	syl3anc 1373	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ^*, < ) = sup(𝐴, ℝ, < ))
72	32	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ⊆ ℝ)
73	27, 28, 30	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ≠ ∅)
74	29, 31	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑦 ≤ 𝑧)
75		infxrre 13351	. . . . . . . 8 ⊢ (({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ⊆ ℝ ∧ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑦 ≤ 𝑧) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ))
76	72, 73, 74, 75	syl3anc 1373	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ))
77	76	xnegeqd 45412	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ))
78	26, 60	sylanl1 680	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℝ)
79	78	rexnegd 45115	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) = -inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ))
80	77, 79	eqtrd 2770	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ))
81	69, 71, 80	3eqtr4d 2780	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))
82		simpr 484	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦)
83		simplr 768	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → 𝑦 ∈ ℝ)
84	26	sselda 3958	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℝ)
85	84	adantlr 715	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℝ)
86	83, 85	ltnled 11380	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → (𝑦 < 𝑧 ↔ ¬ 𝑧 ≤ 𝑦))
87	86	rexbidva 3162	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ∃𝑧 ∈ 𝐴 ¬ 𝑧 ≤ 𝑦))
88		rexnal 3089	. . . . . . . . . . . 12 ⊢ (∃𝑧 ∈ 𝐴 ¬ 𝑧 ≤ 𝑦 ↔ ¬ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦)
89	88	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∃𝑧 ∈ 𝐴 ¬ 𝑧 ≤ 𝑦 ↔ ¬ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦))
90	87, 89	bitrd 279	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ¬ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦))
91	90	ralbidva 3161	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ∀𝑦 ∈ ℝ ¬ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦))
92		ralnex 3062	. . . . . . . . . 10 ⊢ (∀𝑦 ∈ ℝ ¬ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ↔ ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦)
93	92	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑦 ∈ ℝ ¬ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ↔ ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦))
94	91, 93	bitrd 279	. . . . . . . 8 ⊢ (𝜑 → (∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦))
95	94	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → (∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦))
96	82, 95	mpbird 257	. . . . . 6 ⊢ ((𝜑 ∧ ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)
97		xnegmnf 13224	. . . . . . . . 9 ⊢ -_𝑒-∞ = +∞
98	97	eqcomi 2744	. . . . . . . 8 ⊢ +∞ = -_𝑒-∞
99	98	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → +∞ = -_𝑒-∞)
100		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)
101		ressxr 11277	. . . . . . . . . . . 12 ⊢ ℝ ⊆ ℝ^*
102	101	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → ℝ ⊆ ℝ^*)
103	26, 102	sstrd 3969	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ⊆ ℝ^*)
104		supxrunb2 13334	. . . . . . . . . 10 ⊢ (𝐴 ⊆ ℝ^* → (∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ sup(𝐴, ℝ^*, < ) = +∞))
105	103, 104	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ sup(𝐴, ℝ^*, < ) = +∞))
106	105	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → (∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ sup(𝐴, ℝ^*, < ) = +∞))
107	100, 106	mpbid 232	. . . . . . 7 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → sup(𝐴, ℝ^*, < ) = +∞)
108		renegcl 11544	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ ℝ → -𝑣 ∈ ℝ)
109	108	adantl 481	. . . . . . . . . . . . 13 ⊢ ((∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ∧ 𝑣 ∈ ℝ) → -𝑣 ∈ ℝ)
110		simpl 482	. . . . . . . . . . . . 13 ⊢ ((∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ∧ 𝑣 ∈ ℝ) → ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)
111		breq1 5122	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = -𝑣 → (𝑦 < 𝑧 ↔ -𝑣 < 𝑧))
112	111	rexbidv 3164	. . . . . . . . . . . . . 14 ⊢ (𝑦 = -𝑣 → (∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ∃𝑧 ∈ 𝐴 -𝑣 < 𝑧))
113	112	rspcva 3599	. . . . . . . . . . . . 13 ⊢ ((-𝑣 ∈ ℝ ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → ∃𝑧 ∈ 𝐴 -𝑣 < 𝑧)
114	109, 110, 113	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ∧ 𝑣 ∈ ℝ) → ∃𝑧 ∈ 𝐴 -𝑣 < 𝑧)
115	114	adantll 714	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) ∧ 𝑣 ∈ ℝ) → ∃𝑧 ∈ 𝐴 -𝑣 < 𝑧)
116		negeq 11472	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = -𝑧 → -𝑥 = --𝑧)
117	116	eleq1d 2819	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = -𝑧 → (-𝑥 ∈ 𝐴 ↔ --𝑧 ∈ 𝐴))
118	84	renegcld 11662	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → -𝑧 ∈ ℝ)
119	118	ad4ant13 751	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → -𝑧 ∈ ℝ)
120	84	recnd 11261	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℂ)
121	120	negnegd 11583	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → --𝑧 = 𝑧)
122		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴)
123	121, 122	eqeltrd 2834	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → --𝑧 ∈ 𝐴)
124	123	ad4ant13 751	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → --𝑧 ∈ 𝐴)
125	117, 119, 124	elrabd 3673	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → -𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴})
126		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → -𝑣 < 𝑧)
127	108	ad3antlr 731	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → -𝑣 ∈ ℝ)
128	84	ad4ant13 751	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → 𝑧 ∈ ℝ)
129	127, 128	ltnegd 11813	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → (-𝑣 < 𝑧 ↔ -𝑧 < --𝑣))
130	126, 129	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → -𝑧 < --𝑣)
131		simpllr 775	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → 𝑣 ∈ ℝ)
132		recn 11217	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ ℝ → 𝑣 ∈ ℂ)
133		negneg 11531	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ ℂ → --𝑣 = 𝑣)
134	131, 132, 133	3syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → --𝑣 = 𝑣)
135	130, 134	breqtrd 5145	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → -𝑧 < 𝑣)
136		breq1 5122	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = -𝑧 → (𝑤 < 𝑣 ↔ -𝑧 < 𝑣))
137	136	rspcev 3601	. . . . . . . . . . . . . 14 ⊢ ((-𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ∧ -𝑧 < 𝑣) → ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣)
138	125, 135, 137	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣)
139	138	rexlimdva2 3143	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑣 ∈ ℝ) → (∃𝑧 ∈ 𝐴 -𝑣 < 𝑧 → ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣))
140	139	adantlr 715	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) ∧ 𝑣 ∈ ℝ) → (∃𝑧 ∈ 𝐴 -𝑣 < 𝑧 → ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣))
141	115, 140	mpd 15	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) ∧ 𝑣 ∈ ℝ) → ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣)
142	141	ralrimiva 3132	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → ∀𝑣 ∈ ℝ ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣)
143	32, 101	sstri 3968	. . . . . . . . . 10 ⊢ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ⊆ ℝ^*
144		infxrunb2 45343	. . . . . . . . . 10 ⊢ ({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ⊆ ℝ^* → (∀𝑣 ∈ ℝ ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣 ↔ inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -∞))
145	143, 144	ax-mp 5	. . . . . . . . 9 ⊢ (∀𝑣 ∈ ℝ ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣 ↔ inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -∞)
146	142, 145	sylib 218	. . . . . . . 8 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -∞)
147	146	xnegeqd 45412	. . . . . . 7 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -_𝑒-∞)
148	99, 107, 147	3eqtr4d 2780	. . . . . 6 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))
149	96, 148	syldan 591	. . . . 5 ⊢ ((𝜑 ∧ ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))
150	149	adantlr 715	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))
151	81, 150	pm2.61dan 812	. . 3 ⊢ ((𝜑 ∧ 𝐴 ≠ ∅) → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))
152	25, 151	sylan2 593	. 2 ⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))
153	24, 152	pm2.61dan 812	1 ⊢ (𝜑 → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2108 ≠ wne 2932 ∀wral 3051 ∃wrex 3060 {crab 3415 ⊆ wss 3926 ∅c0 4308 class class class wbr 5119 supcsup 9450 infcinf 9451 ℂcc 11125 ℝcr 11126 +∞cpnf 11264 -∞cmnf 11265 ℝ^*cxr 11266 < clt 11267 ≤ cle 11268 -cneg 11465 -_𝑒cxne 13123

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-sep 5266 ax-nul 5276 ax-pow 5335 ax-pr 5402 ax-un 7727 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204 ax-pre-sup 11205

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3359 df-reu 3360 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-op 4608 df-uni 4884 df-br 5120 df-opab 5182 df-mpt 5202 df-id 5548 df-po 5561 df-so 5562 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-iota 6483 df-fun 6532 df-fn 6533 df-f 6534 df-f1 6535 df-fo 6536 df-f1o 6537 df-fv 6538 df-isom 6539 df-riota 7360 df-ov 7406 df-oprab 7407 df-mpo 7408 df-er 8717 df-en 8958 df-dom 8959 df-sdom 8960 df-sup 9452 df-inf 9453 df-pnf 11269 df-mnf 11270 df-xr 11271 df-ltxr 11272 df-le 11273 df-sub 11466 df-neg 11467 df-xneg 13126

This theorem is referenced by: supminfxr2 45444

W3C validator