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 46219

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 9415	. . . . 5 ⊢ (𝐴 = ∅ → sup(𝐴, ℝ^, < ) = sup(∅, ℝ^, < ))
2		xrsup0 13367	. . . . . 6 ⊢ sup(∅, ℝ^*, < ) = -∞
3	2	a1i 11	. . . . 5 ⊢ (𝐴 = ∅ → sup(∅, ℝ^*, < ) = -∞)
4	1, 3	eqtrd 2801	. . . 4 ⊢ (𝐴 = ∅ → sup(𝐴, ℝ^*, < ) = -∞)
5	4	adantl 487	. . 3 ⊢ ((𝜑 ∧ 𝐴 = ∅) → sup(𝐴, ℝ^*, < ) = -∞)
6		eleq2 2855	. . . . . . . . . 10 ⊢ (𝐴 = ∅ → (-𝑥 ∈ 𝐴 ↔ -𝑥 ∈ ∅))
7	6	rabbidv 3426	. . . . . . . . 9 ⊢ (𝐴 = ∅ → {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} = {𝑥 ∈ ℝ ∣ -𝑥 ∈ ∅})
8		noel 4294	. . . . . . . . . . . . 13 ⊢ ¬ -𝑥 ∈ ∅
9	8	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → ¬ -𝑥 ∈ ∅)
10	9	rgen 3084	. . . . . . . . . . 11 ⊢ ∀𝑥 ∈ ℝ ¬ -𝑥 ∈ ∅
11		rabeq0 4348	. . . . . . . . . . 11 ⊢ ({𝑥 ∈ ℝ ∣ -𝑥 ∈ ∅} = ∅ ↔ ∀𝑥 ∈ ℝ ¬ -𝑥 ∈ ∅)
12	10, 11	mpbir 234	. . . . . . . . . 10 ⊢ {𝑥 ∈ ℝ ∣ -𝑥 ∈ ∅} = ∅
13	12	a1i 11	. . . . . . . . 9 ⊢ (𝐴 = ∅ → {𝑥 ∈ ℝ ∣ -𝑥 ∈ ∅} = ∅)
14	7, 13	eqtrd 2801	. . . . . . . 8 ⊢ (𝐴 = ∅ → {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} = ∅)
15	14	infeq1d 9448	. . . . . . 7 ⊢ (𝐴 = ∅ → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ) = inf(∅, ℝ^, < ))
16		xrinf0 13383	. . . . . . . 8 ⊢ inf(∅, ℝ^*, < ) = +∞
17	16	a1i 11	. . . . . . 7 ⊢ (𝐴 = ∅ → inf(∅, ℝ^*, < ) = +∞)
18	15, 17	eqtrd 2801	. . . . . 6 ⊢ (𝐴 = ∅ → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = +∞)
19	18	xnegeqd 46192	. . . . 5 ⊢ (𝐴 = ∅ → -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -_𝑒+∞)
20		xnegpnf 13253	. . . . . 6 ⊢ -_𝑒+∞ = -∞
21	20	a1i 11	. . . . 5 ⊢ (𝐴 = ∅ → -_𝑒+∞ = -∞)
22	19, 21	eqtrd 2801	. . . 4 ⊢ (𝐴 = ∅ → -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -∞)
23	22	adantl 487	. . 3 ⊢ ((𝜑 ∧ 𝐴 = ∅) → -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -∞)
24	5, 23	eqtr4d 2804	. 2 ⊢ ((𝜑 ∧ 𝐴 = ∅) → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))
25		neqne 2969	. . 3 ⊢ (¬ 𝐴 = ∅ → 𝐴 ≠ ∅)
26		supminfxr.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
27	26	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → 𝐴 ⊆ ℝ)
28		simplr 781	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → 𝐴 ≠ ∅)
29		simpr 490	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦)
30		negn0 11661	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) → {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ≠ ∅)
31		ublbneg 12975	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑦 ≤ 𝑧)
32		ssrab2 4037	. . . . . . . . . . 11 ⊢ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ⊆ ℝ
33		infrenegsup 12216	. . . . . . . . . . 11 ⊢ (({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ⊆ ℝ ∧ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑦 ≤ 𝑧) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) = -sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}, ℝ, < ))
34	32, 33	mp3an1 1477	. . . . . . . . . 10 ⊢ (({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑦 ≤ 𝑧) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) = -sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}, ℝ, < ))
35	30, 31, 34	syl2an 608	. . . . . . . . 9 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) = -sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}, ℝ, < ))
36	35	3impa 1127	. . . . . . . 8 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) = -sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}, ℝ, < ))
37		elrabi 3649	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}} → 𝑦 ∈ ℝ)
38	37	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}) → 𝑦 ∈ ℝ)
39		ssel2 3935	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ)
40		negeq 11467	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑦 → -𝑤 = -𝑦)
41	40	eleq1d 2851	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑦 → (-𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ↔ -𝑦 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}))
42	41	elrab3 3654	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ → (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}} ↔ -𝑦 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}))
43		renegcl 11539	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℝ → -𝑦 ∈ ℝ)
44		negeq 11467	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = -𝑦 → -𝑥 = --𝑦)
45	44	eleq1d 2851	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = -𝑦 → (-𝑥 ∈ 𝐴 ↔ --𝑦 ∈ 𝐴))
46	45	elrab3 3654	. . . . . . . . . . . . . . 15 ⊢ (-𝑦 ∈ ℝ → (-𝑦 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ↔ --𝑦 ∈ 𝐴))
47	43, 46	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ → (-𝑦 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ↔ --𝑦 ∈ 𝐴))
48		recn 11208	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
49	48	negnegd 11578	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℝ → --𝑦 = 𝑦)
50	49	eleq1d 2851	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ → (--𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
51	42, 47, 50	3bitrd 308	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℝ → (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}} ↔ 𝑦 ∈ 𝐴))
52	51	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ) → (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}} ↔ 𝑦 ∈ 𝐴))
53	38, 39, 52	eqrdav 2765	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ ℝ → {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}} = 𝐴)
54	53	supeq1d 9416	. . . . . . . . . 10 ⊢ (𝐴 ⊆ ℝ → sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}, ℝ, < ) = sup(𝐴, ℝ, < ))
55	54	3ad2ant1 1151	. . . . . . . . 9 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}, ℝ, < ) = sup(𝐴, ℝ, < ))
56	55	negeqd 11469	. . . . . . . 8 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → -sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}}, ℝ, < ) = -sup(𝐴, ℝ, < ))
57	36, 56	eqtrd 2801	. . . . . . 7 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) = -sup(𝐴, ℝ, < ))
58		infrecl 12215	. . . . . . . . . . 11 ⊢ (({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ⊆ ℝ ∧ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑦 ≤ 𝑧) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℝ)
59	32, 58	mp3an1 1477	. . . . . . . . . 10 ⊢ (({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑦 ≤ 𝑧) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℝ)
60	30, 31, 59	syl2an 608	. . . . . . . . 9 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℝ)
61	60	3impa 1127	. . . . . . . 8 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℝ)
62		suprcl 12193	. . . . . . . 8 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ, < ) ∈ ℝ)
63		recn 11208	. . . . . . . . 9 ⊢ (inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℝ → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℂ)
64		recn 11208	. . . . . . . . 9 ⊢ (sup(𝐴, ℝ, < ) ∈ ℝ → sup(𝐴, ℝ, < ) ∈ ℂ)
65		negcon2 11529	. . . . . . . . 9 ⊢ ((inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℂ ∧ sup(𝐴, ℝ, < ) ∈ ℂ) → (inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) = -sup(𝐴, ℝ, < ) ↔ sup(𝐴, ℝ, < ) = -inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < )))
66	63, 64, 65	syl2an 608	. . . . . . . 8 ⊢ ((inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℝ ∧ sup(𝐴, ℝ, < ) ∈ ℝ) → (inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) = -sup(𝐴, ℝ, < ) ↔ sup(𝐴, ℝ, < ) = -inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < )))
67	61, 62, 66	syl2anc 596	. . . . . . 7 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → (inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) = -sup(𝐴, ℝ, < ) ↔ sup(𝐴, ℝ, < ) = -inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < )))
68	57, 67	mpbid 235	. . . . . 6 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ, < ) = -inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ))
69	27, 28, 29, 68	syl3anc 1398	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ, < ) = -inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ))
70		supxrre 13371	. . . . . 6 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ^*, < ) = sup(𝐴, ℝ, < ))
71	27, 28, 29, 70	syl3anc 1398	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ^*, < ) = sup(𝐴, ℝ, < ))
72	32	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ⊆ ℝ)
73	27, 28, 30	syl2anc 596	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ≠ ∅)
74	29, 31	syl 18	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑦 ≤ 𝑧)
75		infxrre 13381	. . . . . . . 8 ⊢ (({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ⊆ ℝ ∧ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑦 ≤ 𝑧) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ))
76	72, 73, 74, 75	syl3anc 1398	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ))
77	76	xnegeqd 46192	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ))
78	26, 60	sylanl1 693	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) ∈ ℝ)
79	78	rexnegd 45902	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ) = -inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ))
80	77, 79	eqtrd 2801	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ, < ))
81	69, 71, 80	3eqtr4d 2811	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))
82		simpr 490	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦)
83		simplr 781	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → 𝑦 ∈ ℝ)
84	26	sselda 3940	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℝ)
85	84	adantlr 728	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℝ)
86	83, 85	ltnled 11375	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → (𝑦 < 𝑧 ↔ ¬ 𝑧 ≤ 𝑦))
87	86	rexbidva 3190	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ∃𝑧 ∈ 𝐴 ¬ 𝑧 ≤ 𝑦))
88		rexnal 3120	. . . . . . . . . . . 12 ⊢ (∃𝑧 ∈ 𝐴 ¬ 𝑧 ≤ 𝑦 ↔ ¬ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦)
89	88	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∃𝑧 ∈ 𝐴 ¬ 𝑧 ≤ 𝑦 ↔ ¬ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦))
90	87, 89	bitrd 282	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ¬ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦))
91	90	ralbidva 3189	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ∀𝑦 ∈ ℝ ¬ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦))
92		ralnex 3094	. . . . . . . . . 10 ⊢ (∀𝑦 ∈ ℝ ¬ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ↔ ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦)
93	92	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑦 ∈ ℝ ¬ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ↔ ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦))
94	91, 93	bitrd 282	. . . . . . . 8 ⊢ (𝜑 → (∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦))
95	94	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → (∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦))
96	82, 95	mpbird 260	. . . . . 6 ⊢ ((𝜑 ∧ ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)
97		xnegmnf 13254	. . . . . . . . 9 ⊢ -_𝑒-∞ = +∞
98	97	eqcomi 2775	. . . . . . . 8 ⊢ +∞ = -_𝑒-∞
99	98	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → +∞ = -_𝑒-∞)
100		simpr 490	. . . . . . . 8 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)
101		ressxr 11271	. . . . . . . . . . . 12 ⊢ ℝ ⊆ ℝ^*
102	101	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → ℝ ⊆ ℝ^*)
103	26, 102	sstrd 3950	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ⊆ ℝ^*)
104		supxrunb2 13364	. . . . . . . . . 10 ⊢ (𝐴 ⊆ ℝ^* → (∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ sup(𝐴, ℝ^*, < ) = +∞))
105	103, 104	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ sup(𝐴, ℝ^*, < ) = +∞))
106	105	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → (∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ sup(𝐴, ℝ^*, < ) = +∞))
107	100, 106	mpbid 235	. . . . . . 7 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → sup(𝐴, ℝ^*, < ) = +∞)
108		renegcl 11539	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ ℝ → -𝑣 ∈ ℝ)
109	108	adantl 487	. . . . . . . . . . . . 13 ⊢ ((∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ∧ 𝑣 ∈ ℝ) → -𝑣 ∈ ℝ)
110		simpl 488	. . . . . . . . . . . . 13 ⊢ ((∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ∧ 𝑣 ∈ ℝ) → ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)
111		breq1 5117	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = -𝑣 → (𝑦 < 𝑧 ↔ -𝑣 < 𝑧))
112	111	rexbidv 3192	. . . . . . . . . . . . . 14 ⊢ (𝑦 = -𝑣 → (∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ∃𝑧 ∈ 𝐴 -𝑣 < 𝑧))
113	112	rspcva 3582	. . . . . . . . . . . . 13 ⊢ ((-𝑣 ∈ ℝ ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → ∃𝑧 ∈ 𝐴 -𝑣 < 𝑧)
114	109, 110, 113	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧 ∧ 𝑣 ∈ ℝ) → ∃𝑧 ∈ 𝐴 -𝑣 < 𝑧)
115	114	adantll 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) ∧ 𝑣 ∈ ℝ) → ∃𝑧 ∈ 𝐴 -𝑣 < 𝑧)
116		negeq 11467	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = -𝑧 → -𝑥 = --𝑧)
117	116	eleq1d 2851	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = -𝑧 → (-𝑥 ∈ 𝐴 ↔ --𝑧 ∈ 𝐴))
118	84	renegcld 11659	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → -𝑧 ∈ ℝ)
119	118	ad4ant13 764	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → -𝑧 ∈ ℝ)
120	84	recnd 11255	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℂ)
121	120	negnegd 11578	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → --𝑧 = 𝑧)
122		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴)
123	121, 122	eqeltrd 2866	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → --𝑧 ∈ 𝐴)
124	123	ad4ant13 764	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → --𝑧 ∈ 𝐴)
125	117, 119, 124	elrabd 3655	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → -𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴})
126		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → -𝑣 < 𝑧)
127	108	ad3antlr 744	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → -𝑣 ∈ ℝ)
128	84	ad4ant13 764	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → 𝑧 ∈ ℝ)
129	127, 128	ltnegd 11810	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → (-𝑣 < 𝑧 ↔ -𝑧 < --𝑣))
130	126, 129	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → -𝑧 < --𝑣)
131		simpllr 788	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → 𝑣 ∈ ℝ)
132		recn 11208	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ ℝ → 𝑣 ∈ ℂ)
133		negneg 11526	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ ℂ → --𝑣 = 𝑣)
134	131, 132, 133	3syl 19	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → --𝑣 = 𝑣)
135	130, 134	breqtrd 5142	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → -𝑧 < 𝑣)
136		breq1 5117	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = -𝑧 → (𝑤 < 𝑣 ↔ -𝑧 < 𝑣))
137	136	rspcev 3584	. . . . . . . . . . . . . 14 ⊢ ((-𝑧 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ∧ -𝑧 < 𝑣) → ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣)
138	125, 135, 137	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑣 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ -𝑣 < 𝑧) → ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣)
139	138	rexlimdva2 3171	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑣 ∈ ℝ) → (∃𝑧 ∈ 𝐴 -𝑣 < 𝑧 → ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣))
140	139	adantlr 728	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) ∧ 𝑣 ∈ ℝ) → (∃𝑧 ∈ 𝐴 -𝑣 < 𝑧 → ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣))
141	115, 140	mpd 16	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) ∧ 𝑣 ∈ ℝ) → ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣)
142	141	ralrimiva 3160	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → ∀𝑣 ∈ ℝ ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣)
143	32, 101	sstri 3949	. . . . . . . . . 10 ⊢ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ⊆ ℝ^*
144		infxrunb2 46124	. . . . . . . . . 10 ⊢ ({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} ⊆ ℝ^* → (∀𝑣 ∈ ℝ ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣 ↔ inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -∞))
145	143, 144	ax-mp 5	. . . . . . . . 9 ⊢ (∀𝑣 ∈ ℝ ∃𝑤 ∈ {𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}𝑤 < 𝑣 ↔ inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -∞)
146	142, 145	sylib 221	. . . . . . . 8 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -∞)
147	146	xnegeqd 46192	. . . . . . 7 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^*, < ) = -_𝑒-∞)
148	99, 107, 147	3eqtr4d 2811	. . . . . 6 ⊢ ((𝜑 ∧ ∀𝑦 ∈ ℝ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))
149	96, 148	syldan 603	. . . . 5 ⊢ ((𝜑 ∧ ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))
150	149	adantlr 728	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ≠ ∅) ∧ ¬ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝑦) → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))
151	81, 150	pm2.61dan 825	. . 3 ⊢ ((𝜑 ∧ 𝐴 ≠ ∅) → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))
152	25, 151	sylan2 605	. 2 ⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))
153	24, 152	pm2.61dan 825	1 ⊢ (𝜑 → sup(𝐴, ℝ^, < ) = -_𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ^, < ))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2146 ≠ wne 2961 ∀wral 3082 ∃wrex 3092 {crab 3419 ⊆ wss 3908 ∅c0 4289 class class class wbr 5114 supcsup 9410 infcinf 9411 ℂcc 11116 ℝcr 11117 +∞cpnf 11258 -∞cmnf 11259 ℝ^*cxr 11260 < clt 11261 ≤ cle 11262 -cneg 11460 -_𝑒cxne 13152

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-sep 5262 ax-nul 5274 ax-pow 5341 ax-pr 5409 ax-un 7745 ax-cnex 11174 ax-resscn 11175 ax-1cn 11176 ax-icn 11177 ax-addcl 11178 ax-addrcl 11179 ax-mulcl 11180 ax-mulrcl 11181 ax-mulcom 11182 ax-addass 11183 ax-mulass 11184 ax-distr 11185 ax-i2m1 11186 ax-1ne0 11187 ax-1rid 11188 ax-rnegex 11189 ax-rrecex 11190 ax-cnre 11191 ax-pre-lttri 11192 ax-pre-lttrn 11193 ax-pre-ltadd 11194 ax-pre-mulgt0 11195 ax-pre-sup 11196

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-nel 3068 df-ral 3083 df-rex 3093 df-rmo 3372 df-reu 3373 df-rab 3420 df-v 3460 df-sbc 3748 df-csb 3857 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4290 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4878 df-br 5115 df-opab 5179 df-mpt 5198 df-id 5561 df-po 5574 df-so 5575 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-iota 6499 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-isom 6552 df-riota 7380 df-ov 7426 df-oprab 7427 df-mpo 7428 df-er 8703 df-en 8953 df-dom 8954 df-sdom 8955 df-sup 9412 df-inf 9413 df-pnf 11263 df-mnf 11264 df-xr 11265 df-ltxr 11266 df-le 11267 df-sub 11461 df-neg 11462 df-xneg 13155

This theorem is used by: supminfxr2 46224

W3C validator