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 33052

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 3944	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝑋 → 𝑥 ∈ ℝ^*))
4		xrofsup.2	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ⊆ ℝ^*)
5	4	sseld 3944	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ 𝑌 → 𝑦 ∈ ℝ^*))
6	3, 5	anim12d 620	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → (𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*)))
7	6	imp 411	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*))
8		xaddcl 13264	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → (𝑥 +_𝑒 𝑦) ∈ ℝ^)
9	7, 8	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑥 +_𝑒 𝑦) ∈ ℝ^*)
10	9	ralrimivva 3214	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝑥 +_𝑒 𝑦) ∈ ℝ^*)
11		fveq2 6882	. . . . . . . 8 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → ( +_𝑒 ‘𝑢) = ( +_𝑒 ‘⟨𝑥, 𝑦⟩))
12		df-ov 7414	. . . . . . . 8 ⊢ (𝑥 +_𝑒 𝑦) = ( +_𝑒 ‘⟨𝑥, 𝑦⟩)
13	11, 12	eqtr4di 2822	. . . . . . 7 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → ( +_𝑒 ‘𝑢) = (𝑥 +_𝑒 𝑦))
14	13	eleq1d 2854	. . . . . 6 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → (( +_𝑒 ‘𝑢) ∈ ℝ^* ↔ (𝑥 +_𝑒 𝑦) ∈ ℝ^*))
15	14	ralxp 5828	. . . . 5 ⊢ (∀𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) ∈ ℝ^* ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝑥 +_𝑒 𝑦) ∈ ℝ^*)
16	10, 15	sylibr 237	. . . 4 ⊢ (𝜑 → ∀𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) ∈ ℝ^*)
17		xaddf 13249	. . . . . 6 ⊢ +_𝑒 :(ℝ^* × ℝ^)⟶ℝ^
18		ffun 6709	. . . . . 6 ⊢ ( +_𝑒 :(ℝ^* × ℝ^)⟶ℝ^ → Fun +_𝑒 )
19	17, 18	ax-mp 5	. . . . 5 ⊢ Fun +_𝑒
20		xpss12 5677	. . . . . . 7 ⊢ ((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) → (𝑋 × 𝑌) ⊆ (ℝ^ × ℝ^*))
21	2, 4, 20	syl2anc 595	. . . . . 6 ⊢ (𝜑 → (𝑋 × 𝑌) ⊆ (ℝ^* × ℝ^*))
22	17	fdmi 6718	. . . . . 6 ⊢ dom +_𝑒 = (ℝ^* × ℝ^*)
23	21, 22	sseqtrrdi 3986	. . . . 5 ⊢ (𝜑 → (𝑋 × 𝑌) ⊆ dom +_𝑒 )
24		funimass4 6946	. . . . 5 ⊢ ((Fun +_𝑒 ∧ (𝑋 × 𝑌) ⊆ dom +_𝑒 ) → (( +_𝑒 “ (𝑋 × 𝑌)) ⊆ ℝ^* ↔ ∀𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) ∈ ℝ^*))
25	19, 23, 24	sylancr 598	. . . 4 ⊢ (𝜑 → (( +_𝑒 “ (𝑋 × 𝑌)) ⊆ ℝ^* ↔ ∀𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) ∈ ℝ^*))
26	16, 25	mpbird 260	. . 3 ⊢ (𝜑 → ( +_𝑒 “ (𝑋 × 𝑌)) ⊆ ℝ^*)
27	1, 26	eqsstrd 3979	. 2 ⊢ (𝜑 → 𝑍 ⊆ ℝ^*)
28		supxrcl 13340	. . . 4 ⊢ (𝑋 ⊆ ℝ^* → sup(𝑋, ℝ^, < ) ∈ ℝ^)
29	2, 28	syl 18	. . 3 ⊢ (𝜑 → sup(𝑋, ℝ^, < ) ∈ ℝ^)
30		supxrcl 13340	. . . 4 ⊢ (𝑌 ⊆ ℝ^* → sup(𝑌, ℝ^, < ) ∈ ℝ^)
31	4, 30	syl 18	. . 3 ⊢ (𝜑 → sup(𝑌, ℝ^, < ) ∈ ℝ^)
32	29, 31	xaddcld 13326	. 2 ⊢ (𝜑 → (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) ∈ ℝ^*)
33	1	eleq2d 2855	. . . . 5 ⊢ (𝜑 → (𝑧 ∈ 𝑍 ↔ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))))
34	33	pm5.32i 584	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑍) ↔ (𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))))
35		nfvd 1942	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → Ⅎ𝑥 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
36		nfvd 1942	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → Ⅎ𝑦 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
37	2	ad2antrr 738	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑋 ⊆ ℝ^*)
38		simprl 782	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑥 ∈ 𝑋)
39		supxrub 13349	. . . . . . . . . . 11 ⊢ ((𝑋 ⊆ ℝ^* ∧ 𝑥 ∈ 𝑋) → 𝑥 ≤ sup(𝑋, ℝ^*, < ))
40	37, 38, 39	syl2anc 595	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑥 ≤ sup(𝑋, ℝ^*, < ))
41	4	ad2antrr 738	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑌 ⊆ ℝ^*)
42		simprr 784	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑦 ∈ 𝑌)
43		supxrub 13349	. . . . . . . . . . 11 ⊢ ((𝑌 ⊆ ℝ^* ∧ 𝑦 ∈ 𝑌) → 𝑦 ≤ sup(𝑌, ℝ^*, < ))
44	41, 42, 43	syl2anc 595	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑦 ≤ sup(𝑌, ℝ^*, < ))
45	37, 38	sseldd 3946	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑥 ∈ ℝ^*)
46	41, 42	sseldd 3946	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑦 ∈ ℝ^*)
47	37, 28	syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → sup(𝑋, ℝ^, < ) ∈ ℝ^)
48	41, 30	syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → sup(𝑌, ℝ^, < ) ∈ ℝ^)
49		xle2add 13284	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) ∧ (sup(𝑋, ℝ^, < ) ∈ ℝ^* ∧ sup(𝑌, ℝ^, < ) ∈ ℝ^)) → ((𝑥 ≤ sup(𝑋, ℝ^, < ) ∧ 𝑦 ≤ sup(𝑌, ℝ^, < )) → (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))))
50	45, 46, 47, 48, 49	syl22anc 851	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑥 ≤ sup(𝑋, ℝ^, < ) ∧ 𝑦 ≤ sup(𝑌, ℝ^, < )) → (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))))
51	40, 44, 50	mp2and 711	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
52	51	ralrimivva 3214	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
53		fvelima 6947	. . . . . . . . . . 11 ⊢ ((Fun +_𝑒 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → ∃𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) = 𝑧)
54	19, 53	mpan 702	. . . . . . . . . 10 ⊢ (𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌)) → ∃𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) = 𝑧)
55	54	adantl 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → ∃𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) = 𝑧)
56	13	eqeq1d 2771	. . . . . . . . . 10 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → (( +_𝑒 ‘𝑢) = 𝑧 ↔ (𝑥 +_𝑒 𝑦) = 𝑧))
57	56	rexxp 5829	. . . . . . . . 9 ⊢ (∃𝑢 ∈ (𝑋 × 𝑌)( +_𝑒 ‘𝑢) = 𝑧 ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 (𝑥 +_𝑒 𝑦) = 𝑧)
58	55, 57	sylib 221	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 (𝑥 +_𝑒 𝑦) = 𝑧)
59	52, 58	r19.29d2r 3158	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ((𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) ∧ (𝑥 +_𝑒 𝑦) = 𝑧))
60		ancom 465	. . . . . . . 8 ⊢ (((𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) ∧ (𝑥 +_𝑒 𝑦) = 𝑧) ↔ ((𝑥 +_𝑒 𝑦) = 𝑧 ∧ (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))))
61	60	2rexbii 3147	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ((𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) ∧ (𝑥 +_𝑒 𝑦) = 𝑧) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ((𝑥 +_𝑒 𝑦) = 𝑧 ∧ (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))))
62	59, 61	sylib 221	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ((𝑥 +_𝑒 𝑦) = 𝑧 ∧ (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))))
63		breq1 5116	. . . . . . . . 9 ⊢ ((𝑥 +_𝑒 𝑦) = 𝑧 → ((𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) ↔ 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))))
64	63	biimpa 481	. . . . . . . 8 ⊢ (((𝑥 +_𝑒 𝑦) = 𝑧 ∧ (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
65	64	reximi 3109	. . . . . . 7 ⊢ (∃𝑦 ∈ 𝑌 ((𝑥 +_𝑒 𝑦) = 𝑧 ∧ (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → ∃𝑦 ∈ 𝑌 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
66	65	reximi 3109	. . . . . 6 ⊢ (∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ((𝑥 +_𝑒 𝑦) = 𝑧 ∧ (𝑥 +_𝑒 𝑦) ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
67	62, 66	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
68	35, 36, 67	19.9d2r 32757	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ( +_𝑒 “ (𝑋 × 𝑌))) → 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
69	34, 68	sylbi 220	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑍) → 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
70	69	ralrimiva 3163	. 2 ⊢ (𝜑 → ∀𝑧 ∈ 𝑍 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
71	2	ad2antrr 738	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → 𝑋 ⊆ ℝ^*)
72	4	ad2antrr 738	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → 𝑌 ⊆ ℝ^*)
73		simplr 780	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → 𝑧 ∈ ℝ)
74	29	ad2antrr 738	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → sup(𝑋, ℝ^, < ) ∈ ℝ^)
75	31	ad2antrr 738	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → sup(𝑌, ℝ^, < ) ∈ ℝ^)
76		xrofsup.3	. . . . . . . 8 ⊢ (𝜑 → sup(𝑋, ℝ^*, < ) ≠ -∞)
77	76	ad2antrr 738	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → sup(𝑋, ℝ^*, < ) ≠ -∞)
78		xrofsup.4	. . . . . . . 8 ⊢ (𝜑 → sup(𝑌, ℝ^*, < ) ≠ -∞)
79	78	ad2antrr 738	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → sup(𝑌, ℝ^*, < ) ≠ -∞)
80		simpr 489	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
81	73, 74, 75, 77, 79, 80	xlt2addrd 33044	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → ∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))
82		nfv 1941	. . . . . . . 8 ⊢ Ⅎ𝑏(𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^*)
83		nfcv 2931	. . . . . . . . 9 ⊢ Ⅎ𝑏ℝ^*
84		nfre1 3296	. . . . . . . . 9 ⊢ Ⅎ𝑏∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))
85	83, 84	nfrexw 3319	. . . . . . . 8 ⊢ Ⅎ𝑏∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))
86	82, 85	nfan 1926	. . . . . . 7 ⊢ Ⅎ𝑏((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))
87		nfvd 1942	. . . . . . 7 ⊢ (((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → Ⅎ𝑎∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤))
88		nfvd 1942	. . . . . . 7 ⊢ (((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → Ⅎ𝑏∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤))
89		id 23	. . . . . . . . . . . 12 ⊢ ((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) → (𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^*))
90	89	ralrimivw 3167	. . . . . . . . . . 11 ⊢ ((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) → ∀𝑏 ∈ ℝ^ (𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^*))
91	90	ralrimivw 3167	. . . . . . . . . 10 ⊢ ((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) → ∀𝑎 ∈ ℝ^ ∀𝑏 ∈ ℝ^* (𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^*))
92	91	adantr 485	. . . . . . . . 9 ⊢ (((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → ∀𝑎 ∈ ℝ^* ∀𝑏 ∈ ℝ^* (𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^*))
93		simpr 489	. . . . . . . . 9 ⊢ (((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → ∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))
94	92, 93	r19.29d2r 3158	. . . . . . . 8 ⊢ (((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → ∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* ((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < ))))
95		simplrr 789	. . . . . . . . . . . . . . 15 ⊢ ((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌 ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤))) → (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))
96	95	3anassrs 1379	. . . . . . . . . . . . . 14 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))
97	96	simp1d 1158	. . . . . . . . . . . . 13 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑧 = (𝑎 +_𝑒 𝑏))
98		simp-4l 794	. . . . . . . . . . . . . 14 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^*))
99		simplrl 788	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌 ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤))) → (𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^*))
100	99	3anassrs 1379	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → (𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^*))
101	100	simpld 499	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑋 ⊆ ℝ^)
102		simpllr 787	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑣 ∈ 𝑋)
103	101, 102	sseldd 3946	. . . . . . . . . . . . . 14 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑣 ∈ ℝ^)
104	100	simprd 500	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑌 ⊆ ℝ^)
105		simplr 780	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑤 ∈ 𝑌)
106	104, 105	sseldd 3946	. . . . . . . . . . . . . 14 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑤 ∈ ℝ^)
107	98, 103, 106	jca32 524	. . . . . . . . . . . . 13 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → ((𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^) ∧ (𝑣 ∈ ℝ^ ∧ 𝑤 ∈ ℝ^*)))
108		simpr 489	. . . . . . . . . . . . 13 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → (𝑎 < 𝑣 ∧ 𝑏 < 𝑤))
109		xlt2add 13285	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ (𝑣 ∈ ℝ^ ∧ 𝑤 ∈ ℝ^*)) → ((𝑎 < 𝑣 ∧ 𝑏 < 𝑤) → (𝑎 +_𝑒 𝑏) < (𝑣 +_𝑒 𝑤)))
110	109	imp 411	. . . . . . . . . . . . . 14 ⊢ ((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ (𝑣 ∈ ℝ^ ∧ 𝑤 ∈ ℝ^*)) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → (𝑎 +_𝑒 𝑏) < (𝑣 +_𝑒 𝑤))
111		breq1 5116	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑎 +_𝑒 𝑏) → (𝑧 < (𝑣 +_𝑒 𝑤) ↔ (𝑎 +_𝑒 𝑏) < (𝑣 +_𝑒 𝑤)))
112	111	biimpar 482	. . . . . . . . . . . . . 14 ⊢ ((𝑧 = (𝑎 +_𝑒 𝑏) ∧ (𝑎 +_𝑒 𝑏) < (𝑣 +_𝑒 𝑤)) → 𝑧 < (𝑣 +_𝑒 𝑤))
113	110, 112	sylan2 604	. . . . . . . . . . . . 13 ⊢ ((𝑧 = (𝑎 +_𝑒 𝑏) ∧ (((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ (𝑣 ∈ ℝ^ ∧ 𝑤 ∈ ℝ^*)) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤))) → 𝑧 < (𝑣 +_𝑒 𝑤))
114	97, 107, 108, 113	syl12anc 849	. . . . . . . . . . . 12 ⊢ ((((((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑤 ∈ 𝑌) ∧ (𝑎 < 𝑣 ∧ 𝑏 < 𝑤)) → 𝑧 < (𝑣 +_𝑒 𝑤))
115		simplll 786	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^)) → 𝑋 ⊆ ℝ^)
116		simprl 782	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^)) → 𝑎 ∈ ℝ^)
117		simplr2 1233	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^)) → 𝑎 < sup(𝑋, ℝ^, < ))
118		supxrlub 13350	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ⊆ ℝ^* ∧ 𝑎 ∈ ℝ^) → (𝑎 < sup(𝑋, ℝ^, < ) ↔ ∃𝑣 ∈ 𝑋 𝑎 < 𝑣))
119	118	biimpa 481	. . . . . . . . . . . . . . 15 ⊢ (((𝑋 ⊆ ℝ^* ∧ 𝑎 ∈ ℝ^) ∧ 𝑎 < sup(𝑋, ℝ^, < )) → ∃𝑣 ∈ 𝑋 𝑎 < 𝑣)
120	115, 116, 117, 119	syl21anc 850	. . . . . . . . . . . . . 14 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^*)) → ∃𝑣 ∈ 𝑋 𝑎 < 𝑣)
121		simpllr 787	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^)) → 𝑌 ⊆ ℝ^)
122		simprr 784	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^)) → 𝑏 ∈ ℝ^)
123		simplr3 1234	. . . . . . . . . . . . . . 15 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^)) → 𝑏 < sup(𝑌, ℝ^, < ))
124		supxrlub 13350	. . . . . . . . . . . . . . . 16 ⊢ ((𝑌 ⊆ ℝ^* ∧ 𝑏 ∈ ℝ^) → (𝑏 < sup(𝑌, ℝ^, < ) ↔ ∃𝑤 ∈ 𝑌 𝑏 < 𝑤))
125	124	biimpa 481	. . . . . . . . . . . . . . 15 ⊢ (((𝑌 ⊆ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ 𝑏 < sup(𝑌, ℝ^, < )) → ∃𝑤 ∈ 𝑌 𝑏 < 𝑤)
126	121, 122, 123, 125	syl21anc 850	. . . . . . . . . . . . . 14 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^*)) → ∃𝑤 ∈ 𝑌 𝑏 < 𝑤)
127		reeanv 3243	. . . . . . . . . . . . . 14 ⊢ (∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 (𝑎 < 𝑣 ∧ 𝑏 < 𝑤) ↔ (∃𝑣 ∈ 𝑋 𝑎 < 𝑣 ∧ ∃𝑤 ∈ 𝑌 𝑏 < 𝑤))
128	120, 126, 127	sylanbrc 594	. . . . . . . . . . . . 13 ⊢ ((((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) ∧ (𝑎 ∈ ℝ^ ∧ 𝑏 ∈ ℝ^*)) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 (𝑎 < 𝑣 ∧ 𝑏 < 𝑤))
129	128	ancoms 463	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 (𝑎 < 𝑣 ∧ 𝑏 < 𝑤))
130	114, 129	reximddv2 3230	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < )))) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤))
131	130	ex 417	. . . . . . . . . 10 ⊢ ((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) → (((𝑋 ⊆ ℝ^ ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^*, < ))) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤)))
132	131	reximdva 3184	. . . . . . . . 9 ⊢ (𝑎 ∈ ℝ^* → (∃𝑏 ∈ ℝ^* ((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → ∃𝑏 ∈ ℝ^ ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤)))
133	132	reximia 3106	. . . . . . . 8 ⊢ (∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* ((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤))
134	94, 133	syl 18	. . . . . . 7 ⊢ (((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → ∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤))
135	86, 87, 88, 134	19.9d2rf 32756	. . . . . 6 ⊢ (((𝑋 ⊆ ℝ^* ∧ 𝑌 ⊆ ℝ^) ∧ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* (𝑧 = (𝑎 +_𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ^, < ) ∧ 𝑏 < sup(𝑌, ℝ^, < ))) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤))
136	71, 72, 81, 135	syl21anc 850	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤))
137		simprl 782	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → 𝑣 ∈ 𝑋)
138		simprr 784	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → 𝑤 ∈ 𝑌)
139	19	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → Fun +_𝑒 )
140	23	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → (𝑋 × 𝑌) ⊆ dom +_𝑒 )
141	137, 138, 139, 140	elovimad 7461	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → (𝑣 +_𝑒 𝑤) ∈ ( +_𝑒 “ (𝑋 × 𝑌)))
142	1	eleq2d 2855	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑣 +_𝑒 𝑤) ∈ 𝑍 ↔ (𝑣 +_𝑒 𝑤) ∈ ( +_𝑒 “ (𝑋 × 𝑌))))
143	142	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → ((𝑣 +_𝑒 𝑤) ∈ 𝑍 ↔ (𝑣 +_𝑒 𝑤) ∈ ( +_𝑒 “ (𝑋 × 𝑌))))
144	141, 143	mpbird 260	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → (𝑣 +_𝑒 𝑤) ∈ 𝑍)
145		simpr 489	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) ∧ 𝑘 = (𝑣 +_𝑒 𝑤)) → 𝑘 = (𝑣 +_𝑒 𝑤))
146	145	breq2d 5125	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) ∧ 𝑘 = (𝑣 +_𝑒 𝑤)) → (𝑧 < 𝑘 ↔ 𝑧 < (𝑣 +_𝑒 𝑤)))
147	144, 146	rspcedv 3583	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌)) → (𝑧 < (𝑣 +_𝑒 𝑤) → ∃𝑘 ∈ 𝑍 𝑧 < 𝑘))
148	147	rexlimdvva 3228	. . . . . 6 ⊢ (𝜑 → (∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤) → ∃𝑘 ∈ 𝑍 𝑧 < 𝑘))
149	148	ad2antrr 738	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → (∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑌 𝑧 < (𝑣 +_𝑒 𝑤) → ∃𝑘 ∈ 𝑍 𝑧 < 𝑘))
150	136, 149	mpd 16	. . . 4 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < ))) → ∃𝑘 ∈ 𝑍 𝑧 < 𝑘)
151	150	ex 417	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → (𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) → ∃𝑘 ∈ 𝑍 𝑧 < 𝑘))
152	151	ralrimiva 3163	. 2 ⊢ (𝜑 → ∀𝑧 ∈ ℝ (𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) → ∃𝑘 ∈ 𝑍 𝑧 < 𝑘))
153		supxr2 13339	. 2 ⊢ (((𝑍 ⊆ ℝ^* ∧ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) ∈ ℝ^) ∧ (∀𝑧 ∈ 𝑍 𝑧 ≤ (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) ∧ ∀𝑧 ∈ ℝ (𝑧 < (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )) → ∃𝑘 ∈ 𝑍 𝑧 < 𝑘))) → sup(𝑍, ℝ^, < ) = (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^, < )))
154	27, 32, 70, 152, 153	syl22anc 851	1 ⊢ (𝜑 → sup(𝑍, ℝ^, < ) = (sup(𝑋, ℝ^, < ) +_𝑒 sup(𝑌, ℝ^*, < )))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1101 = wceq 1567 ∈ wcel 2149 ≠ wne 2964 ∀wral 3085 ∃wrex 3095 ⊆ wss 3913 ⟨cop 4600 class class class wbr 5113 × cxp 5660 dom cdm 5662 “ cima 5665 Fun wfun 6531 ⟶wf 6533 ‘cfv 6537 (class class class)co 7411 supcsup 9399 ℝcr 11098 -∞cmnf 11240 ℝ^*cxr 11241 < clt 11242 ≤ cle 11243 +_𝑒 cxad 13134

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-cnex 11155 ax-resscn 11156 ax-1cn 11157 ax-icn 11158 ax-addcl 11159 ax-addrcl 11160 ax-mulcl 11161 ax-mulrcl 11162 ax-mulcom 11163 ax-addass 11164 ax-mulass 11165 ax-distr 11166 ax-i2m1 11167 ax-1ne0 11168 ax-1rid 11169 ax-rnegex 11170 ax-rrecex 11171 ax-cnre 11172 ax-pre-lttri 11173 ax-pre-lttrn 11174 ax-pre-ltadd 11175 ax-pre-mulgt0 11176 ax-pre-sup 11177

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-iun 4962 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7862 df-1st 7985 df-2nd 7986 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-er 8693 df-en 8943 df-dom 8944 df-sdom 8945 df-sup 9401 df-pnf 11244 df-mnf 11245 df-xr 11246 df-ltxr 11247 df-le 11248 df-sub 11442 df-neg 11443 df-div 11871 df-nn 12233 df-2 12302 df-rp 13016 df-xneg 13136 df-xadd 13137

This theorem is referenced by: (None)

W3C validator