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 31086

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 3925	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝑋 → 𝑥 ∈ ℝ^*))
4		xrofsup.2	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ⊆ ℝ^*)
5	4	sseld 3925	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ 𝑌 → 𝑦 ∈ ℝ^*))
6	3, 5	anim12d 609	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → (𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*)))
7	6	imp 407	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*))
8		xaddcl 12972	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → (𝑥 +_𝑒 𝑦) ∈ ℝ^)
9	7, 8	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑥 +_𝑒 𝑦) ∈ ℝ^*)
10	9	ralrimivva 3117	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝑥 +_𝑒 𝑦) ∈ ℝ^*)
11		fveq2 6771	. . . . . . . 8 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → ( +_𝑒 ‘𝑢) = ( +_𝑒 ‘⟨𝑥, 𝑦⟩))
12		df-ov 7274	. . . . . . . 8 ⊢ (𝑥 +_𝑒 𝑦) = ( +_𝑒 ‘⟨𝑥, 𝑦⟩)
13	11, 12	eqtr4di 2798	. . . . . . 7 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → ( +_𝑒 ‘𝑢) = (𝑥 +_𝑒 𝑦))
14	13	eleq1d 2825	. . . . . 6 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → (( +_𝑒 ‘𝑢) ∈ ℝ^* ↔ (𝑥 +_𝑒 𝑦) ∈ ℝ^*))
15	14	ralxp 5749	. . . . 5 ⊢ (∀𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) ∈ ℝ^* ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝑥 +_𝑒 𝑦) ∈ ℝ^*)
16	10, 15	sylibr 233	. . . 4 ⊢ (𝜑 → ∀𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) ∈ ℝ^*)
17		xaddf 12957	. . . . . 6 ⊢ +_𝑒 :(ℝ^* × ℝ^)⟶ℝ^
18		ffun 6601	. . . . . 6 ⊢ ( +_𝑒 :(ℝ^* × ℝ^)⟶ℝ^ → Fun +_𝑒 )
19	17, 18	ax-mp 5	. . . . 5 ⊢ Fun +_𝑒
20		xpss12 5605	. . . . . . 7 ⊢ ((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) → (𝑋 × 𝑌) ⊆ (ℝ^ × ℝ^*))
21	2, 4, 20	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (𝑋 × 𝑌) ⊆ (ℝ^* × ℝ^*))
22	17	fdmi 6610	. . . . . 6 ⊢ dom +_𝑒 = (ℝ^* × ℝ^*)
23	21, 22	sseqtrrdi 3977	. . . . 5 ⊢ (𝜑 → (𝑋 × 𝑌) ⊆ dom +_𝑒 )
24		funimass4 6831	. . . . 5 ⊢ ((Fun +_𝑒 ∧ (𝑋 × 𝑌) ⊆ dom +_𝑒 ) → (( +_𝑒 “ (𝑋 × 𝑌)) ⊆ ℝ^* ↔ ∀𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) ∈ ℝ^*))
25	19, 23, 24	sylancr 587	. . . 4 ⊢ (𝜑 → (( +_𝑒 “ (𝑋 × 𝑌)) ⊆ ℝ^* ↔ ∀𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) ∈ ℝ^*))
26	16, 25	mpbird 256	. . 3 ⊢ (𝜑 → ( +_𝑒 “ (𝑋 × 𝑌)) ⊆ ℝ^*)
27	1, 26	eqsstrd 3964	. 2 ⊢ (𝜑 → 𝑍 ⊆ ℝ^*)
28		supxrcl 13048	. . . 4 ⊢ (𝑋 ⊆ ℝ^* → sup(𝑋, ℝ^, < ) ∈ ℝ^)
29	2, 28	syl 17	. . 3 ⊢ (𝜑 → sup(𝑋, ℝ^, < ) ∈ ℝ^)
30		supxrcl 13048	. . . 4 ⊢ (𝑌 ⊆ ℝ^* → sup(𝑌, ℝ^, < ) ∈ ℝ^)
31	4, 30	syl 17	. . 3 ⊢ (𝜑 → sup(𝑌, ℝ^, < ) ∈ ℝ^)
32	29, 31	xaddcld 13034	. 2 ⊢ (𝜑 → (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) ∈ ℝ^*)
33	1	eleq2d 2826	. . . . 5 ⊢ (𝜑 → (𝑧 ∈ 𝑍 ↔ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))))
34	33	pm5.32i 575	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑍) ↔ (𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))))
35		nfvd 1922	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → Ⅎ𝑥 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
36		nfvd 1922	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → Ⅎ𝑦 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
37	2	ad2antrr 723	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑋 ⊆ ℝ^*)
38		simprl 768	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑥 ∈ 𝑋)
39		supxrub 13057	. . . . . . . . . . 11 ⊢ ((𝑋 ⊆ ℝ^* ∧ 𝑥 ∈ 𝑋) → 𝑥 ≤ sup(𝑋, ℝ^*, < ))
40	37, 38, 39	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑥 ≤ sup(𝑋, ℝ^*, < ))
41	4	ad2antrr 723	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑌 ⊆ ℝ^*)
42		simprr 770	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑦 ∈ 𝑌)
43		supxrub 13057	. . . . . . . . . . 11 ⊢ ((𝑌 ⊆ ℝ^* ∧ 𝑦 ∈ 𝑌) → 𝑦 ≤ sup(𝑌, ℝ^*, < ))
44	41, 42, 43	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑦 ≤ sup(𝑌, ℝ^*, < ))
45	37, 38	sseldd 3927	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑥 ∈ ℝ^*)
46	41, 42	sseldd 3927	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑦 ∈ ℝ^*)
47	37, 28	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → sup(𝑋, ℝ^, < ) ∈ ℝ^)
48	41, 30	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → sup(𝑌, ℝ^, < ) ∈ ℝ^)
49		xle2add 12992	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) ∧ (sup(𝑋, ℝ^, < ) ∈ ℝ^* ∧ sup(𝑌, ℝ^, < ) ∈ ℝ^)) → ((𝑥 ≤ sup(𝑋, ℝ^, < ) ∧ 𝑦 ≤ sup(𝑌, ℝ^, < )) → (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))))
50	45, 46, 47, 48, 49	syl22anc 836	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑥 ≤ sup(𝑋, ℝ^, < ) ∧ 𝑦 ≤ sup(𝑌, ℝ^, < )) → (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))))
51	40, 44, 50	mp2and 696	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
52	51	ralrimivva 3117	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
53		fvelima 6832	. . . . . . . . . . 11 ⊢ ((Fun +_𝑒 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → ∃𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) = 𝑧)
54	19, 53	mpan 687	. . . . . . . . . 10 ⊢ (𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌)) → ∃𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) = 𝑧)
55	54	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → ∃𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) = 𝑧)
56	13	eqeq1d 2742	. . . . . . . . . 10 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → (( +_𝑒 ‘𝑢) = 𝑧 ↔ (𝑥 +_𝑒 𝑦) = 𝑧))
57	56	rexxp 5750	. . . . . . . . 9 ⊢ (∃𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) = 𝑧 ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 (𝑥 +_𝑒 𝑦) = 𝑧)
58	55, 57	sylib 217	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 (𝑥 +_𝑒 𝑦) = 𝑧)
59	52, 58	r19.29d2r 3264	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ((𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) ∧ (𝑥 +_𝑒 𝑦) = 𝑧))
60		ancom 461	. . . . . . . 8 ⊢ (((𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) ∧ (𝑥 +_𝑒 𝑦) = 𝑧) ↔ ((𝑥 +_𝑒 𝑦) = 𝑧 ∧ (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))))
61	60	2rexbii 3181	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ((𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) ∧ (𝑥 +_𝑒 𝑦) = 𝑧) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ((𝑥 +_𝑒 𝑦) = 𝑧 ∧ (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))))
62	59, 61	sylib 217	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ((𝑥 +_𝑒 𝑦) = 𝑧 ∧ (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))))
63		breq1 5082	. . . . . . . . 9 ⊢ ((𝑥 +_𝑒 𝑦) = 𝑧 → ((𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) ↔ 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))))
64	63	biimpa 477	. . . . . . . 8 ⊢ (((𝑥 +_𝑒 𝑦) = 𝑧 ∧ (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
65	64	reximi 3177	. . . . . . 7 ⊢ (∃𝑦 ∈ 𝑌 ((𝑥 +_𝑒 𝑦) = 𝑧 ∧ (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → ∃𝑦 ∈ 𝑌 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
66	65	reximi 3177	. . . . . 6 ⊢ (∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ((𝑥 +_𝑒 𝑦) = 𝑧 ∧ (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
67	62, 66	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
68	35, 36, 67	19.9d2r 30817	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
69	34, 68	sylbi 216	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑍) → 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
70	69	ralrimiva 3110	. 2 ⊢ (𝜑 → ∀𝑧 ∈ 𝑍 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
71	2	ad2antrr 723	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → 𝑋 ⊆ ℝ^*)
72	4	ad2antrr 723	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → 𝑌 ⊆ ℝ^*)
73		simplr 766	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → 𝑧 ∈ ℝ)
74	29	ad2antrr 723	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → sup(𝑋, ℝ^, < ) ∈ ℝ^)
75	31	ad2antrr 723	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → sup(𝑌, ℝ^, < ) ∈ ℝ^)
76		xrofsup.3	. . . . . . . 8 ⊢ (𝜑 → sup(𝑋, ℝ^*, < ) ≠ -∞)
77	76	ad2antrr 723	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → sup(𝑋, ℝ^*, < ) ≠ -∞)
78		xrofsup.4	. . . . . . . 8 ⊢ (𝜑 → sup(𝑌, ℝ^*, < ) ≠ -∞)
79	78	ad2antrr 723	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → sup(𝑌, ℝ^*, < ) ≠ -∞)
80		simpr 485	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
81	73, 74, 75, 77, 79, 80	xlt2addrd 31077	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → ∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))
82		nfv 1921	. . . . . . . 8 ⊢ Ⅎ𝑏(𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^*)
83		nfcv 2909	. . . . . . . . 9 ⊢ Ⅎ𝑏ℝ^*
84		nfre1 3237	. . . . . . . . 9 ⊢ Ⅎ𝑏∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))
85	83, 84	nfrex 3240	. . . . . . . 8 ⊢ Ⅎ𝑏∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))
86	82, 85	nfan 1906	. . . . . . 7 ⊢ Ⅎ𝑏((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))
87		nfvd 1922	. . . . . . 7 ⊢ (((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → Ⅎ𝑎∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤))
88		nfvd 1922	. . . . . . 7 ⊢ (((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → Ⅎ𝑏∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤))
89		id 22	. . . . . . . . . . . 12 ⊢ ((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) → (𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^*))
90	89	ralrimivw 3111	. . . . . . . . . . 11 ⊢ ((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) → ∀𝑏 ∈ ℝ^ (𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^*))
91	90	ralrimivw 3111	. . . . . . . . . 10 ⊢ ((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) → ∀𝑎 ∈ ℝ^ ∀𝑏 ∈ ℝ^* (𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^*))
92	91	adantr 481	. . . . . . . . 9 ⊢ (((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → ∀𝑎 ∈ ℝ^* ∀𝑏 ∈ ℝ^* (𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^*))
93		simpr 485	. . . . . . . . 9 ⊢ (((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → ∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))
94	92, 93	r19.29d2r 3264	. . . . . . . 8 ⊢ (((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → ∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* ((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < ))))
95		simplrr 775	. . . . . . . . . . . . . . 15 ⊢ ((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌 ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤))) → (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))
96	95	3anassrs 1359	. . . . . . . . . . . . . 14 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))
97	96	simp1d 1141	. . . . . . . . . . . . 13 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑧 = (𝑎 +_𝑒 𝑏))
98		simp-4l 780	. . . . . . . . . . . . . 14 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^*))
99		simplrl 774	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌 ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤))) → (𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^*))
100	99	3anassrs 1359	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → (𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^*))
101	100	simpld 495	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑋 ⊆ ℝ^)
102		simpllr 773	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑣 ∈ 𝑋)
103	101, 102	sseldd 3927	. . . . . . . . . . . . . 14 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑣 ∈ ℝ^)
104	100	simprd 496	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑌 ⊆ ℝ^)
105		simplr 766	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑤 ∈ 𝑌)
106	104, 105	sseldd 3927	. . . . . . . . . . . . . 14 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑤 ∈ ℝ^)
107	98, 103, 106	jca32 516	. . . . . . . . . . . . 13 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → ((𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^) ∧ (𝑣 ∈ ℝ^ ∧ 𝑤 ∈ ℝ^*)))
108		simpr 485	. . . . . . . . . . . . 13 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → (𝑎 < 𝑣 ∧ 𝑏 < 𝑤))
109		xlt2add 12993	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ (𝑣 ∈ ℝ^ ∧ 𝑤 ∈ ℝ^*)) → ((𝑎 < 𝑣 ∧ 𝑏 < 𝑤) → (𝑎 +_𝑒 𝑏) < (𝑣 +_𝑒 𝑤)))
110	109	imp 407	. . . . . . . . . . . . . 14 ⊢ ((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ (𝑣 ∈ ℝ^ ∧ 𝑤 ∈ ℝ^*)) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → (𝑎 +_𝑒 𝑏) < (𝑣 +_𝑒 𝑤))
111		breq1 5082	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑎 +_𝑒 𝑏) → (𝑧 < (𝑣 +_𝑒 𝑤) ↔ (𝑎 +_𝑒 𝑏) < (𝑣 +_𝑒 𝑤)))
112	111	biimpar 478	. . . . . . . . . . . . . 14 ⊢ ((𝑧 = (𝑎 +_𝑒 𝑏) ∧ (𝑎 +_𝑒 𝑏) < (𝑣 +_𝑒 𝑤)) → 𝑧 < (𝑣 +_𝑒 𝑤))
113	110, 112	sylan2 593	. . . . . . . . . . . . 13 ⊢ ((𝑧 = (𝑎 +_𝑒 𝑏) ∧ (((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ (𝑣 ∈ ℝ^ ∧ 𝑤 ∈ ℝ^*)) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤))) → 𝑧 < (𝑣 +_𝑒 𝑤))
114	97, 107, 108, 113	syl12anc 834	. . . . . . . . . . . 12 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑧 < (𝑣 +_𝑒 𝑤))
115		simplll 772	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^)) → 𝑋 ⊆ ℝ^)
116		simprl 768	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^)) → 𝑎 ∈ ℝ^)
117		simplr2 1215	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^)) → 𝑎 < sup(𝑋, ℝ^, < ))
118		supxrlub 13058	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ⊆ ℝ^* ∧ 𝑎 ∈ ℝ^) → (𝑎 < sup(𝑋, ℝ^, < ) ↔ ∃𝑣 ∈ 𝑋 𝑎 < 𝑣))
119	118	biimpa 477	. . . . . . . . . . . . . . 15 ⊢ (((𝑋 ⊆ ℝ^* ∧ 𝑎 ∈ ℝ^) ∧ 𝑎 < sup(𝑋, ℝ^, < )) → ∃𝑣 ∈ 𝑋 𝑎 < 𝑣)
120	115, 116, 117, 119	syl21anc 835	. . . . . . . . . . . . . 14 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^*)) → ∃𝑣 ∈ 𝑋 𝑎 < 𝑣)
121		simpllr 773	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^)) → 𝑌 ⊆ ℝ^)
122		simprr 770	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^)) → 𝑏 ∈ ℝ^)
123		simplr3 1216	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^)) → 𝑏 < sup(𝑌, ℝ^, < ))
124		supxrlub 13058	. . . . . . . . . . . . . . . 16 ⊢ ((𝑌 ⊆ ℝ^* ∧ 𝑏 ∈ ℝ^) → (𝑏 < sup(𝑌, ℝ^, < ) ↔ ∃𝑤 ∈ 𝑌 𝑏 < 𝑤))
125	124	biimpa 477	. . . . . . . . . . . . . . 15 ⊢ (((𝑌 ⊆ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ 𝑏 < sup(𝑌, ℝ^, < )) → ∃𝑤 ∈ 𝑌 𝑏 < 𝑤)
126	121, 122, 123, 125	syl21anc 835	. . . . . . . . . . . . . 14 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^*)) → ∃𝑤 ∈ 𝑌 𝑏 < 𝑤)
127		reeanv 3295	. . . . . . . . . . . . . 14 ⊢ (∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 (𝑎 < 𝑣 ∧ 𝑏 < 𝑤) ↔ (∃𝑣 ∈ 𝑋 𝑎 < 𝑣 ∧ ∃𝑤 ∈ 𝑌 𝑏 < 𝑤))
128	120, 126, 127	sylanbrc 583	. . . . . . . . . . . . 13 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^*)) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 (𝑎 < 𝑣 ∧ 𝑏 < 𝑤))
129	128	ancoms 459	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 (𝑎 < 𝑣 ∧ 𝑏 < 𝑤))
130	114, 129	reximddv2 3209	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤))
131	130	ex 413	. . . . . . . . . 10 ⊢ ((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) → (((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < ))) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤)))
132	131	reximdva 3205	. . . . . . . . 9 ⊢ (𝑎 ∈ ℝ^* → (∃𝑏 ∈ ℝ^* ((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → ∃𝑏 ∈ ℝ^ ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤)))
133	132	reximia 3175	. . . . . . . 8 ⊢ (∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* ((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤))
134	94, 133	syl 17	. . . . . . 7 ⊢ (((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → ∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤))
135	86, 87, 88, 134	19.9d2rf 30816	. . . . . 6 ⊢ (((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤))
136	71, 72, 81, 135	syl21anc 835	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤))
137		simprl 768	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → 𝑣 ∈ 𝑋)
138		simprr 770	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → 𝑤 ∈ 𝑌)
139	19	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → Fun +_𝑒 )
140	23	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → (𝑋 × 𝑌) ⊆ dom +_𝑒 )
141	137, 138, 139, 140	elovimad 7319	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → (𝑣 +_𝑒 𝑤) ∈ ( +_𝑒 “ (𝑋 × 𝑌)))
142	1	eleq2d 2826	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑣 +_𝑒 𝑤) ∈ 𝑍 ↔ (𝑣 +_𝑒 𝑤) ∈ ( +_𝑒 “ (𝑋 × 𝑌))))
143	142	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → ((𝑣 +_𝑒 𝑤) ∈ 𝑍 ↔ (𝑣 +_𝑒 𝑤) ∈ ( +_𝑒 “ (𝑋 × 𝑌))))
144	141, 143	mpbird 256	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → (𝑣 +_𝑒 𝑤) ∈ 𝑍)
145		simpr 485	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) ∧ 𝑘 = (𝑣 +_𝑒 𝑤)) → 𝑘 = (𝑣 +_𝑒 𝑤))
146	145	breq2d 5091	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) ∧ 𝑘 = (𝑣 +_𝑒 𝑤)) → (𝑧 < 𝑘 ↔ 𝑧 < (𝑣 +_𝑒 𝑤)))
147	144, 146	rspcedv 3553	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → (𝑧 < (𝑣 +_𝑒 𝑤) → ∃𝑘 ∈ 𝑍 𝑧 < 𝑘))
148	147	rexlimdvva 3225	. . . . . 6 ⊢ (𝜑 → (∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤) → ∃𝑘 ∈ 𝑍 𝑧 < 𝑘))
149	148	ad2antrr 723	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → (∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤) → ∃𝑘 ∈ 𝑍 𝑧 < 𝑘))
150	136, 149	mpd 15	. . . 4 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → ∃𝑘 ∈ 𝑍 𝑧 < 𝑘)
151	150	ex 413	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → (𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) → ∃𝑘 ∈ 𝑍 𝑧 < 𝑘))
152	151	ralrimiva 3110	. 2 ⊢ (𝜑 → ∀𝑧 ∈ ℝ (𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) → ∃𝑘 ∈ 𝑍 𝑧 < 𝑘))
153		supxr2 13047	. 2 ⊢ (((𝑍 ⊆ ℝ^* ∧ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) ∈ ℝ^) ∧ (∀𝑧 ∈ 𝑍 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) ∧ ∀𝑧 ∈ ℝ (𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) → ∃𝑘 ∈ 𝑍 𝑧 < 𝑘))) → sup(𝑍, ℝ^, < ) = (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
154	27, 32, 70, 152, 153	syl22anc 836	1 ⊢ (𝜑 → sup(𝑍, ℝ^, < ) = (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^*, < )))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1086 = wceq 1542 ∈ wcel 2110 ≠ wne 2945 ∀wral 3066 ∃wrex 3067 ⊆ wss 3892 ⟨cop 4573 class class class wbr 5079 × cxp 5588 dom cdm 5590 “ cima 5593 Fun wfun 6426 ⟶wf 6428 ‘cfv 6432 (class class class)co 7271 supcsup 9177 ℝcr 10871 -∞cmnf 11008 ℝ^*cxr 11009 < clt 11010 ≤ cle 11011 +_𝑒 cxad 12845

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2015 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2711 ax-sep 5227 ax-nul 5234 ax-pow 5292 ax-pr 5356 ax-un 7582 ax-cnex 10928 ax-resscn 10929 ax-1cn 10930 ax-icn 10931 ax-addcl 10932 ax-addrcl 10933 ax-mulcl 10934 ax-mulrcl 10935 ax-mulcom 10936 ax-addass 10937 ax-mulass 10938 ax-distr 10939 ax-i2m1 10940 ax-1ne0 10941 ax-1rid 10942 ax-rnegex 10943 ax-rrecex 10944 ax-cnre 10945 ax-pre-lttri 10946 ax-pre-lttrn 10947 ax-pre-ltadd 10948 ax-pre-mulgt0 10949 ax-pre-sup 10950

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2072 df-mo 2542 df-eu 2571 df-clab 2718 df-cleq 2732 df-clel 2818 df-nfc 2891 df-ne 2946 df-nel 3052 df-ral 3071 df-rex 3072 df-reu 3073 df-rmo 3074 df-rab 3075 df-v 3433 df-sbc 3721 df-csb 3838 df-dif 3895 df-un 3897 df-in 3899 df-ss 3909 df-nul 4263 df-if 4466 df-pw 4541 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4846 df-iun 4932 df-br 5080 df-opab 5142 df-mpt 5163 df-id 5490 df-po 5504 df-so 5505 df-xp 5596 df-rel 5597 df-cnv 5598 df-co 5599 df-dm 5600 df-rn 5601 df-res 5602 df-ima 5603 df-iota 6390 df-fun 6434 df-fn 6435 df-f 6436 df-f1 6437 df-fo 6438 df-f1o 6439 df-fv 6440 df-riota 7228 df-ov 7274 df-oprab 7275 df-mpo 7276 df-1st 7824 df-2nd 7825 df-er 8481 df-en 8717 df-dom 8718 df-sdom 8719 df-sup 9179 df-pnf 11012 df-mnf 11013 df-xr 11014 df-ltxr 11015 df-le 11016 df-sub 11207 df-neg 11208 df-div 11633 df-2 12036 df-rp 12730 df-xneg 12847 df-xadd 12848

This theorem is referenced by: (None)

W3C validator