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 42963

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 9192	. . . . 5 ⊢ (𝐴 = ∅ → sup(𝐴, ℝ^, < ) = sup(∅, ℝ^, < ))
2		xrsup0 13045	. . . . . 6 ⊢ sup(∅, ℝ^*, < ) = -∞
3	2	a1i 11	. . . . 5 ⊢ (𝐴 = ∅ → sup(∅, ℝ^*, < ) = -∞)
4	1, 3	eqtrd 2778	. . . 4 ⊢ (𝐴 = ∅ → sup(𝐴, ℝ^*, < ) = -∞)
5	4	adantl 482	. . 3 ⊢ ((𝜑 ∧ 𝐴 = ∅) → sup(𝐴, ℝ^*, < ) = -∞)
6		eleq2 2827	. . . . . . . . . 10 ⊢ (𝐴 = ∅ → (-𝑥 ∈ 𝐴 ↔ -𝑥 ∈ ∅))
7	6	rabbidv 3412	. . . . . . . . 9 ⊢ (𝐴 = ∅ → {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} = {𝑥 ∈ ℝ ∣ -𝑥 ∈ ∅})
8		noel 4265	. . . . . . . . . . . . 13 ⊢ ¬ -𝑥 ∈ ∅
9	8	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → ¬ -𝑥 ∈ ∅)
10	9	rgen 3074	. . . . . . . . . . 11 ⊢ ∀𝑥 ∈ ℝ ¬ -𝑥 ∈ ∅
11		rabeq0 4319	. . . . . . . . . . 11 ⊢ ({𝑥 ∈ ℝ ∣ -𝑥 ∈ ∅} = ∅ ↔ ∀𝑥 ∈ ℝ ¬ -𝑥 ∈ ∅)
12	10, 11	mpbir 230	. . . . . . . . . 10 ⊢ {𝑥 ∈ ℝ ∣ -𝑥 ∈ ∅} = ∅
13	12	a1i 11	. . . . . . . . 9 ⊢ (𝐴 = ∅ → {𝑥 ∈ ℝ ∣ -𝑥 ∈ ∅} = ∅)
14	7, 13	eqtrd 2778	. . . . . . . 8 ⊢ (𝐴 = ∅ → {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} = ∅)
15	14	infeq1d 9224	. . . . . . 7 ⊢ (𝐴 = ∅ → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ) = inf(∅, ℝ^, < ))
16		xrinf0 13060	. . . . . . . 8 ⊢ inf(∅, ℝ^*, < ) = +∞
17	16	a1i 11	. . . . . . 7 ⊢ (𝐴 = ∅ → inf(∅, ℝ^*, < ) = +∞)
18	15, 17	eqtrd 2778	. . . . . 6 ⊢ (𝐴 = ∅ → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = +∞)
19	18	xnegeqd 42936	. . . . 5 ⊢ (𝐴 = ∅ → -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -_𝑒+∞)
20		xnegpnf 12931	. . . . . 6 ⊢ -_𝑒+∞ = -∞
21	20	a1i 11	. . . . 5 ⊢ (𝐴 = ∅ → -_𝑒+∞ = -∞)
22	19, 21	eqtrd 2778	. . . 4 ⊢ (𝐴 = ∅ → -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -∞)
23	22	adantl 482	. . 3 ⊢ ((𝜑 ∧ 𝐴 = ∅) → -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -∞)
24	5, 23	eqtr4d 2781	. 2 ⊢ ((𝜑 ∧ 𝐴 = ∅) → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))
25		neqne 2951	. . 3 ⊢ (¬ 𝐴 = ∅ → 𝐴 ≠ ∅)
26		supminfxr.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
27	26	ad2antrr 723	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → 𝐴 ⊆ ℝ)
28		simplr 766	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → 𝐴 ≠ ∅)
29		simpr 485	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦)
30		negn0 11392	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) → {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ≠ ∅)
31		ublbneg 12661	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑦 ≤ 𝑧)
32		ssrab2 4013	. . . . . . . . . . 11 ⊢ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ⊆ ℝ
33		infrenegsup 11946	. . . . . . . . . . 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 3618	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}} → 𝑦 ∈ ℝ)
38	37	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}) → 𝑦 ∈ ℝ)
39		ssel2 3916	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ)
40		negeq 11201	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑦 → -𝑤 = -𝑦)
41	40	eleq1d 2823	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑦 → (-𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ↔ -𝑦 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}))
42	41	elrab3 3625	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ → (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}} ↔ -𝑦 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}))
43		renegcl 11272	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℝ → -𝑦 ∈ ℝ)
44		negeq 11201	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = -𝑦 → -𝑥 = --𝑦)
45	44	eleq1d 2823	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = -𝑦 → (-𝑥 ∈ 𝐴 ↔ --𝑦 ∈ 𝐴))
46	45	elrab3 3625	. . . . . . . . . . . . . . 15 ⊢ (-𝑦 ∈ ℝ → (-𝑦 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ↔ --𝑦 ∈ 𝐴))
47	43, 46	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ → (-𝑦 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ↔ --𝑦 ∈ 𝐴))
48		recn 10949	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
49	48	negnegd 11311	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℝ → --𝑦 = 𝑦)
50	49	eleq1d 2823	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ → (--𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
51	42, 47, 50	3bitrd 305	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℝ → (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}} ↔ 𝑦 ∈ 𝐴))
52	51	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ) → (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}} ↔ 𝑦 ∈ 𝐴))
53	38, 39, 52	eqrdav 2737	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ ℝ → {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}} = 𝐴)
54	53	supeq1d 9193	. . . . . . . . . 10 ⊢ (𝐴 ⊆ ℝ → sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}, ℝ, < ) = sup(𝐴, ℝ, < ))
55	54	3ad2ant1 1132	. . . . . . . . 9 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}, ℝ, < ) = sup(𝐴, ℝ, < ))
56	55	negeqd 11203	. . . . . . . 8 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → -sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}, ℝ, < ) = -sup(𝐴, ℝ, < ))
57	36, 56	eqtrd 2778	. . . . . . 7 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) = -sup(𝐴, ℝ, < ))
58		infrecl 11945	. . . . . . . . . . 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 11923	. . . . . . . 8 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ, < ) ∈ ℝ)
63		recn 10949	. . . . . . . . 9 ⊢ (inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℝ → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℂ)
64		recn 10949	. . . . . . . . 9 ⊢ (sup(𝐴, ℝ, < ) ∈ ℝ → sup(𝐴, ℝ, < ) ∈ ℂ)
65		negcon2 11262	. . . . . . . . 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 231	. . . . . 6 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ, < ) = -inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ))
69	27, 28, 29, 68	syl3anc 1370	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ, < ) = -inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ))
70		supxrre 13049	. . . . . 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 13058	. . . . . . . 8 ⊢ (({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ⊆ ℝ ∧ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑦 ≤ 𝑧) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ))
76	72, 73, 74, 75	syl3anc 1370	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ))
77	76	xnegeqd 42936	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ))
78	26, 60	sylanl1 677	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℝ)
79	78	rexnegd 42651	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) = -inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ))
80	77, 79	eqtrd 2778	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ))
81	69, 71, 80	3eqtr4d 2788	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))
82		simpr 485	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦)
83		simplr 766	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → 𝑦 ∈ ℝ)
84	26	sselda 3921	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℝ)
85	84	adantlr 712	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℝ)
86	83, 85	ltnled 11110	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → (𝑦 < 𝑧 ↔ ¬ 𝑧 ≤ 𝑦))
87	86	rexbidva 3223	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ∃𝑧 ∈ 𝐴 ¬ 𝑧 ≤ 𝑦))
88		rexnal 3167	. . . . . . . . . . . 12 ⊢ (∃𝑧 ∈ 𝐴 ¬ 𝑧 ≤ 𝑦 ↔ ¬ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦)
89	88	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∃𝑧 ∈ 𝐴 ¬ 𝑧 ≤ 𝑦 ↔ ¬ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦))
90	87, 89	bitrd 278	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ¬ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦))
91	90	ralbidva 3107	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ∀𝑦 ∈ ℝ ¬ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦))
92		ralnex 3165	. . . . . . . . . 10 ⊢ (∀𝑦 ∈ ℝ ¬ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ↔ ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦)
93	92	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑦 ∈ ℝ ¬ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ↔ ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦))
94	91, 93	bitrd 278	. . . . . . . 8 ⊢ (𝜑 → (∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦))
95	94	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → (∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦))
96	82, 95	mpbird 256	. . . . . 6 ⊢ ((𝜑 ∧ ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)
97		xnegmnf 12932	. . . . . . . . 9 ⊢ -_𝑒-∞ = +∞
98	97	eqcomi 2747	. . . . . . . 8 ⊢ +∞ = -_𝑒-∞
99	98	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → +∞ = -_𝑒-∞)
100		simpr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)
101		ressxr 11007	. . . . . . . . . . . 12 ⊢ ℝ ⊆ ℝ^*
102	101	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → ℝ ⊆ ℝ^*)
103	26, 102	sstrd 3931	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ⊆ ℝ^*)
104		supxrunb2 13042	. . . . . . . . . 10 ⊢ (𝐴 ⊆ ℝ^* → (∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ sup(𝐴, ℝ^*, < ) = +∞))
105	103, 104	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ sup(𝐴, ℝ^*, < ) = +∞))
106	105	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → (∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ sup(𝐴, ℝ^*, < ) = +∞))
107	100, 106	mpbid 231	. . . . . . 7 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → sup(𝐴, ℝ^*, < ) = +∞)
108		renegcl 11272	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ ℝ → -𝑣 ∈ ℝ)
109	108	adantl 482	. . . . . . . . . . . . 13 ⊢ ((∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ∧ 𝑣 ∈ ℝ) → -𝑣 ∈ ℝ)
110		simpl 483	. . . . . . . . . . . . 13 ⊢ ((∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ∧ 𝑣 ∈ ℝ) → ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)
111		breq1 5077	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = -𝑣 → (𝑦 < 𝑧 ↔ -𝑣 < 𝑧))
112	111	rexbidv 3224	. . . . . . . . . . . . . 14 ⊢ (𝑦 = -𝑣 → (∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ∃𝑧 ∈ 𝐴 -𝑣 < 𝑧))
113	112	rspcva 3558	. . . . . . . . . . . . 13 ⊢ ((-𝑣 ∈ ℝ ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → ∃𝑧 ∈ 𝐴 -𝑣 < 𝑧)
114	109, 110, 113	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ∧ 𝑣 ∈ ℝ) → ∃𝑧 ∈ 𝐴 -𝑣 < 𝑧)
115	114	adantll 711	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) ∧ 𝑣 ∈ ℝ) → ∃𝑧 ∈ 𝐴 -𝑣 < 𝑧)
116		negeq 11201	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = -𝑧 → -𝑥 = --𝑧)
117	116	eleq1d 2823	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = -𝑧 → (-𝑥 ∈ 𝐴 ↔ --𝑧 ∈ 𝐴))
118	84	renegcld 11390	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → -𝑧 ∈ ℝ)
119	118	ad4ant13 748	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → -𝑧 ∈ ℝ)
120	84	recnd 10991	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℂ)
121	120	negnegd 11311	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → --𝑧 = 𝑧)
122		simpr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴)
123	121, 122	eqeltrd 2839	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → --𝑧 ∈ 𝐴)
124	123	ad4ant13 748	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → --𝑧 ∈ 𝐴)
125	117, 119, 124	elrabd 3626	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → -𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴})
126		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → -𝑣 < 𝑧)
127	108	ad3antlr 728	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → -𝑣 ∈ ℝ)
128	84	ad4ant13 748	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → 𝑧 ∈ ℝ)
129	127, 128	ltnegd 11541	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → (-𝑣 < 𝑧 ↔ -𝑧 < --𝑣))
130	126, 129	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → -𝑧 < --𝑣)
131		simpllr 773	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → 𝑣 ∈ ℝ)
132		recn 10949	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ ℝ → 𝑣 ∈ ℂ)
133		negneg 11259	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ ℂ → --𝑣 = 𝑣)
134	131, 132, 133	3syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → --𝑣 = 𝑣)
135	130, 134	breqtrd 5100	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → -𝑧 < 𝑣)
136		breq1 5077	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = -𝑧 → (𝑤 < 𝑣 ↔ -𝑧 < 𝑣))
137	136	rspcev 3560	. . . . . . . . . . . . . 14 ⊢ ((-𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ∧ -𝑧 < 𝑣) → ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣)
138	125, 135, 137	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣)
139	138	rexlimdva2 3214	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑣 ∈ ℝ) → (∃𝑧 ∈ 𝐴 -𝑣 < 𝑧 → ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣))
140	139	adantlr 712	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) ∧ 𝑣 ∈ ℝ) → (∃𝑧 ∈ 𝐴 -𝑣 < 𝑧 → ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣))
141	115, 140	mpd 15	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) ∧ 𝑣 ∈ ℝ) → ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣)
142	141	ralrimiva 3113	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → ∀𝑣 ∈ ℝ ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣)
143	32, 101	sstri 3930	. . . . . . . . . 10 ⊢ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ⊆ ℝ^*
144		infxrunb2 42866	. . . . . . . . . 10 ⊢ ({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ⊆ ℝ^* → (∀𝑣 ∈ ℝ ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣 ↔ inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -∞))
145	143, 144	ax-mp 5	. . . . . . . . 9 ⊢ (∀𝑣 ∈ ℝ ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣 ↔ inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -∞)
146	142, 145	sylib 217	. . . . . . . 8 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -∞)
147	146	xnegeqd 42936	. . . . . . 7 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -_𝑒-∞)
148	99, 107, 147	3eqtr4d 2788	. . . . . 6 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))
149	96, 148	syldan 591	. . . . 5 ⊢ ((𝜑 ∧ ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))
150	149	adantlr 712	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))
151	81, 150	pm2.61dan 810	. . 3 ⊢ ((𝜑 ∧ 𝐴 ≠ ∅) → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))
152	25, 151	sylan2 593	. 2 ⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))
153	24, 152	pm2.61dan 810	1 ⊢ (𝜑 → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 ≠ wne 2943 ∀wral 3064 ∃wrex 3065 {crab 3068 ⊆ wss 3887 ∅c0 4257 class class class wbr 5074 supcsup 9187 infcinf 9188 ℂcc 10857 ℝcr 10858 +∞cpnf 10994 -∞cmnf 10995 ℝ^*cxr 10996 < clt 10997 ≤ cle 10998 -cneg 11194 -_𝑒cxne 12833

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-sep 5222 ax-nul 5229 ax-pow 5287 ax-pr 5351 ax-un 7579 ax-cnex 10915 ax-resscn 10916 ax-1cn 10917 ax-icn 10918 ax-addcl 10919 ax-addrcl 10920 ax-mulcl 10921 ax-mulrcl 10922 ax-mulcom 10923 ax-addass 10924 ax-mulass 10925 ax-distr 10926 ax-i2m1 10927 ax-1ne0 10928 ax-1rid 10929 ax-rnegex 10930 ax-rrecex 10931 ax-cnre 10932 ax-pre-lttri 10933 ax-pre-lttrn 10934 ax-pre-ltadd 10935 ax-pre-mulgt0 10936 ax-pre-sup 10937

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-reu 3071 df-rmo 3072 df-rab 3073 df-v 3432 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4258 df-if 4461 df-pw 4536 df-sn 4563 df-pr 4565 df-op 4569 df-uni 4841 df-br 5075 df-opab 5137 df-mpt 5158 df-id 5485 df-po 5499 df-so 5500 df-xp 5591 df-rel 5592 df-cnv 5593 df-co 5594 df-dm 5595 df-rn 5596 df-res 5597 df-ima 5598 df-iota 6385 df-fun 6429 df-fn 6430 df-f 6431 df-f1 6432 df-fo 6433 df-f1o 6434 df-fv 6435 df-isom 6436 df-riota 7225 df-ov 7271 df-oprab 7272 df-mpo 7273 df-er 8486 df-en 8722 df-dom 8723 df-sdom 8724 df-sup 9189 df-inf 9190 df-pnf 10999 df-mnf 11000 df-xr 11001 df-ltxr 11002 df-le 11003 df-sub 11195 df-neg 11196 df-xneg 12836

This theorem is referenced by: supminfxr2 42968

W3C validator