ixxub - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ixxub		Structured version Visualization version GIF version

Theorem ixxub 13319

Description: Extract the upper bound of an interval. (Contributed by Mario Carneiro, 17-Jun-2014.)

**Hypotheses**
Ref	Expression
ixx.1	⊢ 𝑂 = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)})
ixxub.2	⊢ ((𝑤 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝑤 < 𝐵 → 𝑤𝑆𝐵))
ixxub.3	⊢ ((𝑤 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝑤𝑆𝐵 → 𝑤 ≤ 𝐵))
ixxub.4	⊢ ((𝐴 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) → (𝐴 < 𝑤 → 𝐴𝑅𝑤))
ixxub.5	⊢ ((𝐴 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) → (𝐴𝑅𝑤 → 𝐴 ≤ 𝑤))

**Assertion**
Ref	Expression
ixxub	⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) → sup((𝐴𝑂𝐵), ℝ^*, < ) = 𝐵)

Distinct variable groups: 𝑥,𝑤,𝑦,𝑧,𝐴 𝑤,𝑂 𝑤,𝐵,𝑥,𝑦,𝑧 𝑥,𝑅,𝑦,𝑧 𝑥,𝑆,𝑦,𝑧 Allowed substitution hints: 𝑅(𝑤) 𝑆(𝑤) 𝑂(𝑥,𝑦,𝑧)

