xrofsup

Description: The supremum is preserved by extended addition set operation. (Provided minus infinity is not involved as it does not behave well with addition.) (Contributed by Thierry Arnoux, 20-Mar-2017)

	Ref	Expression
Hypotheses	xrofsup.1	$⊢ φ \to X \subseteq ℝ^{*}$
	xrofsup.2	$⊢ φ \to Y \subseteq ℝ^{*}$
	xrofsup.3	$⊢ φ \to sup (X ℝ^{*} <) \neq −∞$
	xrofsup.4	$⊢ φ \to sup (Y ℝ^{*} <) \neq −∞$
	xrofsup.5	$⊢ φ \to Z = +_{𝑒} [X \times Y]$
Assertion	xrofsup	$⊢ φ \to sup (Z ℝ^{} <) = sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{*} <)$

Proof

Step	Hyp	Ref	Expression
1		xrofsup.1	$⊢ φ \to X \subseteq ℝ^{*}$
2		xrofsup.2	$⊢ φ \to Y \subseteq ℝ^{*}$
3		xrofsup.3	$⊢ φ \to sup (X ℝ^{*} <) \neq −∞$
4		xrofsup.4	$⊢ φ \to sup (Y ℝ^{*} <) \neq −∞$
5		xrofsup.5	$⊢ φ \to Z = +_{𝑒} [X \times Y]$
6	1	sseld	$⊢ φ \to (x \in X \to x \in ℝ^{*})$
7	2	sseld	$⊢ φ \to (y \in Y \to y \in ℝ^{*})$
8	6 7	anim12d	$⊢ φ \to ((x \in X \land y \in Y) \to (x \in ℝ^{} \land y \in ℝ^{}))$
9	8	imp	$⊢ (φ \land (x \in X \land y \in Y)) \to (x \in ℝ^{} \land y \in ℝ^{})$
10		xaddcl	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to x +_{𝑒} y \in ℝ^{*}$
11	9 10	syl	$⊢ (φ \land (x \in X \land y \in Y)) \to x +_{𝑒} y \in ℝ^{*}$
12	11	ralrimivva	$⊢ φ \to \forall x \in X \forall y \in Y x +_{𝑒} y \in ℝ^{*}$
13		fveq2	$⊢ u = ⟨x, y⟩ \to +_{𝑒} (u) = +_{𝑒} (⟨x, y⟩)$
14		df-ov	$⊢ x +_{𝑒} y = +_{𝑒} (⟨x, y⟩)$
15	13 14	eqtr4di	$⊢ u = ⟨x, y⟩ \to +_{𝑒} (u) = x +_{𝑒} y$
16	15	eleq1d	$⊢ u = ⟨x, y⟩ \to (+_{𝑒} (u) \in ℝ^{} \leftrightarrow x +_{𝑒} y \in ℝ^{})$
17	16	ralxp	$⊢ \forall u \in (X \times Y) +_{𝑒} (u) \in ℝ^{} \leftrightarrow \forall x \in X \forall y \in Y x +_{𝑒} y \in ℝ^{}$
18	12 17	sylibr	$⊢ φ \to \forall u \in (X \times Y) +_{𝑒} (u) \in ℝ^{*}$
19		xaddf	$⊢ +_{𝑒} : ℝ^{} \times ℝ^{} ⟶ ℝ^{*}$
20		ffun	$⊢ +_{𝑒} : ℝ^{} \times ℝ^{} ⟶ ℝ^{*} \to Fun +_{𝑒}$
21	19 20	ax-mp	$⊢ Fun +_{𝑒}$
22		xpss12	$⊢ (X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \to X \times Y \subseteq ℝ^{} \times ℝ^{}$
23	1 2 22	syl2anc	$⊢ φ \to X \times Y \subseteq ℝ^{} \times ℝ^{}$
24	19	fdmi	$⊢ dom +_{𝑒} = ℝ^{} \times ℝ^{}$
25	23 24	sseqtrrdi	$⊢ φ \to X \times Y \subseteq dom +_{𝑒}$
26		funimass4	$⊢ (Fun +_{𝑒} \land X \times Y \subseteq dom +_{𝑒}) \to (+_{𝑒} [X \times Y] \subseteq ℝ^{} \leftrightarrow \forall u \in (X \times Y) +_{𝑒} (u) \in ℝ^{})$
27	21 25 26	sylancr	$⊢ φ \to (+_{𝑒} [X \times Y] \subseteq ℝ^{} \leftrightarrow \forall u \in (X \times Y) +_{𝑒} (u) \in ℝ^{})$
28	18 27	mpbird	$⊢ φ \to +_{𝑒} [X \times Y] \subseteq ℝ^{*}$
29	5 28	eqsstrd	$⊢ φ \to Z \subseteq ℝ^{*}$
30		supxrcl	$⊢ X \subseteq ℝ^{} \to sup (X ℝ^{} <) \in ℝ^{*}$
31	1 30	syl	$⊢ φ \to sup (X ℝ^{} <) \in ℝ^{}$
32		supxrcl	$⊢ Y \subseteq ℝ^{} \to sup (Y ℝ^{} <) \in ℝ^{*}$
33	2 32	syl	$⊢ φ \to sup (Y ℝ^{} <) \in ℝ^{}$
34	31 33	xaddcld	$⊢ φ \to sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <) \in ℝ^{*}$
35	5	eleq2d	$⊢ φ \to (z \in Z \leftrightarrow z \in +_{𝑒} [X \times Y])$
36	35	pm5.32i	$⊢ (φ \land z \in Z) \leftrightarrow (φ \land z \in +_{𝑒} [X \times Y])$
37		nfvd	$⊢ (φ \land z \in +_{𝑒} [X \times Y]) \to Ⅎ x z \leq sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <)$
38		nfvd	$⊢ (φ \land z \in +_{𝑒} [X \times Y]) \to Ⅎ y z \leq sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <)$
39	1	ad2antrr	$⊢ ((φ \land z \in +_{𝑒} [X \times Y]) \land (x \in X \land y \in Y)) \to X \subseteq ℝ^{*}$
40		simprl	$⊢ ((φ \land z \in +_{𝑒} [X \times Y]) \land (x \in X \land y \in Y)) \to x \in X$
41		supxrub	$⊢ (X \subseteq ℝ^{} \land x \in X) \to x \leq sup (X ℝ^{} <)$
42	39 40 41	syl2anc	$⊢ ((φ \land z \in +_{𝑒} [X \times Y]) \land (x \in X \land y \in Y)) \to x \leq sup (X ℝ^{*} <)$
43	2	ad2antrr	$⊢ ((φ \land z \in +_{𝑒} [X \times Y]) \land (x \in X \land y \in Y)) \to Y \subseteq ℝ^{*}$
44		simprr	$⊢ ((φ \land z \in +_{𝑒} [X \times Y]) \land (x \in X \land y \in Y)) \to y \in Y$
45		supxrub	$⊢ (Y \subseteq ℝ^{} \land y \in Y) \to y \leq sup (Y ℝ^{} <)$
46	43 44 45	syl2anc	$⊢ ((φ \land z \in +_{𝑒} [X \times Y]) \land (x \in X \land y \in Y)) \to y \leq sup (Y ℝ^{*} <)$
47	39 40	sseldd	$⊢ ((φ \land z \in +_{𝑒} [X \times Y]) \land (x \in X \land y \in Y)) \to x \in ℝ^{*}$
48	43 44	sseldd	$⊢ ((φ \land z \in +_{𝑒} [X \times Y]) \land (x \in X \land y \in Y)) \to y \in ℝ^{*}$
49	39 30	syl	$⊢ ((φ \land z \in +_{𝑒} [X \times Y]) \land (x \in X \land y \in Y)) \to sup (X ℝ^{} <) \in ℝ^{}$
50	43 32	syl	$⊢ ((φ \land z \in +_{𝑒} [X \times Y]) \land (x \in X \land y \in Y)) \to sup (Y ℝ^{} <) \in ℝ^{}$
51		xle2add	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land (sup (X ℝ^{} <) \in ℝ^{} \land sup (Y ℝ^{} <) \in ℝ^{})) \to ((x \leq sup (X ℝ^{} <) \land y \leq sup (Y ℝ^{} <)) \to x +_{𝑒} y \leq sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <))$
52	47 48 49 50 51	syl22anc	$⊢ ((φ \land z \in +_{𝑒} [X \times Y]) \land (x \in X \land y \in Y)) \to ((x \leq sup (X ℝ^{} <) \land y \leq sup (Y ℝ^{} <)) \to x +_{𝑒} y \leq sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <))$
53	42 46 52	mp2and	$⊢ ((φ \land z \in +_{𝑒} [X \times Y]) \land (x \in X \land y \in Y)) \to x +_{𝑒} y \leq sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <)$
54	53	ralrimivva	$⊢ (φ \land z \in +_{𝑒} [X \times Y]) \to \forall x \in X \forall y \in Y x +_{𝑒} y \leq sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <)$
55		fvelima	$⊢ (Fun +_{𝑒} \land z \in +_{𝑒} [X \times Y]) \to \exists u \in (X \times Y) +_{𝑒} (u) = z$
56	21 55	mpan	$⊢ z \in +_{𝑒} [X \times Y] \to \exists u \in (X \times Y) +_{𝑒} (u) = z$
57	56	adantl	$⊢ (φ \land z \in +_{𝑒} [X \times Y]) \to \exists u \in (X \times Y) +_{𝑒} (u) = z$
58	15	eqeq1d	$⊢ u = ⟨x, y⟩ \to (+_{𝑒} (u) = z \leftrightarrow x +_{𝑒} y = z)$
59	58	rexxp	$⊢ \exists u \in (X \times Y) +_{𝑒} (u) = z \leftrightarrow \exists x \in X \exists y \in Y x +_{𝑒} y = z$
60	57 59	sylib	$⊢ (φ \land z \in +_{𝑒} [X \times Y]) \to \exists x \in X \exists y \in Y x +_{𝑒} y = z$
61	54 60	r19.29d2r	$⊢ (φ \land z \in +_{𝑒} [X \times Y]) \to \exists x \in X \exists y \in Y (x +_{𝑒} y \leq sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <) \land x +_{𝑒} y = z)$
62		ancom	$⊢ (x +_{𝑒} y \leq sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <) \land x +_{𝑒} y = z) \leftrightarrow (x +_{𝑒} y = z \land x +_{𝑒} y \leq sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <))$
63	62	2rexbii	$⊢ \exists x \in X \exists y \in Y (x +_{𝑒} y \leq sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <) \land x +_{𝑒} y = z) \leftrightarrow \exists x \in X \exists y \in Y (x +_{𝑒} y = z \land x +_{𝑒} y \leq sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <))$
64	61 63	sylib	$⊢ (φ \land z \in +_{𝑒} [X \times Y]) \to \exists x \in X \exists y \in Y (x +_{𝑒} y = z \land x +_{𝑒} y \leq sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <))$
65		breq1	$⊢ x +_{𝑒} y = z \to (x +_{𝑒} y \leq sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <) \leftrightarrow z \leq sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <))$
66	65	biimpa	$⊢ (x +_{𝑒} y = z \land x +_{𝑒} y \leq sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <)) \to z \leq sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <)$
67	66	reximi	$⊢ \exists y \in Y (x +_{𝑒} y = z \land x +_{𝑒} y \leq sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <)) \to \exists y \in Y z \leq sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <)$
68	67	reximi	$⊢ \exists x \in X \exists y \in Y (x +_{𝑒} y = z \land x +_{𝑒} y \leq sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <)) \to \exists x \in X \exists y \in Y z \leq sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <)$
69	64 68	syl	$⊢ (φ \land z \in +_{𝑒} [X \times Y]) \to \exists x \in X \exists y \in Y z \leq sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <)$
70	37 38 69	19.9d2r	$⊢ (φ \land z \in +_{𝑒} [X \times Y]) \to z \leq sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <)$
71	36 70	sylbi	$⊢ (φ \land z \in Z) \to z \leq sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <)$
72	71	ralrimiva	$⊢ φ \to \forall z \in Z z \leq sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <)$
73	1	ad2antrr	$⊢ ((φ \land z \in ℝ) \land z < sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <)) \to X \subseteq ℝ^{*}$
74	2	ad2antrr	$⊢ ((φ \land z \in ℝ) \land z < sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <)) \to Y \subseteq ℝ^{*}$
75		simplr	$⊢ ((φ \land z \in ℝ) \land z < sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <)) \to z \in ℝ$
76	31	ad2antrr	$⊢ ((φ \land z \in ℝ) \land z < sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <)) \to sup (X ℝ^{} <) \in ℝ^{}$
77	33	ad2antrr	$⊢ ((φ \land z \in ℝ) \land z < sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <)) \to sup (Y ℝ^{} <) \in ℝ^{}$
78	3	ad2antrr	$⊢ ((φ \land z \in ℝ) \land z < sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <)) \to sup (X ℝ^{*} <) \neq −∞$
79	4	ad2antrr	$⊢ ((φ \land z \in ℝ) \land z < sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <)) \to sup (Y ℝ^{*} <) \neq −∞$
80		simpr	$⊢ ((φ \land z \in ℝ) \land z < sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <)) \to z < sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <)$
81	75 76 77 78 79 80	xlt2addrd	$⊢ ((φ \land z \in ℝ) \land z < sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <)) \to \exists a \in ℝ^{} \exists b \in ℝ^{} (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <))$
82		nfv	$⊢ Ⅎ b (X \subseteq ℝ^{} \land Y \subseteq ℝ^{})$
83		nfcv	$⊢ \underline{Ⅎ} b ℝ^{*}$
84		nfre1	$⊢ Ⅎ b \exists b \in ℝ^{} (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{*} <))$
85	83 84	nfrexw	$⊢ Ⅎ b \exists a \in ℝ^{} \exists b \in ℝ^{} (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <))$
86	82 85	nfan	$⊢ Ⅎ b ((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land \exists a \in ℝ^{} \exists b \in ℝ^{} (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <)))$
87		nfvd	$⊢ ((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land \exists a \in ℝ^{} \exists b \in ℝ^{} (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <))) \to Ⅎ a \exists v \in X \exists w \in Y z < v +_{𝑒} w$
88		nfvd	$⊢ ((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land \exists a \in ℝ^{} \exists b \in ℝ^{} (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <))) \to Ⅎ b \exists v \in X \exists w \in Y z < v +_{𝑒} w$
89		id	$⊢ (X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \to (X \subseteq ℝ^{} \land Y \subseteq ℝ^{})$
90	89	ralrimivw	$⊢ (X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \to \forall b \in ℝ^{} (X \subseteq ℝ^{} \land Y \subseteq ℝ^{*})$
91	90	ralrimivw	$⊢ (X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \to \forall a \in ℝ^{} \forall b \in ℝ^{} (X \subseteq ℝ^{} \land Y \subseteq ℝ^{})$
92	91	adantr	$⊢ ((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land \exists a \in ℝ^{} \exists b \in ℝ^{} (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <))) \to \forall a \in ℝ^{} \forall b \in ℝ^{} (X \subseteq ℝ^{} \land Y \subseteq ℝ^{})$
93		simpr	$⊢ ((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land \exists a \in ℝ^{} \exists b \in ℝ^{} (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <))) \to \exists a \in ℝ^{} \exists b \in ℝ^{} (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <))$
94	92 93	r19.29d2r	$⊢ ((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land \exists a \in ℝ^{} \exists b \in ℝ^{} (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <))) \to \exists a \in ℝ^{} \exists b \in ℝ^{} ((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <)))$
95		simplrr	$⊢ (((a \in ℝ^{} \land b \in ℝ^{}) \land ((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <)))) \land (v \in X \land w \in Y \land (a < v \land b < w))) \to (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <))$
96	95	3anassrs	$⊢ (((((a \in ℝ^{} \land b \in ℝ^{}) \land ((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <)))) \land v \in X) \land w \in Y) \land (a < v \land b < w)) \to (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <))$
97	96	simp1d	$⊢ (((((a \in ℝ^{} \land b \in ℝ^{}) \land ((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <)))) \land v \in X) \land w \in Y) \land (a < v \land b < w)) \to z = a +_{𝑒} b$
98		simp-4l	$⊢ (((((a \in ℝ^{} \land b \in ℝ^{}) \land ((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <)))) \land v \in X) \land w \in Y) \land (a < v \land b < w)) \to (a \in ℝ^{} \land b \in ℝ^{})$
99		simplrl	$⊢ (((a \in ℝ^{} \land b \in ℝ^{}) \land ((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <)))) \land (v \in X \land w \in Y \land (a < v \land b < w))) \to (X \subseteq ℝ^{} \land Y \subseteq ℝ^{})$
100	99	3anassrs	$⊢ (((((a \in ℝ^{} \land b \in ℝ^{}) \land ((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <)))) \land v \in X) \land w \in Y) \land (a < v \land b < w)) \to (X \subseteq ℝ^{} \land Y \subseteq ℝ^{})$
101	100	simpld	$⊢ (((((a \in ℝ^{} \land b \in ℝ^{}) \land ((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <)))) \land v \in X) \land w \in Y) \land (a < v \land b < w)) \to X \subseteq ℝ^{*}$
102		simpllr	$⊢ (((((a \in ℝ^{} \land b \in ℝ^{}) \land ((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <)))) \land v \in X) \land w \in Y) \land (a < v \land b < w)) \to v \in X$
103	101 102	sseldd	$⊢ (((((a \in ℝ^{} \land b \in ℝ^{}) \land ((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <)))) \land v \in X) \land w \in Y) \land (a < v \land b < w)) \to v \in ℝ^{*}$
104	100	simprd	$⊢ (((((a \in ℝ^{} \land b \in ℝ^{}) \land ((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <)))) \land v \in X) \land w \in Y) \land (a < v \land b < w)) \to Y \subseteq ℝ^{*}$
105		simplr	$⊢ (((((a \in ℝ^{} \land b \in ℝ^{}) \land ((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <)))) \land v \in X) \land w \in Y) \land (a < v \land b < w)) \to w \in Y$
106	104 105	sseldd	$⊢ (((((a \in ℝ^{} \land b \in ℝ^{}) \land ((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <)))) \land v \in X) \land w \in Y) \land (a < v \land b < w)) \to w \in ℝ^{*}$
107	98 103 106	jca32	$⊢ (((((a \in ℝ^{} \land b \in ℝ^{}) \land ((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <)))) \land v \in X) \land w \in Y) \land (a < v \land b < w)) \to ((a \in ℝ^{} \land b \in ℝ^{}) \land (v \in ℝ^{} \land w \in ℝ^{}))$
108		simpr	$⊢ (((((a \in ℝ^{} \land b \in ℝ^{}) \land ((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <)))) \land v \in X) \land w \in Y) \land (a < v \land b < w)) \to (a < v \land b < w)$
109		xlt2add	$⊢ ((a \in ℝ^{} \land b \in ℝ^{}) \land (v \in ℝ^{} \land w \in ℝ^{})) \to ((a < v \land b < w) \to a +_{𝑒} b < v +_{𝑒} w)$
110	109	imp	$⊢ (((a \in ℝ^{} \land b \in ℝ^{}) \land (v \in ℝ^{} \land w \in ℝ^{})) \land (a < v \land b < w)) \to a +_{𝑒} b < v +_{𝑒} w$
111		breq1	$⊢ z = a +_{𝑒} b \to (z < v +_{𝑒} w \leftrightarrow a +_{𝑒} b < v +_{𝑒} w)$
112	111	biimpar	$⊢ (z = a +_{𝑒} b \land a +_{𝑒} b < v +_{𝑒} w) \to z < v +_{𝑒} w$
113	110 112	sylan2	$⊢ (z = a +_{𝑒} b \land (((a \in ℝ^{} \land b \in ℝ^{}) \land (v \in ℝ^{} \land w \in ℝ^{})) \land (a < v \land b < w))) \to z < v +_{𝑒} w$
114	97 107 108 113	syl12anc	$⊢ (((((a \in ℝ^{} \land b \in ℝ^{}) \land ((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <)))) \land v \in X) \land w \in Y) \land (a < v \land b < w)) \to z < v +_{𝑒} w$
115		simplll	$⊢ (((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <))) \land (a \in ℝ^{} \land b \in ℝ^{})) \to X \subseteq ℝ^{*}$
116		simprl	$⊢ (((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <))) \land (a \in ℝ^{} \land b \in ℝ^{})) \to a \in ℝ^{*}$
117		simplr2	$⊢ (((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <))) \land (a \in ℝ^{} \land b \in ℝ^{})) \to a < sup (X ℝ^{*} <)$
118		supxrlub	$⊢ (X \subseteq ℝ^{} \land a \in ℝ^{}) \to (a < sup (X ℝ^{*} <) \leftrightarrow \exists v \in X a < v)$
119	118	biimpa	$⊢ ((X \subseteq ℝ^{} \land a \in ℝ^{}) \land a < sup (X ℝ^{*} <)) \to \exists v \in X a < v$
120	115 116 117 119	syl21anc	$⊢ (((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <))) \land (a \in ℝ^{} \land b \in ℝ^{})) \to \exists v \in X a < v$
121		simpllr	$⊢ (((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <))) \land (a \in ℝ^{} \land b \in ℝ^{})) \to Y \subseteq ℝ^{*}$
122		simprr	$⊢ (((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <))) \land (a \in ℝ^{} \land b \in ℝ^{})) \to b \in ℝ^{*}$
123		simplr3	$⊢ (((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <))) \land (a \in ℝ^{} \land b \in ℝ^{})) \to b < sup (Y ℝ^{*} <)$
124		supxrlub	$⊢ (Y \subseteq ℝ^{} \land b \in ℝ^{}) \to (b < sup (Y ℝ^{*} <) \leftrightarrow \exists w \in Y b < w)$
125	124	biimpa	$⊢ ((Y \subseteq ℝ^{} \land b \in ℝ^{}) \land b < sup (Y ℝ^{*} <)) \to \exists w \in Y b < w$
126	121 122 123 125	syl21anc	$⊢ (((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <))) \land (a \in ℝ^{} \land b \in ℝ^{})) \to \exists w \in Y b < w$
127		reeanv	$⊢ \exists v \in X \exists w \in Y (a < v \land b < w) \leftrightarrow (\exists v \in X a < v \land \exists w \in Y b < w)$
128	120 126 127	sylanbrc	$⊢ (((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <))) \land (a \in ℝ^{} \land b \in ℝ^{})) \to \exists v \in X \exists w \in Y (a < v \land b < w)$
129	128	ancoms	$⊢ ((a \in ℝ^{} \land b \in ℝ^{}) \land ((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <)))) \to \exists v \in X \exists w \in Y (a < v \land b < w)$
130	114 129	reximddv2	$⊢ ((a \in ℝ^{} \land b \in ℝ^{}) \land ((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <)))) \to \exists v \in X \exists w \in Y z < v +_{𝑒} w$
131	130	ex	$⊢ (a \in ℝ^{} \land b \in ℝ^{}) \to (((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <))) \to \exists v \in X \exists w \in Y z < v +_{𝑒} w)$
132	131	reximdva	$⊢ a \in ℝ^{} \to (\exists b \in ℝ^{} ((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <))) \to \exists b \in ℝ^{*} \exists v \in X \exists w \in Y z < v +_{𝑒} w)$
133	132	reximia	$⊢ \exists a \in ℝ^{} \exists b \in ℝ^{} ((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <))) \to \exists a \in ℝ^{} \exists b \in ℝ^{} \exists v \in X \exists w \in Y z < v +_{𝑒} w$
134	94 133	syl	$⊢ ((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land \exists a \in ℝ^{} \exists b \in ℝ^{} (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <))) \to \exists a \in ℝ^{} \exists b \in ℝ^{} \exists v \in X \exists w \in Y z < v +_{𝑒} w$
135	86 87 88 134	19.9d2rf	$⊢ ((X \subseteq ℝ^{} \land Y \subseteq ℝ^{}) \land \exists a \in ℝ^{} \exists b \in ℝ^{} (z = a +_{𝑒} b \land a < sup (X ℝ^{} <) \land b < sup (Y ℝ^{} <))) \to \exists v \in X \exists w \in Y z < v +_{𝑒} w$
136	73 74 81 135	syl21anc	$⊢ ((φ \land z \in ℝ) \land z < sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <)) \to \exists v \in X \exists w \in Y z < v +_{𝑒} w$
137		simprl	$⊢ (φ \land (v \in X \land w \in Y)) \to v \in X$
138		simprr	$⊢ (φ \land (v \in X \land w \in Y)) \to w \in Y$
139	21	a1i	$⊢ (φ \land (v \in X \land w \in Y)) \to Fun +_{𝑒}$
140	25	adantr	$⊢ (φ \land (v \in X \land w \in Y)) \to X \times Y \subseteq dom +_{𝑒}$
141	137 138 139 140	elovimad	$⊢ (φ \land (v \in X \land w \in Y)) \to v +_{𝑒} w \in +_{𝑒} [X \times Y]$
142	5	eleq2d	$⊢ φ \to (v +_{𝑒} w \in Z \leftrightarrow v +_{𝑒} w \in +_{𝑒} [X \times Y])$
143	142	adantr	$⊢ (φ \land (v \in X \land w \in Y)) \to (v +_{𝑒} w \in Z \leftrightarrow v +_{𝑒} w \in +_{𝑒} [X \times Y])$
144	141 143	mpbird	$⊢ (φ \land (v \in X \land w \in Y)) \to v +_{𝑒} w \in Z$
145		simpr	$⊢ ((φ \land (v \in X \land w \in Y)) \land k = v +_{𝑒} w) \to k = v +_{𝑒} w$
146	145	breq2d	$⊢ ((φ \land (v \in X \land w \in Y)) \land k = v +_{𝑒} w) \to (z < k \leftrightarrow z < v +_{𝑒} w)$
147	144 146	rspcedv	$⊢ (φ \land (v \in X \land w \in Y)) \to (z < v +_{𝑒} w \to \exists k \in Z z < k)$
148	147	rexlimdvva	$⊢ φ \to (\exists v \in X \exists w \in Y z < v +_{𝑒} w \to \exists k \in Z z < k)$
149	148	ad2antrr	$⊢ ((φ \land z \in ℝ) \land z < sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <)) \to (\exists v \in X \exists w \in Y z < v +_{𝑒} w \to \exists k \in Z z < k)$
150	136 149	mpd	$⊢ ((φ \land z \in ℝ) \land z < sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <)) \to \exists k \in Z z < k$
151	150	ex	$⊢ (φ \land z \in ℝ) \to (z < sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <) \to \exists k \in Z z < k)$
152	151	ralrimiva	$⊢ φ \to \forall z \in ℝ (z < sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <) \to \exists k \in Z z < k)$
153		supxr2	$⊢ ((Z \subseteq ℝ^{} \land sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <) \in ℝ^{}) \land (\forall z \in Z z \leq sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <) \land \forall z \in ℝ (z < sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{} <) \to \exists k \in Z z < k))) \to sup (Z ℝ^{} <) = sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{*} <)$
154	29 34 72 152 153	syl22anc	$⊢ φ \to sup (Z ℝ^{} <) = sup (X ℝ^{} <) +_{𝑒} sup (Y ℝ^{*} <)$

Metamath Proof Explorer

Theorem xrofsup

Proof