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 13266

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 13254	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝑤 ∈ (𝐴𝑂𝐵) ↔ (𝑤 ∈ ℝ^ ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵)))
3	2	3adant3 1132	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) → (𝑤 ∈ (𝐴𝑂𝐵) ↔ (𝑤 ∈ ℝ^* ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵)))
4	3	biimpa 476	. . . . . 6 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → (𝑤 ∈ ℝ^* ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵))
5	4	simp1d 1142	. . . . 5 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝑤 ∈ ℝ^*)
6	5	ex 412	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) → (𝑤 ∈ (𝐴𝑂𝐵) → 𝑤 ∈ ℝ^*))
7	6	ssrdv 3935	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) → (𝐴𝑂𝐵) ⊆ ℝ^*)
8		supxrcl 13214	. . 3 ⊢ ((𝐴𝑂𝐵) ⊆ ℝ^* → sup((𝐴𝑂𝐵), ℝ^, < ) ∈ ℝ^)
9	7, 8	syl 17	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) → sup((𝐴𝑂𝐵), ℝ^, < ) ∈ ℝ^)
10		simp2 1137	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) → 𝐵 ∈ ℝ^*)
11	4	simp3d 1144	. . . . 5 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝑤𝑆𝐵)
12	10	adantr 480	. . . . . 6 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝐵 ∈ ℝ^*)
13		ixxub.3	. . . . . 6 ⊢ ((𝑤 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝑤𝑆𝐵 → 𝑤 ≤ 𝐵))
14	5, 12, 13	syl2anc 584	. . . . 5 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → (𝑤𝑆𝐵 → 𝑤 ≤ 𝐵))
15	11, 14	mpd 15	. . . 4 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝑤 ≤ 𝐵)
16	15	ralrimiva 3124	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) → ∀𝑤 ∈ (𝐴𝑂𝐵)𝑤 ≤ 𝐵)
17		supxrleub 13225	. . . 4 ⊢ (((𝐴𝑂𝐵) ⊆ ℝ^* ∧ 𝐵 ∈ ℝ^) → (sup((𝐴𝑂𝐵), ℝ^, < ) ≤ 𝐵 ↔ ∀𝑤 ∈ (𝐴𝑂𝐵)𝑤 ≤ 𝐵))
18	7, 10, 17	syl2anc 584	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) → (sup((𝐴𝑂𝐵), ℝ^*, < ) ≤ 𝐵 ↔ ∀𝑤 ∈ (𝐴𝑂𝐵)𝑤 ≤ 𝐵))
19	16, 18	mpbird 257	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) → sup((𝐴𝑂𝐵), ℝ^*, < ) ≤ 𝐵)
20		simprl 770	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → sup((𝐴𝑂𝐵), ℝ^, < ) < 𝑤)
21	7	ad2antrr 726	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → (𝐴𝑂𝐵) ⊆ ℝ^)
22		qre 12851	. . . . . . . . . . 11 ⊢ (𝑤 ∈ ℚ → 𝑤 ∈ ℝ)
23	22	rexrd 11162	. . . . . . . . . 10 ⊢ (𝑤 ∈ ℚ → 𝑤 ∈ ℝ^*)
24	23	ad2antlr 727	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → 𝑤 ∈ ℝ^)
25		simp1 1136	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) → 𝐴 ∈ ℝ^*)
26	25	ad2antrr 726	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → 𝐴 ∈ ℝ^)
27	9	ad2antrr 726	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → sup((𝐴𝑂𝐵), ℝ^, < ) ∈ ℝ^*)
28		simp3 1138	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) → (𝐴𝑂𝐵) ≠ ∅)
29		n0 4300	. . . . . . . . . . . . . 14 ⊢ ((𝐴𝑂𝐵) ≠ ∅ ↔ ∃𝑤 𝑤 ∈ (𝐴𝑂𝐵))
30	28, 29	sylib 218	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) → ∃𝑤 𝑤 ∈ (𝐴𝑂𝐵))
31	25	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝐴 ∈ ℝ^*)
32	9	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → sup((𝐴𝑂𝐵), ℝ^, < ) ∈ ℝ^)
33	4	simp2d 1143	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝐴𝑅𝑤)
34		ixxub.5	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) → (𝐴𝑅𝑤 → 𝐴 ≤ 𝑤))
35	31, 5, 34	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → (𝐴𝑅𝑤 → 𝐴 ≤ 𝑤))
36	33, 35	mpd 15	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝐴 ≤ 𝑤)
37		supxrub 13223	. . . . . . . . . . . . . . 15 ⊢ (((𝐴𝑂𝐵) ⊆ ℝ^* ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝑤 ≤ sup((𝐴𝑂𝐵), ℝ^*, < ))
38	7, 37	sylan 580	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝑤 ≤ sup((𝐴𝑂𝐵), ℝ^*, < ))
39	31, 5, 32, 36, 38	xrletrd 13061	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝐴 ≤ sup((𝐴𝑂𝐵), ℝ^*, < ))
40	30, 39	exlimddv 1936	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) → 𝐴 ≤ sup((𝐴𝑂𝐵), ℝ^*, < ))
41	40	ad2antrr 726	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → 𝐴 ≤ sup((𝐴𝑂𝐵), ℝ^, < ))
42	26, 27, 24, 41, 20	xrlelttrd 13059	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^*, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → 𝐴 < 𝑤)
43		ixxub.4	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) → (𝐴 < 𝑤 → 𝐴𝑅𝑤))
44	26, 24, 43	syl2anc 584	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^*, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → (𝐴 < 𝑤 → 𝐴𝑅𝑤))
45	42, 44	mpd 15	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^*, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → 𝐴𝑅𝑤)
46		simprr 772	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^*, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → 𝑤 < 𝐵)
47	10	ad2antrr 726	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → 𝐵 ∈ ℝ^)
48		ixxub.2	. . . . . . . . . . 11 ⊢ ((𝑤 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝑤 < 𝐵 → 𝑤𝑆𝐵))
49	24, 47, 48	syl2anc 584	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^*, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → (𝑤 < 𝐵 → 𝑤𝑆𝐵))
50	46, 49	mpd 15	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^*, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → 𝑤𝑆𝐵)
51	3	ad2antrr 726	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → (𝑤 ∈ (𝐴𝑂𝐵) ↔ (𝑤 ∈ ℝ^ ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵)))
52	24, 45, 50, 51	mpbir3and 1343	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^*, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → 𝑤 ∈ (𝐴𝑂𝐵))
53	21, 52, 37	syl2anc 584	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → 𝑤 ≤ sup((𝐴𝑂𝐵), ℝ^, < ))
54	24, 27	xrlenltd 11178	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → (𝑤 ≤ sup((𝐴𝑂𝐵), ℝ^, < ) ↔ ¬ sup((𝐴𝑂𝐵), ℝ^*, < ) < 𝑤))
55	53, 54	mpbid 232	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ^, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → ¬ sup((𝐴𝑂𝐵), ℝ^, < ) < 𝑤)
56	20, 55	pm2.65da 816	. . . . 5 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) → ¬ (sup((𝐴𝑂𝐵), ℝ^*, < ) < 𝑤 ∧ 𝑤 < 𝐵))
57	56	nrexdv 3127	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) → ¬ ∃𝑤 ∈ ℚ (sup((𝐴𝑂𝐵), ℝ^*, < ) < 𝑤 ∧ 𝑤 < 𝐵))
58		qbtwnxr 13099	. . . . . 6 ⊢ ((sup((𝐴𝑂𝐵), ℝ^, < ) ∈ ℝ^ ∧ 𝐵 ∈ ℝ^* ∧ sup((𝐴𝑂𝐵), ℝ^, < ) < 𝐵) → ∃𝑤 ∈ ℚ (sup((𝐴𝑂𝐵), ℝ^, < ) < 𝑤 ∧ 𝑤 < 𝐵))
59	58	3expia 1121	. . . . 5 ⊢ ((sup((𝐴𝑂𝐵), ℝ^, < ) ∈ ℝ^ ∧ 𝐵 ∈ ℝ^) → (sup((𝐴𝑂𝐵), ℝ^, < ) < 𝐵 → ∃𝑤 ∈ ℚ (sup((𝐴𝑂𝐵), ℝ^*, < ) < 𝑤 ∧ 𝑤 < 𝐵)))
60	9, 10, 59	syl2anc 584	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) → (sup((𝐴𝑂𝐵), ℝ^, < ) < 𝐵 → ∃𝑤 ∈ ℚ (sup((𝐴𝑂𝐵), ℝ^, < ) < 𝑤 ∧ 𝑤 < 𝐵)))
61	57, 60	mtod 198	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) → ¬ sup((𝐴𝑂𝐵), ℝ^*, < ) < 𝐵)
62	10, 9, 61	xrnltled 11181	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) → 𝐵 ≤ sup((𝐴𝑂𝐵), ℝ^*, < ))
63	9, 10, 19, 62	xrletrid 13054	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐴𝑂𝐵) ≠ ∅) → sup((𝐴𝑂𝐵), ℝ^*, < ) = 𝐵)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∃wex 1780 ∈ wcel 2111 ≠ wne 2928 ∀wral 3047 ∃wrex 3056 {crab 3395 ⊆ wss 3897 ∅c0 4280 class class class wbr 5089 (class class class)co 7346 ∈ cmpo 7348 supcsup 9324 ℝ^*cxr 11145 < clt 11146 ≤ cle 11147 ℚcq 12846

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7668 ax-cnex 11062 ax-resscn 11063 ax-1cn 11064 ax-icn 11065 ax-addcl 11066 ax-addrcl 11067 ax-mulcl 11068 ax-mulrcl 11069 ax-mulcom 11070 ax-addass 11071 ax-mulass 11072 ax-distr 11073 ax-i2m1 11074 ax-1ne0 11075 ax-1rid 11076 ax-rnegex 11077 ax-rrecex 11078 ax-cnre 11079 ax-pre-lttri 11080 ax-pre-lttrn 11081 ax-pre-ltadd 11082 ax-pre-mulgt0 11083 ax-pre-sup 11084

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4857 df-iun 4941 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-om 7797 df-1st 7921 df-2nd 7922 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-er 8622 df-en 8870 df-dom 8871 df-sdom 8872 df-sup 9326 df-inf 9327 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-le 11152 df-sub 11346 df-neg 11347 df-div 11775 df-nn 12126 df-n0 12382 df-z 12469 df-uz 12733 df-q 12847

This theorem is referenced by: ioopnfsup 13768 icopnfsup 13769 bndth 24884 ioorf 25501 ioorinv2 25503 ioossioobi 45627

W3C validator