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 31740

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 3946	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝑋 → 𝑥 ∈ ℝ^*))
4		xrofsup.2	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ⊆ ℝ^*)
5	4	sseld 3946	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ 𝑌 → 𝑦 ∈ ℝ^*))
6	3, 5	anim12d 609	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → (𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*)))
7	6	imp 407	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*))
8		xaddcl 13168	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → (𝑥 +_𝑒 𝑦) ∈ ℝ^)
9	7, 8	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑥 +_𝑒 𝑦) ∈ ℝ^*)
10	9	ralrimivva 3193	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝑥 +_𝑒 𝑦) ∈ ℝ^*)
11		fveq2 6847	. . . . . . . 8 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → ( +_𝑒 ‘𝑢) = ( +_𝑒 ‘⟨𝑥, 𝑦⟩))
12		df-ov 7365	. . . . . . . 8 ⊢ (𝑥 +_𝑒 𝑦) = ( +_𝑒 ‘⟨𝑥, 𝑦⟩)
13	11, 12	eqtr4di 2789	. . . . . . 7 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → ( +_𝑒 ‘𝑢) = (𝑥 +_𝑒 𝑦))
14	13	eleq1d 2817	. . . . . 6 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → (( +_𝑒 ‘𝑢) ∈ ℝ^* ↔ (𝑥 +_𝑒 𝑦) ∈ ℝ^*))
15	14	ralxp 5802	. . . . 5 ⊢ (∀𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) ∈ ℝ^* ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝑥 +_𝑒 𝑦) ∈ ℝ^*)
16	10, 15	sylibr 233	. . . 4 ⊢ (𝜑 → ∀𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) ∈ ℝ^*)
17		xaddf 13153	. . . . . 6 ⊢ +_𝑒 :(ℝ^* × ℝ^)⟶ℝ^
18		ffun 6676	. . . . . 6 ⊢ ( +_𝑒 :(ℝ^* × ℝ^)⟶ℝ^ → Fun +_𝑒 )
19	17, 18	ax-mp 5	. . . . 5 ⊢ Fun +_𝑒
20		xpss12 5653	. . . . . . 7 ⊢ ((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) → (𝑋 × 𝑌) ⊆ (ℝ^ × ℝ^*))
21	2, 4, 20	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (𝑋 × 𝑌) ⊆ (ℝ^* × ℝ^*))
22	17	fdmi 6685	. . . . . 6 ⊢ dom +_𝑒 = (ℝ^* × ℝ^*)
23	21, 22	sseqtrrdi 3998	. . . . 5 ⊢ (𝜑 → (𝑋 × 𝑌) ⊆ dom +_𝑒 )
24		funimass4 6912	. . . . 5 ⊢ ((Fun +_𝑒 ∧ (𝑋 × 𝑌) ⊆ dom +_𝑒 ) → (( +_𝑒 “ (𝑋 × 𝑌)) ⊆ ℝ^* ↔ ∀𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) ∈ ℝ^*))
25	19, 23, 24	sylancr 587	. . . 4 ⊢ (𝜑 → (( +_𝑒 “ (𝑋 × 𝑌)) ⊆ ℝ^* ↔ ∀𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) ∈ ℝ^*))
26	16, 25	mpbird 256	. . 3 ⊢ (𝜑 → ( +_𝑒 “ (𝑋 × 𝑌)) ⊆ ℝ^*)
27	1, 26	eqsstrd 3985	. 2 ⊢ (𝜑 → 𝑍 ⊆ ℝ^*)
28		supxrcl 13244	. . . 4 ⊢ (𝑋 ⊆ ℝ^* → sup(𝑋, ℝ^, < ) ∈ ℝ^)
29	2, 28	syl 17	. . 3 ⊢ (𝜑 → sup(𝑋, ℝ^, < ) ∈ ℝ^)
30		supxrcl 13244	. . . 4 ⊢ (𝑌 ⊆ ℝ^* → sup(𝑌, ℝ^, < ) ∈ ℝ^)
31	4, 30	syl 17	. . 3 ⊢ (𝜑 → sup(𝑌, ℝ^, < ) ∈ ℝ^)
32	29, 31	xaddcld 13230	. 2 ⊢ (𝜑 → (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) ∈ ℝ^*)
33	1	eleq2d 2818	. . . . 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 13253	. . . . . . . . . . 11 ⊢ ((𝑋 ⊆ ℝ^* ∧ 𝑥 ∈ 𝑋) → 𝑥 ≤ sup(𝑋, ℝ^*, < ))
40	37, 38, 39	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑥 ≤ sup(𝑋, ℝ^*, < ))
41	4	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑌 ⊆ ℝ^*)
42		simprr 771	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑦 ∈ 𝑌)
43		supxrub 13253	. . . . . . . . . . 11 ⊢ ((𝑌 ⊆ ℝ^* ∧ 𝑦 ∈ 𝑌) → 𝑦 ≤ sup(𝑌, ℝ^*, < ))
44	41, 42, 43	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑦 ≤ sup(𝑌, ℝ^*, < ))
45	37, 38	sseldd 3948	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑥 ∈ ℝ^*)
46	41, 42	sseldd 3948	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑦 ∈ ℝ^*)
47	37, 28	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → sup(𝑋, ℝ^, < ) ∈ ℝ^)
48	41, 30	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → sup(𝑌, ℝ^, < ) ∈ ℝ^)
49		xle2add 13188	. . . . . . . . . . 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 3193	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
53		fvelima 6913	. . . . . . . . . . 11 ⊢ ((Fun +_𝑒 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → ∃𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) = 𝑧)
54	19, 53	mpan 688	. . . . . . . . . 10 ⊢ (𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌)) → ∃𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) = 𝑧)
55	54	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → ∃𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) = 𝑧)
56	13	eqeq1d 2733	. . . . . . . . . 10 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → (( +_𝑒 ‘𝑢) = 𝑧 ↔ (𝑥 +_𝑒 𝑦) = 𝑧))
57	56	rexxp 5803	. . . . . . . . 9 ⊢ (∃𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) = 𝑧 ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 (𝑥 +_𝑒 𝑦) = 𝑧)
58	55, 57	sylib 217	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 (𝑥 +_𝑒 𝑦) = 𝑧)
59	52, 58	r19.29d2r 3133	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ((𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) ∧ (𝑥 +_𝑒 𝑦) = 𝑧))
60		ancom 461	. . . . . . . 8 ⊢ (((𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) ∧ (𝑥 +_𝑒 𝑦) = 𝑧) ↔ ((𝑥 +_𝑒 𝑦) = 𝑧 ∧ (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))))
61	60	2rexbii 3124	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ((𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) ∧ (𝑥 +_𝑒 𝑦) = 𝑧) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ((𝑥 +_𝑒 𝑦) = 𝑧 ∧ (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))))
62	59, 61	sylib 217	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ((𝑥 +_𝑒 𝑦) = 𝑧 ∧ (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))))
63		breq1 5113	. . . . . . . . 9 ⊢ ((𝑥 +_𝑒 𝑦) = 𝑧 → ((𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) ↔ 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))))
64	63	biimpa 477	. . . . . . . 8 ⊢ (((𝑥 +_𝑒 𝑦) = 𝑧 ∧ (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
65	64	reximi 3083	. . . . . . 7 ⊢ (∃𝑦 ∈ 𝑌 ((𝑥 +_𝑒 𝑦) = 𝑧 ∧ (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → ∃𝑦 ∈ 𝑌 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
66	65	reximi 3083	. . . . . 6 ⊢ (∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ((𝑥 +_𝑒 𝑦) = 𝑧 ∧ (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
67	62, 66	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
68	35, 36, 67	19.9d2r 31464	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
69	34, 68	sylbi 216	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑍) → 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
70	69	ralrimiva 3139	. 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 31731	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → ∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))
82		nfv 1917	. . . . . . . 8 ⊢ Ⅎ𝑏(𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^*)
83		nfcv 2902	. . . . . . . . 9 ⊢ Ⅎ𝑏ℝ^*
84		nfre1 3266	. . . . . . . . 9 ⊢ Ⅎ𝑏∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))
85	83, 84	nfrexw 3294	. . . . . . . 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 3143	. . . . . . . . . . 11 ⊢ ((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) → ∀𝑏 ∈ ℝ^ (𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^*))
91	90	ralrimivw 3143	. . . . . . . . . 10 ⊢ ((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) → ∀𝑎 ∈ ℝ^ ∀𝑏 ∈ ℝ^* (𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^*))
92	91	adantr 481	. . . . . . . . 9 ⊢ (((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → ∀𝑎 ∈ ℝ^* ∀𝑏 ∈ ℝ^* (𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^*))
93		simpr 485	. . . . . . . . 9 ⊢ (((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → ∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))
94	92, 93	r19.29d2r 3133	. . . . . . . 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 3948	. . . . . . . . . . . . . 14 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑣 ∈ ℝ^)
104	100	simprd 496	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑌 ⊆ ℝ^)
105		simplr 767	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑤 ∈ 𝑌)
106	104, 105	sseldd 3948	. . . . . . . . . . . . . 14 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑤 ∈ ℝ^)
107	98, 103, 106	jca32 516	. . . . . . . . . . . . 13 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → ((𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^) ∧ (𝑣 ∈ ℝ^ ∧ 𝑤 ∈ ℝ^*)))
108		simpr 485	. . . . . . . . . . . . 13 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → (𝑎 < 𝑣 ∧ 𝑏 < 𝑤))
109		xlt2add 13189	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ (𝑣 ∈ ℝ^ ∧ 𝑤 ∈ ℝ^*)) → ((𝑎 < 𝑣 ∧ 𝑏 < 𝑤) → (𝑎 +_𝑒 𝑏) < (𝑣 +_𝑒 𝑤)))
110	109	imp 407	. . . . . . . . . . . . . 14 ⊢ ((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ (𝑣 ∈ ℝ^ ∧ 𝑤 ∈ ℝ^*)) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → (𝑎 +_𝑒 𝑏) < (𝑣 +_𝑒 𝑤))
111		breq1 5113	. . . . . . . . . . . . . . 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 13254	. . . . . . . . . . . . . . . 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 13254	. . . . . . . . . . . . . . . 16 ⊢ ((𝑌 ⊆ ℝ^* ∧ 𝑏 ∈ ℝ^) → (𝑏 < sup(𝑌, ℝ^, < ) ↔ ∃𝑤 ∈ 𝑌 𝑏 < 𝑤))
125	124	biimpa 477	. . . . . . . . . . . . . . 15 ⊢ (((𝑌 ⊆ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ 𝑏 < sup(𝑌, ℝ^, < )) → ∃𝑤 ∈ 𝑌 𝑏 < 𝑤)
126	121, 122, 123, 125	syl21anc 836	. . . . . . . . . . . . . 14 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^*)) → ∃𝑤 ∈ 𝑌 𝑏 < 𝑤)
127		reeanv 3215	. . . . . . . . . . . . . 14 ⊢ (∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 (𝑎 < 𝑣 ∧ 𝑏 < 𝑤) ↔ (∃𝑣 ∈ 𝑋 𝑎 < 𝑣 ∧ ∃𝑤 ∈ 𝑌 𝑏 < 𝑤))
128	120, 126, 127	sylanbrc 583	. . . . . . . . . . . . 13 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^*)) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 (𝑎 < 𝑣 ∧ 𝑏 < 𝑤))
129	128	ancoms 459	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 (𝑎 < 𝑣 ∧ 𝑏 < 𝑤))
130	114, 129	reximddv2 3202	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤))
131	130	ex 413	. . . . . . . . . 10 ⊢ ((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) → (((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < ))) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤)))
132	131	reximdva 3161	. . . . . . . . 9 ⊢ (𝑎 ∈ ℝ^* → (∃𝑏 ∈ ℝ^* ((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → ∃𝑏 ∈ ℝ^ ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤)))
133	132	reximia 3080	. . . . . . . 8 ⊢ (∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* ((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤))
134	94, 133	syl 17	. . . . . . 7 ⊢ (((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → ∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤))
135	86, 87, 88, 134	19.9d2rf 31463	. . . . . 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 7410	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → (𝑣 +_𝑒 𝑤) ∈ ( +_𝑒 “ (𝑋 × 𝑌)))
142	1	eleq2d 2818	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑣 +_𝑒 𝑤) ∈ 𝑍 ↔ (𝑣 +_𝑒 𝑤) ∈ ( +_𝑒 “ (𝑋 × 𝑌))))
143	142	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → ((𝑣 +_𝑒 𝑤) ∈ 𝑍 ↔ (𝑣 +_𝑒 𝑤) ∈ ( +_𝑒 “ (𝑋 × 𝑌))))
144	141, 143	mpbird 256	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → (𝑣 +_𝑒 𝑤) ∈ 𝑍)
145		simpr 485	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) ∧ 𝑘 = (𝑣 +_𝑒 𝑤)) → 𝑘 = (𝑣 +_𝑒 𝑤))
146	145	breq2d 5122	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) ∧ 𝑘 = (𝑣 +_𝑒 𝑤)) → (𝑧 < 𝑘 ↔ 𝑧 < (𝑣 +_𝑒 𝑤)))
147	144, 146	rspcedv 3575	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → (𝑧 < (𝑣 +_𝑒 𝑤) → ∃𝑘 ∈ 𝑍 𝑧 < 𝑘))
148	147	rexlimdvva 3201	. . . . . 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 3139	. 2 ⊢ (𝜑 → ∀𝑧 ∈ ℝ (𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) → ∃𝑘 ∈ 𝑍 𝑧 < 𝑘))
153		supxr2 13243	. 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 2939 ∀wral 3060 ∃wrex 3069 ⊆ wss 3913 ⟨cop 4597 class class class wbr 5110 × cxp 5636 dom cdm 5638 “ cima 5641 Fun wfun 6495 ⟶wf 6497 ‘cfv 6501 (class class class)co 7362 supcsup 9385 ℝcr 11059 -∞cmnf 11196 ℝ^*cxr 11197 < clt 11198 ≤ cle 11199 +_𝑒 cxad 13040

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 2702 ax-sep 5261 ax-nul 5268 ax-pow 5325 ax-pr 5389 ax-un 7677 ax-cnex 11116 ax-resscn 11117 ax-1cn 11118 ax-icn 11119 ax-addcl 11120 ax-addrcl 11121 ax-mulcl 11122 ax-mulrcl 11123 ax-mulcom 11124 ax-addass 11125 ax-mulass 11126 ax-distr 11127 ax-i2m1 11128 ax-1ne0 11129 ax-1rid 11130 ax-rnegex 11131 ax-rrecex 11132 ax-cnre 11133 ax-pre-lttri 11134 ax-pre-lttrn 11135 ax-pre-ltadd 11136 ax-pre-mulgt0 11137 ax-pre-sup 11138

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 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3351 df-reu 3352 df-rab 3406 df-v 3448 df-sbc 3743 df-csb 3859 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4288 df-if 4492 df-pw 4567 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4871 df-iun 4961 df-br 5111 df-opab 5173 df-mpt 5194 df-id 5536 df-po 5550 df-so 5551 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-iota 6453 df-fun 6503 df-fn 6504 df-f 6505 df-f1 6506 df-fo 6507 df-f1o 6508 df-fv 6509 df-riota 7318 df-ov 7365 df-oprab 7366 df-mpo 7367 df-1st 7926 df-2nd 7927 df-er 8655 df-en 8891 df-dom 8892 df-sdom 8893 df-sup 9387 df-pnf 11200 df-mnf 11201 df-xr 11202 df-ltxr 11203 df-le 11204 df-sub 11396 df-neg 11397 df-div 11822 df-2 12225 df-rp 12925 df-xneg 13042 df-xadd 13043

This theorem is referenced by: (None)

W3C validator