supxrun

Description: The supremum of the union of two sets of extended reals equals the largest of their suprema. (Contributed by NM, 19-Jan-2006)

		Ref	Expression
	Assertion	supxrun	$⊢ (A \subseteq ℝ^{} \land B \subseteq ℝ^{} \land sup (A ℝ^{} <) \leq sup (B ℝ^{} <)) \to sup (A \cup B ℝ^{} <) = sup (B ℝ^{} <)$

Proof

Step	Hyp	Ref	Expression
1		unss	$⊢ (A \subseteq ℝ^{} \land B \subseteq ℝ^{}) \leftrightarrow A \cup B \subseteq ℝ^{*}$
2	1	biimpi	$⊢ (A \subseteq ℝ^{} \land B \subseteq ℝ^{}) \to A \cup B \subseteq ℝ^{*}$
3	2	3adant3	$⊢ (A \subseteq ℝ^{} \land B \subseteq ℝ^{} \land sup (A ℝ^{} <) \leq sup (B ℝ^{} <)) \to A \cup B \subseteq ℝ^{*}$
4		supxrcl	$⊢ B \subseteq ℝ^{} \to sup (B ℝ^{} <) \in ℝ^{*}$
5	4	3ad2ant2	$⊢ (A \subseteq ℝ^{} \land B \subseteq ℝ^{} \land sup (A ℝ^{} <) \leq sup (B ℝ^{} <)) \to sup (B ℝ^{} <) \in ℝ^{}$
6		elun	$⊢ x \in (A \cup B) \leftrightarrow (x \in A \lor x \in B)$
7		xrltso	$⊢ < Or ℝ^{*}$
8	7	a1i	$⊢ A \subseteq ℝ^{} \to < Or ℝ^{}$
9		xrsupss	$⊢ A \subseteq ℝ^{} \to \exists y \in ℝ^{} (\forall z \in A \neg y < z \land \forall z \in ℝ^{*} (z < y \to \exists w \in A z < w))$
10	8 9	supub	$⊢ A \subseteq ℝ^{} \to (x \in A \to \neg sup (A ℝ^{} <) < x)$
11	10	3ad2ant1	$⊢ (A \subseteq ℝ^{} \land B \subseteq ℝ^{} \land sup (A ℝ^{} <) \leq sup (B ℝ^{} <)) \to (x \in A \to \neg sup (A ℝ^{*} <) < x)$
12		supxrcl	$⊢ A \subseteq ℝ^{} \to sup (A ℝ^{} <) \in ℝ^{*}$
13	12	ad2antrr	$⊢ ((A \subseteq ℝ^{} \land B \subseteq ℝ^{}) \land x \in A) \to sup (A ℝ^{} <) \in ℝ^{}$
14	4	ad2antlr	$⊢ ((A \subseteq ℝ^{} \land B \subseteq ℝ^{}) \land x \in A) \to sup (B ℝ^{} <) \in ℝ^{}$
15		ssel2	$⊢ (A \subseteq ℝ^{} \land x \in A) \to x \in ℝ^{}$
16	15	adantlr	$⊢ ((A \subseteq ℝ^{} \land B \subseteq ℝ^{}) \land x \in A) \to x \in ℝ^{*}$
17		xrlelttr	$⊢ (sup (A ℝ^{} <) \in ℝ^{} \land sup (B ℝ^{} <) \in ℝ^{} \land x \in ℝ^{}) \to ((sup (A ℝ^{} <) \leq sup (B ℝ^{} <) \land sup (B ℝ^{} <) < x) \to sup (A ℝ^{*} <) < x)$
18	13 14 16 17	syl3anc	$⊢ ((A \subseteq ℝ^{} \land B \subseteq ℝ^{}) \land x \in A) \to ((sup (A ℝ^{} <) \leq sup (B ℝ^{} <) \land sup (B ℝ^{} <) < x) \to sup (A ℝ^{} <) < x)$
19	18	expdimp	$⊢ (((A \subseteq ℝ^{} \land B \subseteq ℝ^{}) \land x \in A) \land sup (A ℝ^{} <) \leq sup (B ℝ^{} <)) \to (sup (B ℝ^{} <) < x \to sup (A ℝ^{} <) < x)$
20	19	con3d	$⊢ (((A \subseteq ℝ^{} \land B \subseteq ℝ^{}) \land x \in A) \land sup (A ℝ^{} <) \leq sup (B ℝ^{} <)) \to (\neg sup (A ℝ^{} <) < x \to \neg sup (B ℝ^{} <) < x)$
21	20	exp41	$⊢ A \subseteq ℝ^{} \to (B \subseteq ℝ^{} \to (x \in A \to (sup (A ℝ^{} <) \leq sup (B ℝ^{} <) \to (\neg sup (A ℝ^{} <) < x \to \neg sup (B ℝ^{} <) < x))))$
22	21	com34	$⊢ A \subseteq ℝ^{} \to (B \subseteq ℝ^{} \to (sup (A ℝ^{} <) \leq sup (B ℝ^{} <) \to (x \in A \to (\neg sup (A ℝ^{} <) < x \to \neg sup (B ℝ^{} <) < x))))$
23	22	3imp	$⊢ (A \subseteq ℝ^{} \land B \subseteq ℝ^{} \land sup (A ℝ^{} <) \leq sup (B ℝ^{} <)) \to (x \in A \to (\neg sup (A ℝ^{} <) < x \to \neg sup (B ℝ^{} <) < x))$
24	11 23	mpdd	$⊢ (A \subseteq ℝ^{} \land B \subseteq ℝ^{} \land sup (A ℝ^{} <) \leq sup (B ℝ^{} <)) \to (x \in A \to \neg sup (B ℝ^{*} <) < x)$
25	7	a1i	$⊢ B \subseteq ℝ^{} \to < Or ℝ^{}$
26		xrsupss	$⊢ B \subseteq ℝ^{} \to \exists y \in ℝ^{} (\forall z \in B \neg y < z \land \forall z \in ℝ^{*} (z < y \to \exists w \in B z < w))$
27	25 26	supub	$⊢ B \subseteq ℝ^{} \to (x \in B \to \neg sup (B ℝ^{} <) < x)$
28	27	3ad2ant2	$⊢ (A \subseteq ℝ^{} \land B \subseteq ℝ^{} \land sup (A ℝ^{} <) \leq sup (B ℝ^{} <)) \to (x \in B \to \neg sup (B ℝ^{*} <) < x)$
29	24 28	jaod	$⊢ (A \subseteq ℝ^{} \land B \subseteq ℝ^{} \land sup (A ℝ^{} <) \leq sup (B ℝ^{} <)) \to ((x \in A \lor x \in B) \to \neg sup (B ℝ^{*} <) < x)$
30	6 29	biimtrid	$⊢ (A \subseteq ℝ^{} \land B \subseteq ℝ^{} \land sup (A ℝ^{} <) \leq sup (B ℝ^{} <)) \to (x \in (A \cup B) \to \neg sup (B ℝ^{*} <) < x)$
31	30	ralrimiv	$⊢ (A \subseteq ℝ^{} \land B \subseteq ℝ^{} \land sup (A ℝ^{} <) \leq sup (B ℝ^{} <)) \to \forall x \in (A \cup B) \neg sup (B ℝ^{*} <) < x$
32		rexr	$⊢ x \in ℝ \to x \in ℝ^{*}$
33		xrsupss	$⊢ B \subseteq ℝ^{} \to \exists x \in ℝ^{} (\forall z \in B \neg x < z \land \forall z \in ℝ^{*} (z < x \to \exists y \in B z < y))$
34	25 33	suplub	$⊢ B \subseteq ℝ^{} \to ((x \in ℝ^{} \land x < sup (B ℝ^{*} <)) \to \exists y \in B x < y)$
35	32 34	sylani	$⊢ B \subseteq ℝ^{} \to ((x \in ℝ \land x < sup (B ℝ^{} <)) \to \exists y \in B x < y)$
36		elun2	$⊢ y \in B \to y \in (A \cup B)$
37	36	anim1i	$⊢ (y \in B \land x < y) \to (y \in (A \cup B) \land x < y)$
38	37	reximi2	$⊢ \exists y \in B x < y \to \exists y \in (A \cup B) x < y$
39	35 38	syl6	$⊢ B \subseteq ℝ^{} \to ((x \in ℝ \land x < sup (B ℝ^{} <)) \to \exists y \in (A \cup B) x < y)$
40	39	expd	$⊢ B \subseteq ℝ^{} \to (x \in ℝ \to (x < sup (B ℝ^{} <) \to \exists y \in (A \cup B) x < y))$
41	40	ralrimiv	$⊢ B \subseteq ℝ^{} \to \forall x \in ℝ (x < sup (B ℝ^{} <) \to \exists y \in (A \cup B) x < y)$
42	41	3ad2ant2	$⊢ (A \subseteq ℝ^{} \land B \subseteq ℝ^{} \land sup (A ℝ^{} <) \leq sup (B ℝ^{} <)) \to \forall x \in ℝ (x < sup (B ℝ^{*} <) \to \exists y \in (A \cup B) x < y)$
43		supxr	$⊢ ((A \cup B \subseteq ℝ^{} \land sup (B ℝ^{} <) \in ℝ^{}) \land (\forall x \in (A \cup B) \neg sup (B ℝ^{} <) < x \land \forall x \in ℝ (x < sup (B ℝ^{} <) \to \exists y \in (A \cup B) x < y))) \to sup (A \cup B ℝ^{} <) = sup (B ℝ^{*} <)$
44	3 5 31 42 43	syl22anc	$⊢ (A \subseteq ℝ^{} \land B \subseteq ℝ^{} \land sup (A ℝ^{} <) \leq sup (B ℝ^{} <)) \to sup (A \cup B ℝ^{} <) = sup (B ℝ^{} <)$

Metamath Proof Explorer

Theorem supxrun

Proof