**Proof of Theorem ixxub**
Step	Hyp	Ref	Expression
1		ixx.1	. . . . . . . . 9 ⊢ 𝑂 = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)})
2	1	elixx1 13307	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝑤 ∈ (𝐴𝑂𝐵) ↔ (𝑤 ∈ ℝ^ ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵)))
3	2	3adant3 1133	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) → (𝑤 ∈ (𝐴𝑂𝐵) ↔ (𝑤 ∈ ℝ^* ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵)))
4	3	biimpa 476	. . . . . 6 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → (𝑤 ∈ ℝ^* ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵))
5	4	simp1d 1143	. . . . 5 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝑤 ∈ ℝ^*)
6	5	ex 412	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) → (𝑤 ∈ (𝐴𝑂𝐵) → 𝑤 ∈ ℝ^*))
7	6	ssrdv 3927	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) → (𝐴𝑂𝐵) ⊆ ℝ^*)
8		supxrcl 13267	. . 3 ⊢ ((𝐴𝑂𝐵) ⊆ ℝ^* → sup((𝐴𝑂𝐵), ℝ^, < ) ∈ ℝ^)
9	7, 8	syl 17	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) → sup((𝐴𝑂𝐵), ℝ^, < ) ∈ ℝ^)
10		simp2 1138	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) → 𝐵 ∈ ℝ^*)
11	4	simp3d 1145	. . . . 5 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝑤𝑆𝐵)
12	10	adantr 480	. . . . . 6 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝐵 ∈ ℝ^*)
13		ixxub.3	. . . . . 6 ⊢ ((𝑤 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝑤𝑆𝐵 → 𝑤 ≤ 𝐵))
14	5, 12, 13	syl2anc 585	. . . . 5 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → (𝑤𝑆𝐵 → 𝑤 ≤ 𝐵))
15	11, 14	mpd 15	. . . 4 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝑤 ≤ 𝐵)
16	15	ralrimiva 3129	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) → ∀𝑤 ∈ (𝐴𝑂𝐵)𝑤 ≤ 𝐵)
17		supxrleub 13278	. . . 4 ⊢ (((𝐴𝑂𝐵) ⊆ ℝ^* ∧ 𝐵 ∈ ℝ^) → (sup((𝐴𝑂𝐵), ℝ^, < ) ≤ 𝐵 ↔ ∀𝑤 ∈ (𝐴𝑂𝐵)𝑤 ≤ 𝐵))
18	7, 10, 17	syl2anc 585	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) → (sup((𝐴𝑂𝐵), ℝ^*, < ) ≤ 𝐵 ↔ ∀𝑤 ∈ (𝐴𝑂𝐵)𝑤 ≤ 𝐵))
19	16, 18	mpbird 257	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) → sup((𝐴𝑂𝐵), ℝ^*, < ) ≤ 𝐵)
20		simprl 771	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → sup((𝐴𝑂𝐵), ℝ^, < ) < 𝑤)
21	7	ad2antrr 727	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → (𝐴𝑂𝐵) ⊆ ℝ^)
22		qre 12903	. . . . . . . . . . 11 ⊢ (𝑤 ∈ ℚ → 𝑤 ∈ ℝ)
23	22	rexrd 11195	. . . . . . . . . 10 ⊢ (𝑤 ∈ ℚ → 𝑤 ∈ ℝ^*)
24	23	ad2antlr 728	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → 𝑤 ∈ ℝ^)
25		simp1 1137	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) → 𝐴 ∈ ℝ^*)
26	25	ad2antrr 727	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → 𝐴 ∈ ℝ^)
27	9	ad2antrr 727	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → sup((𝐴𝑂𝐵), ℝ^, < ) ∈ ℝ^*)
28		simp3 1139	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) → (𝐴𝑂𝐵) ≠ ∅)
29		n0 4293	. . . . . . . . . . . . . 14 ⊢ ((𝐴𝑂𝐵) ≠ ∅ ↔ ∃𝑤 𝑤 ∈ (𝐴𝑂𝐵))
30	28, 29	sylib 218	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) → ∃𝑤 𝑤 ∈ (𝐴𝑂𝐵))
31	25	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝐴 ∈ ℝ^*)
32	9	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → sup((𝐴𝑂𝐵), ℝ^, < ) ∈ ℝ^)
33	4	simp2d 1144	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝐴𝑅𝑤)
34		ixxub.5	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) → (𝐴𝑅𝑤 → 𝐴 ≤ 𝑤))
35	31, 5, 34	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → (𝐴𝑅𝑤 → 𝐴 ≤ 𝑤))
36	33, 35	mpd 15	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝐴 ≤ 𝑤)
37		supxrub 13276	. . . . . . . . . . . . . . 15 ⊢ (((𝐴𝑂𝐵) ⊆ ℝ^* ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝑤 ≤ sup((𝐴𝑂𝐵), ℝ^*, < ))
38	7, 37	sylan 581	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝑤 ≤ sup((𝐴𝑂𝐵), ℝ^*, < ))
39	31, 5, 32, 36, 38	xrletrd 13113	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝐴 ≤ sup((𝐴𝑂𝐵), ℝ^*, < ))
40	30, 39	exlimddv 1937	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) → 𝐴 ≤ sup((𝐴𝑂𝐵), ℝ^*, < ))
41	40	ad2antrr 727	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → 𝐴 ≤ sup((𝐴𝑂𝐵), ℝ^, < ))
42	26, 27, 24, 41, 20	xrlelttrd 13111	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^*, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → 𝐴 < 𝑤)
43		ixxub.4	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) → (𝐴 < 𝑤 → 𝐴𝑅𝑤))
44	26, 24, 43	syl2anc 585	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^*, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → (𝐴 < 𝑤 → 𝐴𝑅𝑤))
45	42, 44	mpd 15	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^*, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → 𝐴𝑅𝑤)
46		simprr 773	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^*, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → 𝑤 < 𝐵)
47	10	ad2antrr 727	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → 𝐵 ∈ ℝ^)
48		ixxub.2	. . . . . . . . . . 11 ⊢ ((𝑤 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝑤 < 𝐵 → 𝑤𝑆𝐵))
49	24, 47, 48	syl2anc 585	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^*, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → (𝑤 < 𝐵 → 𝑤𝑆𝐵))
50	46, 49	mpd 15	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^*, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → 𝑤𝑆𝐵)
51	3	ad2antrr 727	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → (𝑤 ∈ (𝐴𝑂𝐵) ↔ (𝑤 ∈ ℝ^ ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵)))
52	24, 45, 50, 51	mpbir3and 1344	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^*, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → 𝑤 ∈ (𝐴𝑂𝐵))
53	21, 52, 37	syl2anc 585	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → 𝑤 ≤ sup((𝐴𝑂𝐵), ℝ^, < ))
54	24, 27	xrlenltd 11211	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → (𝑤 ≤ sup((𝐴𝑂𝐵), ℝ^, < ) ↔ ¬ sup((𝐴𝑂𝐵), ℝ^*, < ) < 𝑤))
55	53, 54	mpbid 232	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → ¬ sup((𝐴𝑂𝐵), ℝ^, < ) < 𝑤)
56	20, 55	pm2.65da 817	. . . . 5 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) → ¬ (sup((𝐴𝑂𝐵), ℝ^*, < ) < 𝑤 ∧ 𝑤 < 𝐵))
57	56	nrexdv 3132	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) → ¬ ∃𝑤 ∈ ℚ (sup((𝐴𝑂𝐵), ℝ^*, < ) < 𝑤 ∧ 𝑤 < 𝐵))
58		qbtwnxr 13152	. . . . . 6 ⊢ ((sup((𝐴𝑂𝐵), ℝ^, < ) ∈ ℝ^ ∧ 𝐵 ∈ ℝ^* ∧ sup((𝐴𝑂𝐵), ℝ^, < ) < 𝐵) → ∃𝑤 ∈ ℚ (sup((𝐴𝑂𝐵), ℝ^, < ) < 𝑤 ∧ 𝑤 < 𝐵))
59	58	3expia 1122	. . . . 5 ⊢ ((sup((𝐴𝑂𝐵), ℝ^, < ) ∈ ℝ^ ∧ 𝐵 ∈ ℝ^) → (sup((𝐴𝑂𝐵), ℝ^, < ) < 𝐵 → ∃𝑤 ∈ ℚ (sup((𝐴𝑂𝐵), ℝ^*, < ) < 𝑤 ∧ 𝑤 < 𝐵)))
60	9, 10, 59	syl2anc 585	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) → (sup((𝐴𝑂𝐵), ℝ^, < ) < 𝐵 → ∃𝑤 ∈ ℚ (sup((𝐴𝑂𝐵), ℝ^, < ) < 𝑤 ∧ 𝑤 < 𝐵)))
61	57, 60	mtod 198	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) → ¬ sup((𝐴𝑂𝐵), ℝ^*, < ) < 𝐵)
62	10, 9, 61	xrnltled 11214	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) → 𝐵 ≤ sup((𝐴𝑂𝐵), ℝ^*, < ))
63	9, 10, 19, 62	xrletrid 13106	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) → sup((𝐴𝑂𝐵), ℝ^*, < ) = 𝐵)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∃wex 1781 ∈ wcel 2114 ≠ wne 2932 ∀wral 3051 ∃wrex 3061 {crab 3389 ⊆ wss 3889 ∅c0 4273 class class class wbr 5085 (class class class)co 7367 ∈ cmpo 7369 supcsup 9353 ℝ^*cxr 11178 < clt 11179 ≤ cle 11180 ℚcq 12898

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2708 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-pre-sup 11116

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3062 df-rmo 3342 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3909 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4851 df-iun 4935 df-br 5086 df-opab 5148 df-mpt 5167 df-tr 5193 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6265 df-ord 6326 df-on 6327 df-lim 6328 df-suc 6329 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-om 7818 df-1st 7942 df-2nd 7943 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-er 8643 df-en 8894 df-dom 8895 df-sdom 8896 df-sup 9355 df-inf 9356 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-sub 11379 df-neg 11380 df-div 11808 df-nn 12175 df-n0 12438 df-z 12525 df-uz 12789 df-q 12899

This theorem is referenced by: ioopnfsup 13823 icopnfsup 13824 bndth 24925 ioorf 25540 ioorinv2 25542 ioossioobi 45947

W3C validator