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 45379

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 9514	. . . . 5 ⊢ (𝐴 = ∅ → sup(𝐴, ℝ^, < ) = sup(∅, ℝ^, < ))
2		xrsup0 13385	. . . . . 6 ⊢ sup(∅, ℝ^*, < ) = -∞
3	2	a1i 11	. . . . 5 ⊢ (𝐴 = ∅ → sup(∅, ℝ^*, < ) = -∞)
4	1, 3	eqtrd 2780	. . . 4 ⊢ (𝐴 = ∅ → sup(𝐴, ℝ^*, < ) = -∞)
5	4	adantl 481	. . 3 ⊢ ((𝜑 ∧ 𝐴 = ∅) → sup(𝐴, ℝ^*, < ) = -∞)
6		eleq2 2833	. . . . . . . . . 10 ⊢ (𝐴 = ∅ → (-𝑥 ∈ 𝐴 ↔ -𝑥 ∈ ∅))
7	6	rabbidv 3451	. . . . . . . . 9 ⊢ (𝐴 = ∅ → {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} = {𝑥 ∈ ℝ ∣ -𝑥 ∈ ∅})
8		noel 4360	. . . . . . . . . . . . 13 ⊢ ¬ -𝑥 ∈ ∅
9	8	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → ¬ -𝑥 ∈ ∅)
10	9	rgen 3069	. . . . . . . . . . 11 ⊢ ∀𝑥 ∈ ℝ ¬ -𝑥 ∈ ∅
11		rabeq0 4411	. . . . . . . . . . 11 ⊢ ({𝑥 ∈ ℝ ∣ -𝑥 ∈ ∅} = ∅ ↔ ∀𝑥 ∈ ℝ ¬ -𝑥 ∈ ∅)
12	10, 11	mpbir 231	. . . . . . . . . 10 ⊢ {𝑥 ∈ ℝ ∣ -𝑥 ∈ ∅} = ∅
13	12	a1i 11	. . . . . . . . 9 ⊢ (𝐴 = ∅ → {𝑥 ∈ ℝ ∣ -𝑥 ∈ ∅} = ∅)
14	7, 13	eqtrd 2780	. . . . . . . 8 ⊢ (𝐴 = ∅ → {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} = ∅)
15	14	infeq1d 9546	. . . . . . 7 ⊢ (𝐴 = ∅ → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ) = inf(∅, ℝ^, < ))
16		xrinf0 13400	. . . . . . . 8 ⊢ inf(∅, ℝ^*, < ) = +∞
17	16	a1i 11	. . . . . . 7 ⊢ (𝐴 = ∅ → inf(∅, ℝ^*, < ) = +∞)
18	15, 17	eqtrd 2780	. . . . . 6 ⊢ (𝐴 = ∅ → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = +∞)
19	18	xnegeqd 45352	. . . . 5 ⊢ (𝐴 = ∅ → -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -_𝑒+∞)
20		xnegpnf 13271	. . . . . 6 ⊢ -_𝑒+∞ = -∞
21	20	a1i 11	. . . . 5 ⊢ (𝐴 = ∅ → -_𝑒+∞ = -∞)
22	19, 21	eqtrd 2780	. . . 4 ⊢ (𝐴 = ∅ → -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -∞)
23	22	adantl 481	. . 3 ⊢ ((𝜑 ∧ 𝐴 = ∅) → -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -∞)
24	5, 23	eqtr4d 2783	. 2 ⊢ ((𝜑 ∧ 𝐴 = ∅) → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))
25		neqne 2954	. . 3 ⊢ (¬ 𝐴 = ∅ → 𝐴 ≠ ∅)
26		supminfxr.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
27	26	ad2antrr 725	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → 𝐴 ⊆ ℝ)
28		simplr 768	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → 𝐴 ≠ ∅)
29		simpr 484	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦)
30		negn0 11719	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) → {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ≠ ∅)
31		ublbneg 12998	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑦 ≤ 𝑧)
32		ssrab2 4103	. . . . . . . . . . 11 ⊢ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ⊆ ℝ
33		infrenegsup 12278	. . . . . . . . . . 11 ⊢ (({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ⊆ ℝ ∧ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑦 ≤ 𝑧) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) = -sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}, ℝ, < ))
34	32, 33	mp3an1 1448	. . . . . . . . . 10 ⊢ (({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑦 ≤ 𝑧) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) = -sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}, ℝ, < ))
35	30, 31, 34	syl2an 595	. . . . . . . . 9 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) = -sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}, ℝ, < ))
36	35	3impa 1110	. . . . . . . 8 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) = -sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}, ℝ, < ))
37		elrabi 3703	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}} → 𝑦 ∈ ℝ)
38	37	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}) → 𝑦 ∈ ℝ)
39		ssel2 4003	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ)
40		negeq 11528	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑦 → -𝑤 = -𝑦)
41	40	eleq1d 2829	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑦 → (-𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ↔ -𝑦 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}))
42	41	elrab3 3709	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ → (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}} ↔ -𝑦 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}))
43		renegcl 11599	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℝ → -𝑦 ∈ ℝ)
44		negeq 11528	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = -𝑦 → -𝑥 = --𝑦)
45	44	eleq1d 2829	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = -𝑦 → (-𝑥 ∈ 𝐴 ↔ --𝑦 ∈ 𝐴))
46	45	elrab3 3709	. . . . . . . . . . . . . . 15 ⊢ (-𝑦 ∈ ℝ → (-𝑦 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ↔ --𝑦 ∈ 𝐴))
47	43, 46	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ → (-𝑦 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ↔ --𝑦 ∈ 𝐴))
48		recn 11274	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
49	48	negnegd 11638	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℝ → --𝑦 = 𝑦)
50	49	eleq1d 2829	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ → (--𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
51	42, 47, 50	3bitrd 305	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℝ → (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}} ↔ 𝑦 ∈ 𝐴))
52	51	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ) → (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}} ↔ 𝑦 ∈ 𝐴))
53	38, 39, 52	eqrdav 2739	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ ℝ → {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}} = 𝐴)
54	53	supeq1d 9515	. . . . . . . . . 10 ⊢ (𝐴 ⊆ ℝ → sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}, ℝ, < ) = sup(𝐴, ℝ, < ))
55	54	3ad2ant1 1133	. . . . . . . . 9 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}, ℝ, < ) = sup(𝐴, ℝ, < ))
56	55	negeqd 11530	. . . . . . . 8 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → -sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}, ℝ, < ) = -sup(𝐴, ℝ, < ))
57	36, 56	eqtrd 2780	. . . . . . 7 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) = -sup(𝐴, ℝ, < ))
58		infrecl 12277	. . . . . . . . . . 11 ⊢ (({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ⊆ ℝ ∧ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑦 ≤ 𝑧) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℝ)
59	32, 58	mp3an1 1448	. . . . . . . . . 10 ⊢ (({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑦 ≤ 𝑧) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℝ)
60	30, 31, 59	syl2an 595	. . . . . . . . 9 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℝ)
61	60	3impa 1110	. . . . . . . 8 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℝ)
62		suprcl 12255	. . . . . . . 8 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ, < ) ∈ ℝ)
63		recn 11274	. . . . . . . . 9 ⊢ (inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℝ → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℂ)
64		recn 11274	. . . . . . . . 9 ⊢ (sup(𝐴, ℝ, < ) ∈ ℝ → sup(𝐴, ℝ, < ) ∈ ℂ)
65		negcon2 11589	. . . . . . . . 9 ⊢ ((inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℂ ∧ sup(𝐴, ℝ, < ) ∈ ℂ) → (inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) = -sup(𝐴, ℝ, < ) ↔ sup(𝐴, ℝ, < ) = -inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < )))
66	63, 64, 65	syl2an 595	. . . . . . . 8 ⊢ ((inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℝ ∧ sup(𝐴, ℝ, < ) ∈ ℝ) → (inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) = -sup(𝐴, ℝ, < ) ↔ sup(𝐴, ℝ, < ) = -inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < )))
67	61, 62, 66	syl2anc 583	. . . . . . 7 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → (inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) = -sup(𝐴, ℝ, < ) ↔ sup(𝐴, ℝ, < ) = -inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < )))
68	57, 67	mpbid 232	. . . . . 6 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ, < ) = -inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ))
69	27, 28, 29, 68	syl3anc 1371	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ, < ) = -inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ))
70		supxrre 13389	. . . . . 6 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ^*, < ) = sup(𝐴, ℝ, < ))
71	27, 28, 29, 70	syl3anc 1371	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ^*, < ) = sup(𝐴, ℝ, < ))
72	32	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ⊆ ℝ)
73	27, 28, 30	syl2anc 583	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ≠ ∅)
74	29, 31	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑦 ≤ 𝑧)
75		infxrre 13398	. . . . . . . 8 ⊢ (({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ⊆ ℝ ∧ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑦 ≤ 𝑧) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ))
76	72, 73, 74, 75	syl3anc 1371	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ))
77	76	xnegeqd 45352	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ))
78	26, 60	sylanl1 679	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℝ)
79	78	rexnegd 45045	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) = -inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ))
80	77, 79	eqtrd 2780	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ))
81	69, 71, 80	3eqtr4d 2790	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))
82		simpr 484	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦)
83		simplr 768	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → 𝑦 ∈ ℝ)
84	26	sselda 4008	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℝ)
85	84	adantlr 714	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℝ)
86	83, 85	ltnled 11437	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → (𝑦 < 𝑧 ↔ ¬ 𝑧 ≤ 𝑦))
87	86	rexbidva 3183	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ∃𝑧 ∈ 𝐴 ¬ 𝑧 ≤ 𝑦))
88		rexnal 3106	. . . . . . . . . . . 12 ⊢ (∃𝑧 ∈ 𝐴 ¬ 𝑧 ≤ 𝑦 ↔ ¬ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦)
89	88	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∃𝑧 ∈ 𝐴 ¬ 𝑧 ≤ 𝑦 ↔ ¬ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦))
90	87, 89	bitrd 279	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ¬ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦))
91	90	ralbidva 3182	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ∀𝑦 ∈ ℝ ¬ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦))
92		ralnex 3078	. . . . . . . . . 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 13272	. . . . . . . . 9 ⊢ -_𝑒-∞ = +∞
98	97	eqcomi 2749	. . . . . . . 8 ⊢ +∞ = -_𝑒-∞
99	98	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → +∞ = -_𝑒-∞)
100		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)
101		ressxr 11334	. . . . . . . . . . . 12 ⊢ ℝ ⊆ ℝ^*
102	101	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → ℝ ⊆ ℝ^*)
103	26, 102	sstrd 4019	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ⊆ ℝ^*)
104		supxrunb2 13382	. . . . . . . . . 10 ⊢ (𝐴 ⊆ ℝ^* → (∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ sup(𝐴, ℝ^*, < ) = +∞))
105	103, 104	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ sup(𝐴, ℝ^*, < ) = +∞))
106	105	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → (∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ sup(𝐴, ℝ^*, < ) = +∞))
107	100, 106	mpbid 232	. . . . . . 7 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → sup(𝐴, ℝ^*, < ) = +∞)
108		renegcl 11599	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ ℝ → -𝑣 ∈ ℝ)
109	108	adantl 481	. . . . . . . . . . . . 13 ⊢ ((∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ∧ 𝑣 ∈ ℝ) → -𝑣 ∈ ℝ)
110		simpl 482	. . . . . . . . . . . . 13 ⊢ ((∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ∧ 𝑣 ∈ ℝ) → ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)
111		breq1 5169	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = -𝑣 → (𝑦 < 𝑧 ↔ -𝑣 < 𝑧))
112	111	rexbidv 3185	. . . . . . . . . . . . . 14 ⊢ (𝑦 = -𝑣 → (∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ∃𝑧 ∈ 𝐴 -𝑣 < 𝑧))
113	112	rspcva 3633	. . . . . . . . . . . . 13 ⊢ ((-𝑣 ∈ ℝ ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → ∃𝑧 ∈ 𝐴 -𝑣 < 𝑧)
114	109, 110, 113	syl2anc 583	. . . . . . . . . . . 12 ⊢ ((∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ∧ 𝑣 ∈ ℝ) → ∃𝑧 ∈ 𝐴 -𝑣 < 𝑧)
115	114	adantll 713	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) ∧ 𝑣 ∈ ℝ) → ∃𝑧 ∈ 𝐴 -𝑣 < 𝑧)
116		negeq 11528	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = -𝑧 → -𝑥 = --𝑧)
117	116	eleq1d 2829	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = -𝑧 → (-𝑥 ∈ 𝐴 ↔ --𝑧 ∈ 𝐴))
118	84	renegcld 11717	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → -𝑧 ∈ ℝ)
119	118	ad4ant13 750	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → -𝑧 ∈ ℝ)
120	84	recnd 11318	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℂ)
121	120	negnegd 11638	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → --𝑧 = 𝑧)
122		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴)
123	121, 122	eqeltrd 2844	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → --𝑧 ∈ 𝐴)
124	123	ad4ant13 750	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → --𝑧 ∈ 𝐴)
125	117, 119, 124	elrabd 3710	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → -𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴})
126		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → -𝑣 < 𝑧)
127	108	ad3antlr 730	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → -𝑣 ∈ ℝ)
128	84	ad4ant13 750	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → 𝑧 ∈ ℝ)
129	127, 128	ltnegd 11868	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → (-𝑣 < 𝑧 ↔ -𝑧 < --𝑣))
130	126, 129	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → -𝑧 < --𝑣)
131		simpllr 775	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → 𝑣 ∈ ℝ)
132		recn 11274	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ ℝ → 𝑣 ∈ ℂ)
133		negneg 11586	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ ℂ → --𝑣 = 𝑣)
134	131, 132, 133	3syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → --𝑣 = 𝑣)
135	130, 134	breqtrd 5192	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → -𝑧 < 𝑣)
136		breq1 5169	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = -𝑧 → (𝑤 < 𝑣 ↔ -𝑧 < 𝑣))
137	136	rspcev 3635	. . . . . . . . . . . . . 14 ⊢ ((-𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ∧ -𝑧 < 𝑣) → ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣)
138	125, 135, 137	syl2anc 583	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣)
139	138	rexlimdva2 3163	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑣 ∈ ℝ) → (∃𝑧 ∈ 𝐴 -𝑣 < 𝑧 → ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣))
140	139	adantlr 714	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) ∧ 𝑣 ∈ ℝ) → (∃𝑧 ∈ 𝐴 -𝑣 < 𝑧 → ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣))
141	115, 140	mpd 15	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) ∧ 𝑣 ∈ ℝ) → ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣)
142	141	ralrimiva 3152	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → ∀𝑣 ∈ ℝ ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣)
143	32, 101	sstri 4018	. . . . . . . . . 10 ⊢ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ⊆ ℝ^*
144		infxrunb2 45283	. . . . . . . . . 10 ⊢ ({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ⊆ ℝ^* → (∀𝑣 ∈ ℝ ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣 ↔ inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -∞))
145	143, 144	ax-mp 5	. . . . . . . . 9 ⊢ (∀𝑣 ∈ ℝ ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣 ↔ inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -∞)
146	142, 145	sylib 218	. . . . . . . 8 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -∞)
147	146	xnegeqd 45352	. . . . . . 7 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -_𝑒-∞)
148	99, 107, 147	3eqtr4d 2790	. . . . . 6 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))
149	96, 148	syldan 590	. . . . 5 ⊢ ((𝜑 ∧ ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))
150	149	adantlr 714	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))
151	81, 150	pm2.61dan 812	. . 3 ⊢ ((𝜑 ∧ 𝐴 ≠ ∅) → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))
152	25, 151	sylan2 592	. 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 1087 = wceq 1537 ∈ wcel 2108 ≠ wne 2946 ∀wral 3067 ∃wrex 3076 {crab 3443 ⊆ wss 3976 ∅c0 4352 class class class wbr 5166 supcsup 9509 infcinf 9510 ℂcc 11182 ℝcr 11183 +∞cpnf 11321 -∞cmnf 11322 ℝ^*cxr 11323 < clt 11324 ≤ cle 11325 -cneg 11521 -_𝑒cxne 13172

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770 ax-cnex 11240 ax-resscn 11241 ax-1cn 11242 ax-icn 11243 ax-addcl 11244 ax-addrcl 11245 ax-mulcl 11246 ax-mulrcl 11247 ax-mulcom 11248 ax-addass 11249 ax-mulass 11250 ax-distr 11251 ax-i2m1 11252 ax-1ne0 11253 ax-1rid 11254 ax-rnegex 11255 ax-rrecex 11256 ax-cnre 11257 ax-pre-lttri 11258 ax-pre-lttrn 11259 ax-pre-ltadd 11260 ax-pre-mulgt0 11261 ax-pre-sup 11262

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-nel 3053 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-br 5167 df-opab 5229 df-mpt 5250 df-id 5593 df-po 5607 df-so 5608 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-isom 6582 df-riota 7404 df-ov 7451 df-oprab 7452 df-mpo 7453 df-er 8763 df-en 9004 df-dom 9005 df-sdom 9006 df-sup 9511 df-inf 9512 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11522 df-neg 11523 df-xneg 13175

This theorem is referenced by: supminfxr2 45384

W3C validator