xrofsup - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > xrofsup		Structured version Visualization version GIF version

Theorem xrofsup 32235

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.)

**Hypotheses**
Ref	Expression
xrofsup.1	⊢ (𝜑 → 𝑋 ⊆ ℝ^*)
xrofsup.2	⊢ (𝜑 → 𝑌 ⊆ ℝ^*)
xrofsup.3	⊢ (𝜑 → sup(𝑋, ℝ^*, < ) ≠ -∞)
xrofsup.4	⊢ (𝜑 → sup(𝑌, ℝ^*, < ) ≠ -∞)
xrofsup.5	⊢ (𝜑 → 𝑍 = ( +_𝑒 “ (𝑋 × 𝑌)))

**Assertion**
Ref	Expression
xrofsup	⊢ (𝜑 → sup(𝑍, ℝ^, < ) = (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^*, < )))

Proof of Theorem xrofsup Dummy variables 𝑎 𝑏 𝑘 𝑢 𝑣 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		xrofsup.5	. . 3 ⊢ (𝜑 → 𝑍 = ( +_𝑒 “ (𝑋 × 𝑌)))
2		xrofsup.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ⊆ ℝ^*)
3	2	sseld 3981	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝑋 → 𝑥 ∈ ℝ^*))
4		xrofsup.2	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ⊆ ℝ^*)
5	4	sseld 3981	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ 𝑌 → 𝑦 ∈ ℝ^*))
6	3, 5	anim12d 609	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → (𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*)))
7	6	imp 407	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*))
8		xaddcl 13222	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → (𝑥 +_𝑒 𝑦) ∈ ℝ^)
9	7, 8	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑥 +_𝑒 𝑦) ∈ ℝ^*)
10	9	ralrimivva 3200	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝑥 +_𝑒 𝑦) ∈ ℝ^*)
11		fveq2 6891	. . . . . . . 8 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → ( +_𝑒 ‘𝑢) = ( +_𝑒 ‘⟨𝑥, 𝑦⟩))
12		df-ov 7414	. . . . . . . 8 ⊢ (𝑥 +_𝑒 𝑦) = ( +_𝑒 ‘⟨𝑥, 𝑦⟩)
13	11, 12	eqtr4di 2790	. . . . . . 7 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → ( +_𝑒 ‘𝑢) = (𝑥 +_𝑒 𝑦))
14	13	eleq1d 2818	. . . . . 6 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → (( +_𝑒 ‘𝑢) ∈ ℝ^* ↔ (𝑥 +_𝑒 𝑦) ∈ ℝ^*))
15	14	ralxp 5841	. . . . 5 ⊢ (∀𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) ∈ ℝ^* ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝑥 +_𝑒 𝑦) ∈ ℝ^*)
16	10, 15	sylibr 233	. . . 4 ⊢ (𝜑 → ∀𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) ∈ ℝ^*)
17		xaddf 13207	. . . . . 6 ⊢ +_𝑒 :(ℝ^* × ℝ^)⟶ℝ^
18		ffun 6720	. . . . . 6 ⊢ ( +_𝑒 :(ℝ^* × ℝ^)⟶ℝ^ → Fun +_𝑒 )
19	17, 18	ax-mp 5	. . . . 5 ⊢ Fun +_𝑒
20		xpss12 5691	. . . . . . 7 ⊢ ((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) → (𝑋 × 𝑌) ⊆ (ℝ^ × ℝ^*))
21	2, 4, 20	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (𝑋 × 𝑌) ⊆ (ℝ^* × ℝ^*))
22	17	fdmi 6729	. . . . . 6 ⊢ dom +_𝑒 = (ℝ^* × ℝ^*)
23	21, 22	sseqtrrdi 4033	. . . . 5 ⊢ (𝜑 → (𝑋 × 𝑌) ⊆ dom +_𝑒 )
24		funimass4 6956	. . . . 5 ⊢ ((Fun +_𝑒 ∧ (𝑋 × 𝑌) ⊆ dom +_𝑒 ) → (( +_𝑒 “ (𝑋 × 𝑌)) ⊆ ℝ^* ↔ ∀𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) ∈ ℝ^*))
25	19, 23, 24	sylancr 587	. . . 4 ⊢ (𝜑 → (( +_𝑒 “ (𝑋 × 𝑌)) ⊆ ℝ^* ↔ ∀𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) ∈ ℝ^*))
26	16, 25	mpbird 256	. . 3 ⊢ (𝜑 → ( +_𝑒 “ (𝑋 × 𝑌)) ⊆ ℝ^*)
27	1, 26	eqsstrd 4020	. 2 ⊢ (𝜑 → 𝑍 ⊆ ℝ^*)
28		supxrcl 13298	. . . 4 ⊢ (𝑋 ⊆ ℝ^* → sup(𝑋, ℝ^, < ) ∈ ℝ^)
29	2, 28	syl 17	. . 3 ⊢ (𝜑 → sup(𝑋, ℝ^, < ) ∈ ℝ^)
30		supxrcl 13298	. . . 4 ⊢ (𝑌 ⊆ ℝ^* → sup(𝑌, ℝ^, < ) ∈ ℝ^)
31	4, 30	syl 17	. . 3 ⊢ (𝜑 → sup(𝑌, ℝ^, < ) ∈ ℝ^)
32	29, 31	xaddcld 13284	. 2 ⊢ (𝜑 → (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) ∈ ℝ^*)
33	1	eleq2d 2819	. . . . 5 ⊢ (𝜑 → (𝑧 ∈ 𝑍 ↔ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))))
34	33	pm5.32i 575	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑍) ↔ (𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))))
35		nfvd 1918	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → Ⅎ𝑥 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
36		nfvd 1918	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → Ⅎ𝑦 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
37	2	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑋 ⊆ ℝ^*)
38		simprl 769	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑥 ∈ 𝑋)
39		supxrub 13307	. . . . . . . . . . 11 ⊢ ((𝑋 ⊆ ℝ^* ∧ 𝑥 ∈ 𝑋) → 𝑥 ≤ sup(𝑋, ℝ^*, < ))
40	37, 38, 39	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑥 ≤ sup(𝑋, ℝ^*, < ))
41	4	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑌 ⊆ ℝ^*)
42		simprr 771	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑦 ∈ 𝑌)
43		supxrub 13307	. . . . . . . . . . 11 ⊢ ((𝑌 ⊆ ℝ^* ∧ 𝑦 ∈ 𝑌) → 𝑦 ≤ sup(𝑌, ℝ^*, < ))
44	41, 42, 43	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑦 ≤ sup(𝑌, ℝ^*, < ))
45	37, 38	sseldd 3983	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑥 ∈ ℝ^*)
46	41, 42	sseldd 3983	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑦 ∈ ℝ^*)
47	37, 28	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → sup(𝑋, ℝ^, < ) ∈ ℝ^)
48	41, 30	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → sup(𝑌, ℝ^, < ) ∈ ℝ^)
49		xle2add 13242	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) ∧ (sup(𝑋, ℝ^, < ) ∈ ℝ^* ∧ sup(𝑌, ℝ^, < ) ∈ ℝ^)) → ((𝑥 ≤ sup(𝑋, ℝ^, < ) ∧ 𝑦 ≤ sup(𝑌, ℝ^, < )) → (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))))
50	45, 46, 47, 48, 49	syl22anc 837	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑥 ≤ sup(𝑋, ℝ^, < ) ∧ 𝑦 ≤ sup(𝑌, ℝ^, < )) → (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))))
51	40, 44, 50	mp2and 697	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
52	51	ralrimivva 3200	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
53		fvelima 6957	. . . . . . . . . . 11 ⊢ ((Fun +_𝑒 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → ∃𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) = 𝑧)
54	19, 53	mpan 688	. . . . . . . . . 10 ⊢ (𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌)) → ∃𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) = 𝑧)
55	54	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → ∃𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) = 𝑧)
56	13	eqeq1d 2734	. . . . . . . . . 10 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → (( +_𝑒 ‘𝑢) = 𝑧 ↔ (𝑥 +_𝑒 𝑦) = 𝑧))
57	56	rexxp 5842	. . . . . . . . 9 ⊢ (∃𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) = 𝑧 ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 (𝑥 +_𝑒 𝑦) = 𝑧)
58	55, 57	sylib 217	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 (𝑥 +_𝑒 𝑦) = 𝑧)
59	52, 58	r19.29d2r 3140	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ((𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) ∧ (𝑥 +_𝑒 𝑦) = 𝑧))
60		ancom 461	. . . . . . . 8 ⊢ (((𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) ∧ (𝑥 +_𝑒 𝑦) = 𝑧) ↔ ((𝑥 +_𝑒 𝑦) = 𝑧 ∧ (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))))
61	60	2rexbii 3129	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ((𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) ∧ (𝑥 +_𝑒 𝑦) = 𝑧) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ((𝑥 +_𝑒 𝑦) = 𝑧 ∧ (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))))
62	59, 61	sylib 217	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ((𝑥 +_𝑒 𝑦) = 𝑧 ∧ (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))))
63		breq1 5151	. . . . . . . . 9 ⊢ ((𝑥 +_𝑒 𝑦) = 𝑧 → ((𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) ↔ 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))))
64	63	biimpa 477	. . . . . . . 8 ⊢ (((𝑥 +_𝑒 𝑦) = 𝑧 ∧ (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
65	64	reximi 3084	. . . . . . 7 ⊢ (∃𝑦 ∈ 𝑌 ((𝑥 +_𝑒 𝑦) = 𝑧 ∧ (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → ∃𝑦 ∈ 𝑌 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
66	65	reximi 3084	. . . . . 6 ⊢ (∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ((𝑥 +_𝑒 𝑦) = 𝑧 ∧ (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
67	62, 66	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
68	35, 36, 67	19.9d2r 31967	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
69	34, 68	sylbi 216	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑍) → 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
70	69	ralrimiva 3146	. 2 ⊢ (𝜑 → ∀𝑧 ∈ 𝑍 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
71	2	ad2antrr 724	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → 𝑋 ⊆ ℝ^*)
72	4	ad2antrr 724	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → 𝑌 ⊆ ℝ^*)
73		simplr 767	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → 𝑧 ∈ ℝ)
74	29	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → sup(𝑋, ℝ^, < ) ∈ ℝ^)
75	31	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → sup(𝑌, ℝ^, < ) ∈ ℝ^)
76		xrofsup.3	. . . . . . . 8 ⊢ (𝜑 → sup(𝑋, ℝ^*, < ) ≠ -∞)
77	76	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → sup(𝑋, ℝ^*, < ) ≠ -∞)
78		xrofsup.4	. . . . . . . 8 ⊢ (𝜑 → sup(𝑌, ℝ^*, < ) ≠ -∞)
79	78	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → sup(𝑌, ℝ^*, < ) ≠ -∞)
80		simpr 485	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
81	73, 74, 75, 77, 79, 80	xlt2addrd 32226	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → ∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))
82		nfv 1917	. . . . . . . 8 ⊢ Ⅎ𝑏(𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^*)
83		nfcv 2903	. . . . . . . . 9 ⊢ Ⅎ𝑏ℝ^*
84		nfre1 3282	. . . . . . . . 9 ⊢ Ⅎ𝑏∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))
85	83, 84	nfrexw 3310	. . . . . . . 8 ⊢ Ⅎ𝑏∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))
86	82, 85	nfan 1902	. . . . . . 7 ⊢ Ⅎ𝑏((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))
87		nfvd 1918	. . . . . . 7 ⊢ (((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → Ⅎ𝑎∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤))
88		nfvd 1918	. . . . . . 7 ⊢ (((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → Ⅎ𝑏∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤))
89		id 22	. . . . . . . . . . . 12 ⊢ ((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) → (𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^*))
90	89	ralrimivw 3150	. . . . . . . . . . 11 ⊢ ((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) → ∀𝑏 ∈ ℝ^ (𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^*))
91	90	ralrimivw 3150	. . . . . . . . . 10 ⊢ ((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) → ∀𝑎 ∈ ℝ^ ∀𝑏 ∈ ℝ^* (𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^*))
92	91	adantr 481	. . . . . . . . 9 ⊢ (((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → ∀𝑎 ∈ ℝ^* ∀𝑏 ∈ ℝ^* (𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^*))
93		simpr 485	. . . . . . . . 9 ⊢ (((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → ∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))
94	92, 93	r19.29d2r 3140	. . . . . . . 8 ⊢ (((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → ∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* ((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < ))))
95		simplrr 776	. . . . . . . . . . . . . . 15 ⊢ ((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌 ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤))) → (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))
96	95	3anassrs 1360	. . . . . . . . . . . . . 14 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))
97	96	simp1d 1142	. . . . . . . . . . . . 13 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑧 = (𝑎 +_𝑒 𝑏))
98		simp-4l 781	. . . . . . . . . . . . . 14 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^*))
99		simplrl 775	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌 ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤))) → (𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^*))
100	99	3anassrs 1360	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → (𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^*))
101	100	simpld 495	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑋 ⊆ ℝ^)
102		simpllr 774	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑣 ∈ 𝑋)
103	101, 102	sseldd 3983	. . . . . . . . . . . . . 14 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑣 ∈ ℝ^)
104	100	simprd 496	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑌 ⊆ ℝ^)
105		simplr 767	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑤 ∈ 𝑌)
106	104, 105	sseldd 3983	. . . . . . . . . . . . . 14 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑤 ∈ ℝ^)
107	98, 103, 106	jca32 516	. . . . . . . . . . . . 13 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → ((𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^) ∧ (𝑣 ∈ ℝ^ ∧ 𝑤 ∈ ℝ^*)))
108		simpr 485	. . . . . . . . . . . . 13 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → (𝑎 < 𝑣 ∧ 𝑏 < 𝑤))
109		xlt2add 13243	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ (𝑣 ∈ ℝ^ ∧ 𝑤 ∈ ℝ^*)) → ((𝑎 < 𝑣 ∧ 𝑏 < 𝑤) → (𝑎 +_𝑒 𝑏) < (𝑣 +_𝑒 𝑤)))
110	109	imp 407	. . . . . . . . . . . . . 14 ⊢ ((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ (𝑣 ∈ ℝ^ ∧ 𝑤 ∈ ℝ^*)) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → (𝑎 +_𝑒 𝑏) < (𝑣 +_𝑒 𝑤))
111		breq1 5151	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑎 +_𝑒 𝑏) → (𝑧 < (𝑣 +_𝑒 𝑤) ↔ (𝑎 +_𝑒 𝑏) < (𝑣 +_𝑒 𝑤)))
112	111	biimpar 478	. . . . . . . . . . . . . 14 ⊢ ((𝑧 = (𝑎 +_𝑒 𝑏) ∧ (𝑎 +_𝑒 𝑏) < (𝑣 +_𝑒 𝑤)) → 𝑧 < (𝑣 +_𝑒 𝑤))
113	110, 112	sylan2 593	. . . . . . . . . . . . 13 ⊢ ((𝑧 = (𝑎 +_𝑒 𝑏) ∧ (((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ (𝑣 ∈ ℝ^ ∧ 𝑤 ∈ ℝ^*)) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤))) → 𝑧 < (𝑣 +_𝑒 𝑤))
114	97, 107, 108, 113	syl12anc 835	. . . . . . . . . . . 12 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑧 < (𝑣 +_𝑒 𝑤))
115		simplll 773	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^)) → 𝑋 ⊆ ℝ^)
116		simprl 769	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^)) → 𝑎 ∈ ℝ^)
117		simplr2 1216	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^)) → 𝑎 < sup(𝑋, ℝ^, < ))
118		supxrlub 13308	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ⊆ ℝ^* ∧ 𝑎 ∈ ℝ^) → (𝑎 < sup(𝑋, ℝ^, < ) ↔ ∃𝑣 ∈ 𝑋 𝑎 < 𝑣))
119	118	biimpa 477	. . . . . . . . . . . . . . 15 ⊢ (((𝑋 ⊆ ℝ^* ∧ 𝑎 ∈ ℝ^) ∧ 𝑎 < sup(𝑋, ℝ^, < )) → ∃𝑣 ∈ 𝑋 𝑎 < 𝑣)
120	115, 116, 117, 119	syl21anc 836	. . . . . . . . . . . . . 14 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^*)) → ∃𝑣 ∈ 𝑋 𝑎 < 𝑣)
121		simpllr 774	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^)) → 𝑌 ⊆ ℝ^)
122		simprr 771	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^)) → 𝑏 ∈ ℝ^)
123		simplr3 1217	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^)) → 𝑏 < sup(𝑌, ℝ^, < ))
124		supxrlub 13308	. . . . . . . . . . . . . . . 16 ⊢ ((𝑌 ⊆ ℝ^* ∧ 𝑏 ∈ ℝ^) → (𝑏 < sup(𝑌, ℝ^, < ) ↔ ∃𝑤 ∈ 𝑌 𝑏 < 𝑤))
125	124	biimpa 477	. . . . . . . . . . . . . . 15 ⊢ (((𝑌 ⊆ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ 𝑏 < sup(𝑌, ℝ^, < )) → ∃𝑤 ∈ 𝑌 𝑏 < 𝑤)
126	121, 122, 123, 125	syl21anc 836	. . . . . . . . . . . . . 14 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^*)) → ∃𝑤 ∈ 𝑌 𝑏 < 𝑤)
127		reeanv 3226	. . . . . . . . . . . . . 14 ⊢ (∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 (𝑎 < 𝑣 ∧ 𝑏 < 𝑤) ↔ (∃𝑣 ∈ 𝑋 𝑎 < 𝑣 ∧ ∃𝑤 ∈ 𝑌 𝑏 < 𝑤))
128	120, 126, 127	sylanbrc 583	. . . . . . . . . . . . 13 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^*)) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 (𝑎 < 𝑣 ∧ 𝑏 < 𝑤))
129	128	ancoms 459	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 (𝑎 < 𝑣 ∧ 𝑏 < 𝑤))
130	114, 129	reximddv2 3212	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤))
131	130	ex 413	. . . . . . . . . 10 ⊢ ((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) → (((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < ))) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤)))
132	131	reximdva 3168	. . . . . . . . 9 ⊢ (𝑎 ∈ ℝ^* → (∃𝑏 ∈ ℝ^* ((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → ∃𝑏 ∈ ℝ^ ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤)))
133	132	reximia 3081	. . . . . . . 8 ⊢ (∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* ((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤))
134	94, 133	syl 17	. . . . . . 7 ⊢ (((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → ∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤))
135	86, 87, 88, 134	19.9d2rf 31966	. . . . . 6 ⊢ (((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤))
136	71, 72, 81, 135	syl21anc 836	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤))
137		simprl 769	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → 𝑣 ∈ 𝑋)
138		simprr 771	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → 𝑤 ∈ 𝑌)
139	19	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → Fun +_𝑒 )
140	23	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → (𝑋 × 𝑌) ⊆ dom +_𝑒 )
141	137, 138, 139, 140	elovimad 7459	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → (𝑣 +_𝑒 𝑤) ∈ ( +_𝑒 “ (𝑋 × 𝑌)))
142	1	eleq2d 2819	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑣 +_𝑒 𝑤) ∈ 𝑍 ↔ (𝑣 +_𝑒 𝑤) ∈ ( +_𝑒 “ (𝑋 × 𝑌))))
143	142	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → ((𝑣 +_𝑒 𝑤) ∈ 𝑍 ↔ (𝑣 +_𝑒 𝑤) ∈ ( +_𝑒 “ (𝑋 × 𝑌))))
144	141, 143	mpbird 256	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → (𝑣 +_𝑒 𝑤) ∈ 𝑍)
145		simpr 485	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) ∧ 𝑘 = (𝑣 +_𝑒 𝑤)) → 𝑘 = (𝑣 +_𝑒 𝑤))
146	145	breq2d 5160	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) ∧ 𝑘 = (𝑣 +_𝑒 𝑤)) → (𝑧 < 𝑘 ↔ 𝑧 < (𝑣 +_𝑒 𝑤)))
147	144, 146	rspcedv 3605	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → (𝑧 < (𝑣 +_𝑒 𝑤) → ∃𝑘 ∈ 𝑍 𝑧 < 𝑘))
148	147	rexlimdvva 3211	. . . . . 6 ⊢ (𝜑 → (∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤) → ∃𝑘 ∈ 𝑍 𝑧 < 𝑘))
149	148	ad2antrr 724	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → (∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤) → ∃𝑘 ∈ 𝑍 𝑧 < 𝑘))
150	136, 149	mpd 15	. . . 4 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → ∃𝑘 ∈ 𝑍 𝑧 < 𝑘)
151	150	ex 413	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → (𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) → ∃𝑘 ∈ 𝑍 𝑧 < 𝑘))
152	151	ralrimiva 3146	. 2 ⊢ (𝜑 → ∀𝑧 ∈ ℝ (𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) → ∃𝑘 ∈ 𝑍 𝑧 < 𝑘))
153		supxr2 13297	. 2 ⊢ (((𝑍 ⊆ ℝ^* ∧ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) ∈ ℝ^) ∧ (∀𝑧 ∈ 𝑍 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) ∧ ∀𝑧 ∈ ℝ (𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) → ∃𝑘 ∈ 𝑍 𝑧 < 𝑘))) → sup(𝑍, ℝ^, < ) = (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
154	27, 32, 70, 152, 153	syl22anc 837	1 ⊢ (𝜑 → sup(𝑍, ℝ^, < ) = (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^*, < )))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ≠ wne 2940 ∀wral 3061 ∃wrex 3070 ⊆ wss 3948 ⟨cop 4634 class class class wbr 5148 × cxp 5674 dom cdm 5676 “ cima 5679 Fun wfun 6537 ⟶wf 6539 ‘cfv 6543 (class class class)co 7411 supcsup 9437 ℝcr 11111 -∞cmnf 11250 ℝ^*cxr 11251 < clt 11252 ≤ cle 11253 +_𝑒 cxad 13094

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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7727 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189 ax-pre-sup 11190

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5574 df-po 5588 df-so 5589 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7367 df-ov 7414 df-oprab 7415 df-mpo 7416 df-1st 7977 df-2nd 7978 df-er 8705 df-en 8942 df-dom 8943 df-sdom 8944 df-sup 9439 df-pnf 11254 df-mnf 11255 df-xr 11256 df-ltxr 11257 df-le 11258 df-sub 11450 df-neg 11451 df-div 11876 df-2 12279 df-rp 12979 df-xneg 13096 df-xadd 13097

This theorem is referenced by: (None)

W3C validator