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 30486

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 3966	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝑋 → 𝑥 ∈ ℝ^*))
4		xrofsup.2	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ⊆ ℝ^*)
5	4	sseld 3966	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ 𝑌 → 𝑦 ∈ ℝ^*))
6	3, 5	anim12d 610	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → (𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*)))
7	6	imp 409	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*))
8		xaddcl 12626	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → (𝑥 +_𝑒 𝑦) ∈ ℝ^)
9	7, 8	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑥 +_𝑒 𝑦) ∈ ℝ^*)
10	9	ralrimivva 3191	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝑥 +_𝑒 𝑦) ∈ ℝ^*)
11		fveq2 6665	. . . . . . . 8 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → ( +_𝑒 ‘𝑢) = ( +_𝑒 ‘⟨𝑥, 𝑦⟩))
12		df-ov 7153	. . . . . . . 8 ⊢ (𝑥 +_𝑒 𝑦) = ( +_𝑒 ‘⟨𝑥, 𝑦⟩)
13	11, 12	syl6eqr 2874	. . . . . . 7 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → ( +_𝑒 ‘𝑢) = (𝑥 +_𝑒 𝑦))
14	13	eleq1d 2897	. . . . . 6 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → (( +_𝑒 ‘𝑢) ∈ ℝ^* ↔ (𝑥 +_𝑒 𝑦) ∈ ℝ^*))
15	14	ralxp 5707	. . . . 5 ⊢ (∀𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) ∈ ℝ^* ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝑥 +_𝑒 𝑦) ∈ ℝ^*)
16	10, 15	sylibr 236	. . . 4 ⊢ (𝜑 → ∀𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) ∈ ℝ^*)
17		xaddf 12611	. . . . . 6 ⊢ +_𝑒 :(ℝ^* × ℝ^)⟶ℝ^
18		ffun 6512	. . . . . 6 ⊢ ( +_𝑒 :(ℝ^* × ℝ^)⟶ℝ^ → Fun +_𝑒 )
19	17, 18	ax-mp 5	. . . . 5 ⊢ Fun +_𝑒
20		xpss12 5565	. . . . . . 7 ⊢ ((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) → (𝑋 × 𝑌) ⊆ (ℝ^ × ℝ^*))
21	2, 4, 20	syl2anc 586	. . . . . 6 ⊢ (𝜑 → (𝑋 × 𝑌) ⊆ (ℝ^* × ℝ^*))
22	17	fdmi 6519	. . . . . 6 ⊢ dom +_𝑒 = (ℝ^* × ℝ^*)
23	21, 22	sseqtrrdi 4018	. . . . 5 ⊢ (𝜑 → (𝑋 × 𝑌) ⊆ dom +_𝑒 )
24		funimass4 6725	. . . . 5 ⊢ ((Fun +_𝑒 ∧ (𝑋 × 𝑌) ⊆ dom +_𝑒 ) → (( +_𝑒 “ (𝑋 × 𝑌)) ⊆ ℝ^* ↔ ∀𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) ∈ ℝ^*))
25	19, 23, 24	sylancr 589	. . . 4 ⊢ (𝜑 → (( +_𝑒 “ (𝑋 × 𝑌)) ⊆ ℝ^* ↔ ∀𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) ∈ ℝ^*))
26	16, 25	mpbird 259	. . 3 ⊢ (𝜑 → ( +_𝑒 “ (𝑋 × 𝑌)) ⊆ ℝ^*)
27	1, 26	eqsstrd 4005	. 2 ⊢ (𝜑 → 𝑍 ⊆ ℝ^*)
28		supxrcl 12702	. . . 4 ⊢ (𝑋 ⊆ ℝ^* → sup(𝑋, ℝ^, < ) ∈ ℝ^)
29	2, 28	syl 17	. . 3 ⊢ (𝜑 → sup(𝑋, ℝ^, < ) ∈ ℝ^)
30		supxrcl 12702	. . . 4 ⊢ (𝑌 ⊆ ℝ^* → sup(𝑌, ℝ^, < ) ∈ ℝ^)
31	4, 30	syl 17	. . 3 ⊢ (𝜑 → sup(𝑌, ℝ^, < ) ∈ ℝ^)
32	29, 31	xaddcld 12688	. 2 ⊢ (𝜑 → (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) ∈ ℝ^*)
33	1	eleq2d 2898	. . . . 5 ⊢ (𝜑 → (𝑧 ∈ 𝑍 ↔ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))))
34	33	pm5.32i 577	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑍) ↔ (𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))))
35		nfvd 1912	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → Ⅎ𝑥 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
36		nfvd 1912	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → Ⅎ𝑦 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
37	2	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑋 ⊆ ℝ^*)
38		simprl 769	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑥 ∈ 𝑋)
39		supxrub 12711	. . . . . . . . . . 11 ⊢ ((𝑋 ⊆ ℝ^* ∧ 𝑥 ∈ 𝑋) → 𝑥 ≤ sup(𝑋, ℝ^*, < ))
40	37, 38, 39	syl2anc 586	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑥 ≤ sup(𝑋, ℝ^*, < ))
41	4	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑌 ⊆ ℝ^*)
42		simprr 771	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑦 ∈ 𝑌)
43		supxrub 12711	. . . . . . . . . . 11 ⊢ ((𝑌 ⊆ ℝ^* ∧ 𝑦 ∈ 𝑌) → 𝑦 ≤ sup(𝑌, ℝ^*, < ))
44	41, 42, 43	syl2anc 586	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑦 ≤ sup(𝑌, ℝ^*, < ))
45	37, 38	sseldd 3968	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑥 ∈ ℝ^*)
46	41, 42	sseldd 3968	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑦 ∈ ℝ^*)
47	37, 28	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → sup(𝑋, ℝ^, < ) ∈ ℝ^)
48	41, 30	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → sup(𝑌, ℝ^, < ) ∈ ℝ^)
49		xle2add 12646	. . . . . . . . . . 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 697	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
52	51	ralrimivva 3191	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
53		fvelima 6726	. . . . . . . . . . 11 ⊢ ((Fun +_𝑒 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → ∃𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) = 𝑧)
54	19, 53	mpan 688	. . . . . . . . . 10 ⊢ (𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌)) → ∃𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) = 𝑧)
55	54	adantl 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → ∃𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) = 𝑧)
56	13	eqeq1d 2823	. . . . . . . . . 10 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → (( +_𝑒 ‘𝑢) = 𝑧 ↔ (𝑥 +_𝑒 𝑦) = 𝑧))
57	56	rexxp 5708	. . . . . . . . 9 ⊢ (∃𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) = 𝑧 ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 (𝑥 +_𝑒 𝑦) = 𝑧)
58	55, 57	sylib 220	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 (𝑥 +_𝑒 𝑦) = 𝑧)
59	52, 58	r19.29d2r 3335	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ((𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) ∧ (𝑥 +_𝑒 𝑦) = 𝑧))
60		ancom 463	. . . . . . . 8 ⊢ (((𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) ∧ (𝑥 +_𝑒 𝑦) = 𝑧) ↔ ((𝑥 +_𝑒 𝑦) = 𝑧 ∧ (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))))
61	60	2rexbii 3248	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ((𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) ∧ (𝑥 +_𝑒 𝑦) = 𝑧) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ((𝑥 +_𝑒 𝑦) = 𝑧 ∧ (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))))
62	59, 61	sylib 220	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ((𝑥 +_𝑒 𝑦) = 𝑧 ∧ (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))))
63		breq1 5062	. . . . . . . . 9 ⊢ ((𝑥 +_𝑒 𝑦) = 𝑧 → ((𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) ↔ 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))))
64	63	biimpa 479	. . . . . . . 8 ⊢ (((𝑥 +_𝑒 𝑦) = 𝑧 ∧ (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
65	64	reximi 3243	. . . . . . 7 ⊢ (∃𝑦 ∈ 𝑌 ((𝑥 +_𝑒 𝑦) = 𝑧 ∧ (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → ∃𝑦 ∈ 𝑌 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
66	65	reximi 3243	. . . . . 6 ⊢ (∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ((𝑥 +_𝑒 𝑦) = 𝑧 ∧ (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
67	62, 66	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
68	35, 36, 67	19.9d2r 30230	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
69	34, 68	sylbi 219	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑍) → 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
70	69	ralrimiva 3182	. 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 487	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
81	73, 74, 75, 77, 79, 80	xlt2addrd 30476	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → ∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))
82		nfv 1911	. . . . . . . 8 ⊢ Ⅎ𝑏(𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^*)
83		nfcv 2977	. . . . . . . . 9 ⊢ Ⅎ𝑏ℝ^*
84		nfre1 3306	. . . . . . . . 9 ⊢ Ⅎ𝑏∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))
85	83, 84	nfrex 3309	. . . . . . . 8 ⊢ Ⅎ𝑏∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))
86	82, 85	nfan 1896	. . . . . . 7 ⊢ Ⅎ𝑏((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))
87		nfvd 1912	. . . . . . 7 ⊢ (((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → Ⅎ𝑎∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤))
88		nfvd 1912	. . . . . . 7 ⊢ (((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → Ⅎ𝑏∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤))
89		id 22	. . . . . . . . . . . 12 ⊢ ((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) → (𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^*))
90	89	ralrimivw 3183	. . . . . . . . . . 11 ⊢ ((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) → ∀𝑏 ∈ ℝ^ (𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^*))
91	90	ralrimivw 3183	. . . . . . . . . 10 ⊢ ((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) → ∀𝑎 ∈ ℝ^ ∀𝑏 ∈ ℝ^* (𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^*))
92	91	adantr 483	. . . . . . . . 9 ⊢ (((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → ∀𝑎 ∈ ℝ^* ∀𝑏 ∈ ℝ^* (𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^*))
93		simpr 487	. . . . . . . . 9 ⊢ (((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → ∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))
94	92, 93	r19.29d2r 3335	. . . . . . . 8 ⊢ (((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → ∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* ((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < ))))
95		simplrr 776	. . . . . . . . . . . . . . 15 ⊢ ((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌 ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤))) → (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))
96	95	3anassrs 1356	. . . . . . . . . . . . . 14 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))
97	96	simp1d 1138	. . . . . . . . . . . . 13 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑧 = (𝑎 +_𝑒 𝑏))
98		simp-4l 781	. . . . . . . . . . . . . 14 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^*))
99		simplrl 775	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌 ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤))) → (𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^*))
100	99	3anassrs 1356	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → (𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^*))
101	100	simpld 497	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑋 ⊆ ℝ^)
102		simpllr 774	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑣 ∈ 𝑋)
103	101, 102	sseldd 3968	. . . . . . . . . . . . . 14 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑣 ∈ ℝ^)
104	100	simprd 498	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑌 ⊆ ℝ^)
105		simplr 767	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑤 ∈ 𝑌)
106	104, 105	sseldd 3968	. . . . . . . . . . . . . 14 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑤 ∈ ℝ^)
107	98, 103, 106	jca32 518	. . . . . . . . . . . . 13 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → ((𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^) ∧ (𝑣 ∈ ℝ^ ∧ 𝑤 ∈ ℝ^*)))
108		simpr 487	. . . . . . . . . . . . 13 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → (𝑎 < 𝑣 ∧ 𝑏 < 𝑤))
109		xlt2add 12647	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ (𝑣 ∈ ℝ^ ∧ 𝑤 ∈ ℝ^*)) → ((𝑎 < 𝑣 ∧ 𝑏 < 𝑤) → (𝑎 +_𝑒 𝑏) < (𝑣 +_𝑒 𝑤)))
110	109	imp 409	. . . . . . . . . . . . . 14 ⊢ ((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ (𝑣 ∈ ℝ^ ∧ 𝑤 ∈ ℝ^*)) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → (𝑎 +_𝑒 𝑏) < (𝑣 +_𝑒 𝑤))
111		breq1 5062	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑎 +_𝑒 𝑏) → (𝑧 < (𝑣 +_𝑒 𝑤) ↔ (𝑎 +_𝑒 𝑏) < (𝑣 +_𝑒 𝑤)))
112	111	biimpar 480	. . . . . . . . . . . . . 14 ⊢ ((𝑧 = (𝑎 +_𝑒 𝑏) ∧ (𝑎 +_𝑒 𝑏) < (𝑣 +_𝑒 𝑤)) → 𝑧 < (𝑣 +_𝑒 𝑤))
113	110, 112	sylan2 594	. . . . . . . . . . . . 13 ⊢ ((𝑧 = (𝑎 +_𝑒 𝑏) ∧ (((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ (𝑣 ∈ ℝ^ ∧ 𝑤 ∈ ℝ^*)) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤))) → 𝑧 < (𝑣 +_𝑒 𝑤))
114	97, 107, 108, 113	syl12anc 834	. . . . . . . . . . . 12 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑧 < (𝑣 +_𝑒 𝑤))
115		simplll 773	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^)) → 𝑋 ⊆ ℝ^)
116		simprl 769	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^)) → 𝑎 ∈ ℝ^)
117		simplr2 1212	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^)) → 𝑎 < sup(𝑋, ℝ^, < ))
118		supxrlub 12712	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ⊆ ℝ^* ∧ 𝑎 ∈ ℝ^) → (𝑎 < sup(𝑋, ℝ^, < ) ↔ ∃𝑣 ∈ 𝑋 𝑎 < 𝑣))
119	118	biimpa 479	. . . . . . . . . . . . . . 15 ⊢ (((𝑋 ⊆ ℝ^* ∧ 𝑎 ∈ ℝ^) ∧ 𝑎 < sup(𝑋, ℝ^, < )) → ∃𝑣 ∈ 𝑋 𝑎 < 𝑣)
120	115, 116, 117, 119	syl21anc 835	. . . . . . . . . . . . . 14 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^*)) → ∃𝑣 ∈ 𝑋 𝑎 < 𝑣)
121		simpllr 774	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^)) → 𝑌 ⊆ ℝ^)
122		simprr 771	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^)) → 𝑏 ∈ ℝ^)
123		simplr3 1213	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^)) → 𝑏 < sup(𝑌, ℝ^, < ))
124		supxrlub 12712	. . . . . . . . . . . . . . . 16 ⊢ ((𝑌 ⊆ ℝ^* ∧ 𝑏 ∈ ℝ^) → (𝑏 < sup(𝑌, ℝ^, < ) ↔ ∃𝑤 ∈ 𝑌 𝑏 < 𝑤))
125	124	biimpa 479	. . . . . . . . . . . . . . 15 ⊢ (((𝑌 ⊆ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ 𝑏 < sup(𝑌, ℝ^, < )) → ∃𝑤 ∈ 𝑌 𝑏 < 𝑤)
126	121, 122, 123, 125	syl21anc 835	. . . . . . . . . . . . . 14 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^*)) → ∃𝑤 ∈ 𝑌 𝑏 < 𝑤)
127		reeanv 3368	. . . . . . . . . . . . . 14 ⊢ (∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 (𝑎 < 𝑣 ∧ 𝑏 < 𝑤) ↔ (∃𝑣 ∈ 𝑋 𝑎 < 𝑣 ∧ ∃𝑤 ∈ 𝑌 𝑏 < 𝑤))
128	120, 126, 127	sylanbrc 585	. . . . . . . . . . . . 13 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^*)) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 (𝑎 < 𝑣 ∧ 𝑏 < 𝑤))
129	128	ancoms 461	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 (𝑎 < 𝑣 ∧ 𝑏 < 𝑤))
130	114, 129	reximddv2 3278	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤))
131	130	ex 415	. . . . . . . . . 10 ⊢ ((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) → (((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < ))) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤)))
132	131	reximdva 3274	. . . . . . . . 9 ⊢ (𝑎 ∈ ℝ^* → (∃𝑏 ∈ ℝ^* ((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → ∃𝑏 ∈ ℝ^ ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤)))
133	132	reximia 3242	. . . . . . . 8 ⊢ (∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* ((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤))
134	94, 133	syl 17	. . . . . . 7 ⊢ (((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → ∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤))
135	86, 87, 88, 134	19.9d2rf 30229	. . . . . 6 ⊢ (((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤))
136	71, 72, 81, 135	syl21anc 835	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤))
137		simprl 769	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → 𝑣 ∈ 𝑋)
138		simprr 771	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → 𝑤 ∈ 𝑌)
139	19	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → Fun +_𝑒 )
140	23	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → (𝑋 × 𝑌) ⊆ dom +_𝑒 )
141	137, 138, 139, 140	elovimad 7198	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → (𝑣 +_𝑒 𝑤) ∈ ( +_𝑒 “ (𝑋 × 𝑌)))
142	1	eleq2d 2898	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑣 +_𝑒 𝑤) ∈ 𝑍 ↔ (𝑣 +_𝑒 𝑤) ∈ ( +_𝑒 “ (𝑋 × 𝑌))))
143	142	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → ((𝑣 +_𝑒 𝑤) ∈ 𝑍 ↔ (𝑣 +_𝑒 𝑤) ∈ ( +_𝑒 “ (𝑋 × 𝑌))))
144	141, 143	mpbird 259	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → (𝑣 +_𝑒 𝑤) ∈ 𝑍)
145		simpr 487	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) ∧ 𝑘 = (𝑣 +_𝑒 𝑤)) → 𝑘 = (𝑣 +_𝑒 𝑤))
146	145	breq2d 5071	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) ∧ 𝑘 = (𝑣 +_𝑒 𝑤)) → (𝑧 < 𝑘 ↔ 𝑧 < (𝑣 +_𝑒 𝑤)))
147	144, 146	rspcedv 3616	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → (𝑧 < (𝑣 +_𝑒 𝑤) → ∃𝑘 ∈ 𝑍 𝑧 < 𝑘))
148	147	rexlimdvva 3294	. . . . . 6 ⊢ (𝜑 → (∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤) → ∃𝑘 ∈ 𝑍 𝑧 < 𝑘))
149	148	ad2antrr 724	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → (∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤) → ∃𝑘 ∈ 𝑍 𝑧 < 𝑘))
150	136, 149	mpd 15	. . . 4 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → ∃𝑘 ∈ 𝑍 𝑧 < 𝑘)
151	150	ex 415	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → (𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) → ∃𝑘 ∈ 𝑍 𝑧 < 𝑘))
152	151	ralrimiva 3182	. 2 ⊢ (𝜑 → ∀𝑧 ∈ ℝ (𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) → ∃𝑘 ∈ 𝑍 𝑧 < 𝑘))
153		supxr2 12701	. 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 208 ∧ wa 398 ∧ w3a 1083 = wceq 1533 ∈ wcel 2110 ≠ wne 3016 ∀wral 3138 ∃wrex 3139 ⊆ wss 3936 ⟨cop 4567 class class class wbr 5059 × cxp 5548 dom cdm 5550 “ cima 5553 Fun wfun 6344 ⟶wf 6346 ‘cfv 6350 (class class class)co 7150 supcsup 8898 ℝcr 10530 -∞cmnf 10667 ℝ^*cxr 10668 < clt 10669 ≤ cle 10670 +_𝑒 cxad 12499

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2156 ax-12 2172 ax-ext 2793 ax-sep 5196 ax-nul 5203 ax-pow 5259 ax-pr 5322 ax-un 7455 ax-cnex 10587 ax-resscn 10588 ax-1cn 10589 ax-icn 10590 ax-addcl 10591 ax-addrcl 10592 ax-mulcl 10593 ax-mulrcl 10594 ax-mulcom 10595 ax-addass 10596 ax-mulass 10597 ax-distr 10598 ax-i2m1 10599 ax-1ne0 10600 ax-1rid 10601 ax-rnegex 10602 ax-rrecex 10603 ax-cnre 10604 ax-pre-lttri 10605 ax-pre-lttrn 10606 ax-pre-ltadd 10607 ax-pre-mulgt0 10608 ax-pre-sup 10609

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3497 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4833 df-iun 4914 df-br 5060 df-opab 5122 df-mpt 5140 df-id 5455 df-po 5469 df-so 5470 df-xp 5556 df-rel 5557 df-cnv 5558 df-co 5559 df-dm 5560 df-rn 5561 df-res 5562 df-ima 5563 df-iota 6309 df-fun 6352 df-fn 6353 df-f 6354 df-f1 6355 df-fo 6356 df-f1o 6357 df-fv 6358 df-riota 7108 df-ov 7153 df-oprab 7154 df-mpo 7155 df-1st 7683 df-2nd 7684 df-er 8283 df-en 8504 df-dom 8505 df-sdom 8506 df-sup 8900 df-pnf 10671 df-mnf 10672 df-xr 10673 df-ltxr 10674 df-le 10675 df-sub 10866 df-neg 10867 df-div 11292 df-2 11694 df-rp 12384 df-xneg 12501 df-xadd 12502

This theorem is referenced by: (None)

W3C validator