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 45413

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 9482	. . . . 5 ⊢ (𝐴 = ∅ → sup(𝐴, ℝ^, < ) = sup(∅, ℝ^, < ))
2		xrsup0 13361	. . . . . 6 ⊢ sup(∅, ℝ^*, < ) = -∞
3	2	a1i 11	. . . . 5 ⊢ (𝐴 = ∅ → sup(∅, ℝ^*, < ) = -∞)
4	1, 3	eqtrd 2774	. . . 4 ⊢ (𝐴 = ∅ → sup(𝐴, ℝ^*, < ) = -∞)
5	4	adantl 481	. . 3 ⊢ ((𝜑 ∧ 𝐴 = ∅) → sup(𝐴, ℝ^*, < ) = -∞)
6		eleq2 2827	. . . . . . . . . 10 ⊢ (𝐴 = ∅ → (-𝑥 ∈ 𝐴 ↔ -𝑥 ∈ ∅))
7	6	rabbidv 3440	. . . . . . . . 9 ⊢ (𝐴 = ∅ → {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} = {𝑥 ∈ ℝ ∣ -𝑥 ∈ ∅})
8		noel 4343	. . . . . . . . . . . . 13 ⊢ ¬ -𝑥 ∈ ∅
9	8	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → ¬ -𝑥 ∈ ∅)
10	9	rgen 3060	. . . . . . . . . . 11 ⊢ ∀𝑥 ∈ ℝ ¬ -𝑥 ∈ ∅
11		rabeq0 4393	. . . . . . . . . . 11 ⊢ ({𝑥 ∈ ℝ ∣ -𝑥 ∈ ∅} = ∅ ↔ ∀𝑥 ∈ ℝ ¬ -𝑥 ∈ ∅)
12	10, 11	mpbir 231	. . . . . . . . . 10 ⊢ {𝑥 ∈ ℝ ∣ -𝑥 ∈ ∅} = ∅
13	12	a1i 11	. . . . . . . . 9 ⊢ (𝐴 = ∅ → {𝑥 ∈ ℝ ∣ -𝑥 ∈ ∅} = ∅)
14	7, 13	eqtrd 2774	. . . . . . . 8 ⊢ (𝐴 = ∅ → {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} = ∅)
15	14	infeq1d 9514	. . . . . . 7 ⊢ (𝐴 = ∅ → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ) = inf(∅, ℝ^, < ))
16		xrinf0 13376	. . . . . . . 8 ⊢ inf(∅, ℝ^*, < ) = +∞
17	16	a1i 11	. . . . . . 7 ⊢ (𝐴 = ∅ → inf(∅, ℝ^*, < ) = +∞)
18	15, 17	eqtrd 2774	. . . . . 6 ⊢ (𝐴 = ∅ → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = +∞)
19	18	xnegeqd 45386	. . . . 5 ⊢ (𝐴 = ∅ → -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -_𝑒+∞)
20		xnegpnf 13247	. . . . . 6 ⊢ -_𝑒+∞ = -∞
21	20	a1i 11	. . . . 5 ⊢ (𝐴 = ∅ → -_𝑒+∞ = -∞)
22	19, 21	eqtrd 2774	. . . 4 ⊢ (𝐴 = ∅ → -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -∞)
23	22	adantl 481	. . 3 ⊢ ((𝜑 ∧ 𝐴 = ∅) → -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -∞)
24	5, 23	eqtr4d 2777	. 2 ⊢ ((𝜑 ∧ 𝐴 = ∅) → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))
25		neqne 2945	. . 3 ⊢ (¬ 𝐴 = ∅ → 𝐴 ≠ ∅)
26		supminfxr.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
27	26	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → 𝐴 ⊆ ℝ)
28		simplr 769	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → 𝐴 ≠ ∅)
29		simpr 484	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦)
30		negn0 11689	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) → {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ≠ ∅)
31		ublbneg 12972	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑦 ≤ 𝑧)
32		ssrab2 4089	. . . . . . . . . . 11 ⊢ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ⊆ ℝ
33		infrenegsup 12248	. . . . . . . . . . 11 ⊢ (({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ⊆ ℝ ∧ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑦 ≤ 𝑧) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) = -sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}, ℝ, < ))
34	32, 33	mp3an1 1447	. . . . . . . . . 10 ⊢ (({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑦 ≤ 𝑧) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) = -sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}, ℝ, < ))
35	30, 31, 34	syl2an 596	. . . . . . . . 9 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) = -sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}, ℝ, < ))
36	35	3impa 1109	. . . . . . . 8 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) = -sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}, ℝ, < ))
37		elrabi 3689	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}} → 𝑦 ∈ ℝ)
38	37	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}) → 𝑦 ∈ ℝ)
39		ssel2 3989	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ)
40		negeq 11497	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑦 → -𝑤 = -𝑦)
41	40	eleq1d 2823	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑦 → (-𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ↔ -𝑦 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}))
42	41	elrab3 3695	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ → (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}} ↔ -𝑦 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}))
43		renegcl 11569	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℝ → -𝑦 ∈ ℝ)
44		negeq 11497	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = -𝑦 → -𝑥 = --𝑦)
45	44	eleq1d 2823	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = -𝑦 → (-𝑥 ∈ 𝐴 ↔ --𝑦 ∈ 𝐴))
46	45	elrab3 3695	. . . . . . . . . . . . . . 15 ⊢ (-𝑦 ∈ ℝ → (-𝑦 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ↔ --𝑦 ∈ 𝐴))
47	43, 46	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ → (-𝑦 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ↔ --𝑦 ∈ 𝐴))
48		recn 11242	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
49	48	negnegd 11608	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℝ → --𝑦 = 𝑦)
50	49	eleq1d 2823	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ → (--𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
51	42, 47, 50	3bitrd 305	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℝ → (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}} ↔ 𝑦 ∈ 𝐴))
52	51	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ) → (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}} ↔ 𝑦 ∈ 𝐴))
53	38, 39, 52	eqrdav 2733	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ ℝ → {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}} = 𝐴)
54	53	supeq1d 9483	. . . . . . . . . 10 ⊢ (𝐴 ⊆ ℝ → sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}, ℝ, < ) = sup(𝐴, ℝ, < ))
55	54	3ad2ant1 1132	. . . . . . . . 9 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}, ℝ, < ) = sup(𝐴, ℝ, < ))
56	55	negeqd 11499	. . . . . . . 8 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → -sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}, ℝ, < ) = -sup(𝐴, ℝ, < ))
57	36, 56	eqtrd 2774	. . . . . . 7 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) = -sup(𝐴, ℝ, < ))
58		infrecl 12247	. . . . . . . . . . 11 ⊢ (({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ⊆ ℝ ∧ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑦 ≤ 𝑧) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℝ)
59	32, 58	mp3an1 1447	. . . . . . . . . 10 ⊢ (({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑦 ≤ 𝑧) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℝ)
60	30, 31, 59	syl2an 596	. . . . . . . . 9 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℝ)
61	60	3impa 1109	. . . . . . . 8 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℝ)
62		suprcl 12225	. . . . . . . 8 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ, < ) ∈ ℝ)
63		recn 11242	. . . . . . . . 9 ⊢ (inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℝ → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℂ)
64		recn 11242	. . . . . . . . 9 ⊢ (sup(𝐴, ℝ, < ) ∈ ℝ → sup(𝐴, ℝ, < ) ∈ ℂ)
65		negcon2 11559	. . . . . . . . 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 1370	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ, < ) = -inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ))
70		supxrre 13365	. . . . . 6 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ^*, < ) = sup(𝐴, ℝ, < ))
71	27, 28, 29, 70	syl3anc 1370	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ^*, < ) = sup(𝐴, ℝ, < ))
72	32	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ⊆ ℝ)
73	27, 28, 30	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ≠ ∅)
74	29, 31	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑦 ≤ 𝑧)
75		infxrre 13374	. . . . . . . 8 ⊢ (({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ⊆ ℝ ∧ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑦 ≤ 𝑧) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ))
76	72, 73, 74, 75	syl3anc 1370	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ))
77	76	xnegeqd 45386	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ))
78	26, 60	sylanl1 680	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℝ)
79	78	rexnegd 45082	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) = -inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ))
80	77, 79	eqtrd 2774	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ))
81	69, 71, 80	3eqtr4d 2784	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))
82		simpr 484	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦)
83		simplr 769	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → 𝑦 ∈ ℝ)
84	26	sselda 3994	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℝ)
85	84	adantlr 715	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℝ)
86	83, 85	ltnled 11405	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → (𝑦 < 𝑧 ↔ ¬ 𝑧 ≤ 𝑦))
87	86	rexbidva 3174	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ∃𝑧 ∈ 𝐴 ¬ 𝑧 ≤ 𝑦))
88		rexnal 3097	. . . . . . . . . . . 12 ⊢ (∃𝑧 ∈ 𝐴 ¬ 𝑧 ≤ 𝑦 ↔ ¬ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦)
89	88	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∃𝑧 ∈ 𝐴 ¬ 𝑧 ≤ 𝑦 ↔ ¬ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦))
90	87, 89	bitrd 279	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ¬ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦))
91	90	ralbidva 3173	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ∀𝑦 ∈ ℝ ¬ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦))
92		ralnex 3069	. . . . . . . . . 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 13248	. . . . . . . . 9 ⊢ -_𝑒-∞ = +∞
98	97	eqcomi 2743	. . . . . . . 8 ⊢ +∞ = -_𝑒-∞
99	98	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → +∞ = -_𝑒-∞)
100		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)
101		ressxr 11302	. . . . . . . . . . . 12 ⊢ ℝ ⊆ ℝ^*
102	101	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → ℝ ⊆ ℝ^*)
103	26, 102	sstrd 4005	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ⊆ ℝ^*)
104		supxrunb2 13358	. . . . . . . . . 10 ⊢ (𝐴 ⊆ ℝ^* → (∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ sup(𝐴, ℝ^*, < ) = +∞))
105	103, 104	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ sup(𝐴, ℝ^*, < ) = +∞))
106	105	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → (∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ sup(𝐴, ℝ^*, < ) = +∞))
107	100, 106	mpbid 232	. . . . . . 7 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → sup(𝐴, ℝ^*, < ) = +∞)
108		renegcl 11569	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ ℝ → -𝑣 ∈ ℝ)
109	108	adantl 481	. . . . . . . . . . . . 13 ⊢ ((∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ∧ 𝑣 ∈ ℝ) → -𝑣 ∈ ℝ)
110		simpl 482	. . . . . . . . . . . . 13 ⊢ ((∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ∧ 𝑣 ∈ ℝ) → ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)
111		breq1 5150	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = -𝑣 → (𝑦 < 𝑧 ↔ -𝑣 < 𝑧))
112	111	rexbidv 3176	. . . . . . . . . . . . . 14 ⊢ (𝑦 = -𝑣 → (∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ∃𝑧 ∈ 𝐴 -𝑣 < 𝑧))
113	112	rspcva 3619	. . . . . . . . . . . . 13 ⊢ ((-𝑣 ∈ ℝ ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → ∃𝑧 ∈ 𝐴 -𝑣 < 𝑧)
114	109, 110, 113	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ∧ 𝑣 ∈ ℝ) → ∃𝑧 ∈ 𝐴 -𝑣 < 𝑧)
115	114	adantll 714	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) ∧ 𝑣 ∈ ℝ) → ∃𝑧 ∈ 𝐴 -𝑣 < 𝑧)
116		negeq 11497	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = -𝑧 → -𝑥 = --𝑧)
117	116	eleq1d 2823	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = -𝑧 → (-𝑥 ∈ 𝐴 ↔ --𝑧 ∈ 𝐴))
118	84	renegcld 11687	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → -𝑧 ∈ ℝ)
119	118	ad4ant13 751	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → -𝑧 ∈ ℝ)
120	84	recnd 11286	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℂ)
121	120	negnegd 11608	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → --𝑧 = 𝑧)
122		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴)
123	121, 122	eqeltrd 2838	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → --𝑧 ∈ 𝐴)
124	123	ad4ant13 751	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → --𝑧 ∈ 𝐴)
125	117, 119, 124	elrabd 3696	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → -𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴})
126		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → -𝑣 < 𝑧)
127	108	ad3antlr 731	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → -𝑣 ∈ ℝ)
128	84	ad4ant13 751	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → 𝑧 ∈ ℝ)
129	127, 128	ltnegd 11838	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → (-𝑣 < 𝑧 ↔ -𝑧 < --𝑣))
130	126, 129	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → -𝑧 < --𝑣)
131		simpllr 776	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → 𝑣 ∈ ℝ)
132		recn 11242	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ ℝ → 𝑣 ∈ ℂ)
133		negneg 11556	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ ℂ → --𝑣 = 𝑣)
134	131, 132, 133	3syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → --𝑣 = 𝑣)
135	130, 134	breqtrd 5173	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → -𝑧 < 𝑣)
136		breq1 5150	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = -𝑧 → (𝑤 < 𝑣 ↔ -𝑧 < 𝑣))
137	136	rspcev 3621	. . . . . . . . . . . . . 14 ⊢ ((-𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ∧ -𝑧 < 𝑣) → ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣)
138	125, 135, 137	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣)
139	138	rexlimdva2 3154	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑣 ∈ ℝ) → (∃𝑧 ∈ 𝐴 -𝑣 < 𝑧 → ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣))
140	139	adantlr 715	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) ∧ 𝑣 ∈ ℝ) → (∃𝑧 ∈ 𝐴 -𝑣 < 𝑧 → ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣))
141	115, 140	mpd 15	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) ∧ 𝑣 ∈ ℝ) → ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣)
142	141	ralrimiva 3143	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → ∀𝑣 ∈ ℝ ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣)
143	32, 101	sstri 4004	. . . . . . . . . 10 ⊢ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ⊆ ℝ^*
144		infxrunb2 45317	. . . . . . . . . 10 ⊢ ({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ⊆ ℝ^* → (∀𝑣 ∈ ℝ ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣 ↔ inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -∞))
145	143, 144	ax-mp 5	. . . . . . . . 9 ⊢ (∀𝑣 ∈ ℝ ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣 ↔ inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -∞)
146	142, 145	sylib 218	. . . . . . . 8 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -∞)
147	146	xnegeqd 45386	. . . . . . 7 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -_𝑒-∞)
148	99, 107, 147	3eqtr4d 2784	. . . . . 6 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))
149	96, 148	syldan 591	. . . . 5 ⊢ ((𝜑 ∧ ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))
150	149	adantlr 715	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))
151	81, 150	pm2.61dan 813	. . 3 ⊢ ((𝜑 ∧ 𝐴 ≠ ∅) → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))
152	25, 151	sylan2 593	. 2 ⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))
153	24, 152	pm2.61dan 813	1 ⊢ (𝜑 → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1536 ∈ wcel 2105 ≠ wne 2937 ∀wral 3058 ∃wrex 3067 {crab 3432 ⊆ wss 3962 ∅c0 4338 class class class wbr 5147 supcsup 9477 infcinf 9478 ℂcc 11150 ℝcr 11151 +∞cpnf 11289 -∞cmnf 11290 ℝ^*cxr 11291 < clt 11292 ≤ cle 11293 -cneg 11490 -_𝑒cxne 13148

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 ax-sep 5301 ax-nul 5311 ax-pow 5370 ax-pr 5437 ax-un 7753 ax-cnex 11208 ax-resscn 11209 ax-1cn 11210 ax-icn 11211 ax-addcl 11212 ax-addrcl 11213 ax-mulcl 11214 ax-mulrcl 11215 ax-mulcom 11216 ax-addass 11217 ax-mulass 11218 ax-distr 11219 ax-i2m1 11220 ax-1ne0 11221 ax-1rid 11222 ax-rnegex 11223 ax-rrecex 11224 ax-cnre 11225 ax-pre-lttri 11226 ax-pre-lttrn 11227 ax-pre-ltadd 11228 ax-pre-mulgt0 11229 ax-pre-sup 11230

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-nf 1780 df-sb 2062 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-ne 2938 df-nel 3044 df-ral 3059 df-rex 3068 df-rmo 3377 df-reu 3378 df-rab 3433 df-v 3479 df-sbc 3791 df-csb 3908 df-dif 3965 df-un 3967 df-in 3969 df-ss 3979 df-nul 4339 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4912 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5582 df-po 5596 df-so 5597 df-xp 5694 df-rel 5695 df-cnv 5696 df-co 5697 df-dm 5698 df-rn 5699 df-res 5700 df-ima 5701 df-iota 6515 df-fun 6564 df-fn 6565 df-f 6566 df-f1 6567 df-fo 6568 df-f1o 6569 df-fv 6570 df-isom 6571 df-riota 7387 df-ov 7433 df-oprab 7434 df-mpo 7435 df-er 8743 df-en 8984 df-dom 8985 df-sdom 8986 df-sup 9479 df-inf 9480 df-pnf 11294 df-mnf 11295 df-xr 11296 df-ltxr 11297 df-le 11298 df-sub 11491 df-neg 11492 df-xneg 13151

This theorem is referenced by: supminfxr2 45418

W3C validator