ixxub

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

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

Proof

Step	Hyp	Ref	Expression
1		ixx.1	⊢ 𝑂 = ( 𝑥 ∈ ℝ^* , 𝑦 ∈ ℝ^* ↦ { 𝑧 ∈ ℝ^* ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑆 𝑦 ) } )
2		ixxub.2	⊢ ( ( 𝑤 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( 𝑤 < 𝐵 → 𝑤 𝑆 𝐵 ) )
3		ixxub.3	⊢ ( ( 𝑤 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( 𝑤 𝑆 𝐵 → 𝑤 ≤ 𝐵 ) )
4		ixxub.4	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^* ) → ( 𝐴 < 𝑤 → 𝐴 𝑅 𝑤 ) )
5		ixxub.5	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^* ) → ( 𝐴 𝑅 𝑤 → 𝐴 ≤ 𝑤 ) )
6	1	elixx1	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ↔ ( 𝑤 ∈ ℝ^* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑆 𝐵 ) ) )
7	6	3adant3	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → ( 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ↔ ( 𝑤 ∈ ℝ^* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑆 𝐵 ) ) )
8	7	biimpa	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → ( 𝑤 ∈ ℝ^* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑆 𝐵 ) )
9	8	simp1d	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → 𝑤 ∈ ℝ^* )
10	9	ex	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → ( 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) → 𝑤 ∈ ℝ^* ) )
11	10	ssrdv	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → ( 𝐴 𝑂 𝐵 ) ⊆ ℝ^* )
12		supxrcl	⊢ ( ( 𝐴 𝑂 𝐵 ) ⊆ ℝ^* → sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ∈ ℝ^* )
13	11 12	syl	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ∈ ℝ^* )
14		simp2	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → 𝐵 ∈ ℝ^* )
15	8	simp3d	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → 𝑤 𝑆 𝐵 )
16	14	adantr	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → 𝐵 ∈ ℝ^* )
17	9 16 3	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → ( 𝑤 𝑆 𝐵 → 𝑤 ≤ 𝐵 ) )
18	15 17	mpd	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → 𝑤 ≤ 𝐵 )
19	18	ralrimiva	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → ∀ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) 𝑤 ≤ 𝐵 )
20		supxrleub	⊢ ( ( ( 𝐴 𝑂 𝐵 ) ⊆ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ≤ 𝐵 ↔ ∀ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) 𝑤 ≤ 𝐵 ) )
21	11 14 20	syl2anc	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → ( sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ≤ 𝐵 ↔ ∀ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) 𝑤 ≤ 𝐵 ) )
22	19 21	mpbird	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ≤ 𝐵 )
23		simprl	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) < 𝑤 ∧ 𝑤 < 𝐵 ) ) → sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) < 𝑤 )
24	11	ad2antrr	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) < 𝑤 ∧ 𝑤 < 𝐵 ) ) → ( 𝐴 𝑂 𝐵 ) ⊆ ℝ^* )
25		qre	⊢ ( 𝑤 ∈ ℚ → 𝑤 ∈ ℝ )
26	25	rexrd	⊢ ( 𝑤 ∈ ℚ → 𝑤 ∈ ℝ^* )
27	26	ad2antlr	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) < 𝑤 ∧ 𝑤 < 𝐵 ) ) → 𝑤 ∈ ℝ^* )
28		simp1	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → 𝐴 ∈ ℝ^* )
29	28	ad2antrr	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) < 𝑤 ∧ 𝑤 < 𝐵 ) ) → 𝐴 ∈ ℝ^* )
30	13	ad2antrr	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) < 𝑤 ∧ 𝑤 < 𝐵 ) ) → sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ∈ ℝ^* )
31		simp3	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → ( 𝐴 𝑂 𝐵 ) ≠ ∅ )
32		n0	⊢ ( ( 𝐴 𝑂 𝐵 ) ≠ ∅ ↔ ∃ 𝑤 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) )
33	31 32	sylib	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → ∃ 𝑤 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) )
34	28	adantr	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → 𝐴 ∈ ℝ^* )
35	13	adantr	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ∈ ℝ^* )
36	8	simp2d	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → 𝐴 𝑅 𝑤 )
37	34 9 5	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → ( 𝐴 𝑅 𝑤 → 𝐴 ≤ 𝑤 ) )
38	36 37	mpd	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → 𝐴 ≤ 𝑤 )
39		supxrub	⊢ ( ( ( 𝐴 𝑂 𝐵 ) ⊆ ℝ^* ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → 𝑤 ≤ sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) )
40	11 39	sylan	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → 𝑤 ≤ sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) )
41	34 9 35 38 40	xrletrd	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → 𝐴 ≤ sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) )
42	33 41	exlimddv	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → 𝐴 ≤ sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) )
43	42	ad2antrr	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) < 𝑤 ∧ 𝑤 < 𝐵 ) ) → 𝐴 ≤ sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) )
44	29 30 27 43 23	xrlelttrd	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) < 𝑤 ∧ 𝑤 < 𝐵 ) ) → 𝐴 < 𝑤 )
45	29 27 4	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) < 𝑤 ∧ 𝑤 < 𝐵 ) ) → ( 𝐴 < 𝑤 → 𝐴 𝑅 𝑤 ) )
46	44 45	mpd	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) < 𝑤 ∧ 𝑤 < 𝐵 ) ) → 𝐴 𝑅 𝑤 )
47		simprr	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) < 𝑤 ∧ 𝑤 < 𝐵 ) ) → 𝑤 < 𝐵 )
48	14	ad2antrr	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) < 𝑤 ∧ 𝑤 < 𝐵 ) ) → 𝐵 ∈ ℝ^* )
49	27 48 2	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) < 𝑤 ∧ 𝑤 < 𝐵 ) ) → ( 𝑤 < 𝐵 → 𝑤 𝑆 𝐵 ) )
50	47 49	mpd	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) < 𝑤 ∧ 𝑤 < 𝐵 ) ) → 𝑤 𝑆 𝐵 )
51	7	ad2antrr	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) < 𝑤 ∧ 𝑤 < 𝐵 ) ) → ( 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ↔ ( 𝑤 ∈ ℝ^* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑆 𝐵 ) ) )
52	27 46 50 51	mpbir3and	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) < 𝑤 ∧ 𝑤 < 𝐵 ) ) → 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) )
53	24 52 39	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) < 𝑤 ∧ 𝑤 < 𝐵 ) ) → 𝑤 ≤ sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) )
54	27 30	xrlenltd	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) < 𝑤 ∧ 𝑤 < 𝐵 ) ) → ( 𝑤 ≤ sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ↔ ¬ sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) < 𝑤 ) )
55	53 54	mpbid	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) < 𝑤 ∧ 𝑤 < 𝐵 ) ) → ¬ sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) < 𝑤 )
56	23 55	pm2.65da	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) → ¬ ( sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) < 𝑤 ∧ 𝑤 < 𝐵 ) )
57	56	nrexdv	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → ¬ ∃ 𝑤 ∈ ℚ ( sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) < 𝑤 ∧ 𝑤 < 𝐵 ) )
58		qbtwnxr	⊢ ( ( sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) < 𝐵 ) → ∃ 𝑤 ∈ ℚ ( sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) < 𝑤 ∧ 𝑤 < 𝐵 ) )
59	58	3expia	⊢ ( ( sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) < 𝐵 → ∃ 𝑤 ∈ ℚ ( sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) < 𝑤 ∧ 𝑤 < 𝐵 ) ) )
60	13 14 59	syl2anc	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → ( sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) < 𝐵 → ∃ 𝑤 ∈ ℚ ( sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) < 𝑤 ∧ 𝑤 < 𝐵 ) ) )
61	57 60	mtod	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → ¬ sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) < 𝐵 )
62	14 13 61	xrnltled	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → 𝐵 ≤ sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) )
63	13 14 22 62	xrletrid	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → sup ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) = 𝐵 )

Metamath Proof Explorer

Theorem ixxub

Proof