Theorem xrofsup

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)

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

Proof

Step	Hyp	Ref	Expression
1		xrofsup.1	⊢ ( 𝜑 → 𝑋 ⊆ ℝ* )
2		xrofsup.2	⊢ ( 𝜑 → 𝑌 ⊆ ℝ* )
3		xrofsup.3	⊢ ( 𝜑 → sup ( 𝑋 , ℝ* , < ) ≠ -∞ )
4		xrofsup.4	⊢ ( 𝜑 → sup ( 𝑌 , ℝ* , < ) ≠ -∞ )
5		xrofsup.5	⊢ ( 𝜑 → 𝑍 = ( +𝑒 “ ( 𝑋 × 𝑌 ) ) )
6	1	sseld	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 → 𝑥 ∈ ℝ* ) )
7	2	sseld	⊢ ( 𝜑 → ( 𝑦 ∈ 𝑌 → 𝑦 ∈ ℝ* ) )
8	6 7	anim12d	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ) )
9	8	imp	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) )
10		xaddcl	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 +𝑒 𝑦 ) ∈ ℝ* )
11	9 10	syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝑥 +𝑒 𝑦 ) ∈ ℝ* )
12	11	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝑥 +𝑒 𝑦 ) ∈ ℝ* )
13		fveq2	⊢ ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( +𝑒 ‘ 𝑢 ) = ( +𝑒 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
14		df-ov	⊢ ( 𝑥 +𝑒 𝑦 ) = ( +𝑒 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
15	13 14	eqtr4di	⊢ ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( +𝑒 ‘ 𝑢 ) = ( 𝑥 +𝑒 𝑦 ) )
16	15	eleq1d	⊢ ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( +𝑒 ‘ 𝑢 ) ∈ ℝ* ↔ ( 𝑥 +𝑒 𝑦 ) ∈ ℝ* ) )
17	16	ralxp	⊢ ( ∀ 𝑢 ∈ ( 𝑋 × 𝑌 ) ( +𝑒 ‘ 𝑢 ) ∈ ℝ* ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝑥 +𝑒 𝑦 ) ∈ ℝ* )
18	12 17	sylibr	⊢ ( 𝜑 → ∀ 𝑢 ∈ ( 𝑋 × 𝑌 ) ( +𝑒 ‘ 𝑢 ) ∈ ℝ* )
19		xaddf	⊢ +𝑒 : ( ℝ* × ℝ* ) ⟶ ℝ*
20		ffun	⊢ ( +𝑒 : ( ℝ* × ℝ* ) ⟶ ℝ* → Fun +𝑒 )
21	19 20	ax-mp	⊢ Fun +𝑒
22		xpss12	⊢ ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) → ( 𝑋 × 𝑌 ) ⊆ ( ℝ* × ℝ* ) )
23	1 2 22	syl2anc	⊢ ( 𝜑 → ( 𝑋 × 𝑌 ) ⊆ ( ℝ* × ℝ* ) )
24	19	fdmi	⊢ dom +𝑒 = ( ℝ* × ℝ* )
25	23 24	sseqtrrdi	⊢ ( 𝜑 → ( 𝑋 × 𝑌 ) ⊆ dom +𝑒 )
26		funimass4	⊢ ( ( Fun +𝑒 ∧ ( 𝑋 × 𝑌 ) ⊆ dom +𝑒 ) → ( ( +𝑒 “ ( 𝑋 × 𝑌 ) ) ⊆ ℝ* ↔ ∀ 𝑢 ∈ ( 𝑋 × 𝑌 ) ( +𝑒 ‘ 𝑢 ) ∈ ℝ* ) )
27	21 25 26	sylancr	⊢ ( 𝜑 → ( ( +𝑒 “ ( 𝑋 × 𝑌 ) ) ⊆ ℝ* ↔ ∀ 𝑢 ∈ ( 𝑋 × 𝑌 ) ( +𝑒 ‘ 𝑢 ) ∈ ℝ* ) )
28	18 27	mpbird	⊢ ( 𝜑 → ( +𝑒 “ ( 𝑋 × 𝑌 ) ) ⊆ ℝ* )
29	5 28	eqsstrd	⊢ ( 𝜑 → 𝑍 ⊆ ℝ* )
30		supxrcl	⊢ ( 𝑋 ⊆ ℝ* → sup ( 𝑋 , ℝ* , < ) ∈ ℝ* )
31	1 30	syl	⊢ ( 𝜑 → sup ( 𝑋 , ℝ* , < ) ∈ ℝ* )
32		supxrcl	⊢ ( 𝑌 ⊆ ℝ* → sup ( 𝑌 , ℝ* , < ) ∈ ℝ* )
33	2 32	syl	⊢ ( 𝜑 → sup ( 𝑌 , ℝ* , < ) ∈ ℝ* )
34	31 33	xaddcld	⊢ ( 𝜑 → ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) ∈ ℝ* )
35	5	eleq2d	⊢ ( 𝜑 → ( 𝑧 ∈ 𝑍 ↔ 𝑧 ∈ ( +𝑒 “ ( 𝑋 × 𝑌 ) ) ) )
36	35	pm5.32i	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑍 ) ↔ ( 𝜑 ∧ 𝑧 ∈ ( +𝑒 “ ( 𝑋 × 𝑌 ) ) ) )
37		nfvd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( +𝑒 “ ( 𝑋 × 𝑌 ) ) ) → Ⅎ 𝑥 𝑧 ≤ ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) )
38		nfvd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( +𝑒 “ ( 𝑋 × 𝑌 ) ) ) → Ⅎ 𝑦 𝑧 ≤ ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) )
39	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( +𝑒 “ ( 𝑋 × 𝑌 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → 𝑋 ⊆ ℝ* )
40		simprl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( +𝑒 “ ( 𝑋 × 𝑌 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → 𝑥 ∈ 𝑋 )
41		supxrub	⊢ ( ( 𝑋 ⊆ ℝ* ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ≤ sup ( 𝑋 , ℝ* , < ) )
42	39 40 41	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( +𝑒 “ ( 𝑋 × 𝑌 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → 𝑥 ≤ sup ( 𝑋 , ℝ* , < ) )
43	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( +𝑒 “ ( 𝑋 × 𝑌 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → 𝑌 ⊆ ℝ* )
44		simprr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( +𝑒 “ ( 𝑋 × 𝑌 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → 𝑦 ∈ 𝑌 )
45		supxrub	⊢ ( ( 𝑌 ⊆ ℝ* ∧ 𝑦 ∈ 𝑌 ) → 𝑦 ≤ sup ( 𝑌 , ℝ* , < ) )
46	43 44 45	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( +𝑒 “ ( 𝑋 × 𝑌 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → 𝑦 ≤ sup ( 𝑌 , ℝ* , < ) )
47	39 40	sseldd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( +𝑒 “ ( 𝑋 × 𝑌 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → 𝑥 ∈ ℝ* )
48	43 44	sseldd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( +𝑒 “ ( 𝑋 × 𝑌 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → 𝑦 ∈ ℝ* )
49	39 30	syl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( +𝑒 “ ( 𝑋 × 𝑌 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → sup ( 𝑋 , ℝ* , < ) ∈ ℝ* )
50	43 32	syl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( +𝑒 “ ( 𝑋 × 𝑌 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → sup ( 𝑌 , ℝ* , < ) ∈ ℝ* )
51		xle2add	⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ( sup ( 𝑋 , ℝ* , < ) ∈ ℝ* ∧ sup ( 𝑌 , ℝ* , < ) ∈ ℝ* ) ) → ( ( 𝑥 ≤ sup ( 𝑋 , ℝ* , < ) ∧ 𝑦 ≤ sup ( 𝑌 , ℝ* , < ) ) → ( 𝑥 +𝑒 𝑦 ) ≤ ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) ) )
52	47 48 49 50 51	syl22anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( +𝑒 “ ( 𝑋 × 𝑌 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → ( ( 𝑥 ≤ sup ( 𝑋 , ℝ* , < ) ∧ 𝑦 ≤ sup ( 𝑌 , ℝ* , < ) ) → ( 𝑥 +𝑒 𝑦 ) ≤ ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) ) )
53	42 46 52	mp2and	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( +𝑒 “ ( 𝑋 × 𝑌 ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝑥 +𝑒 𝑦 ) ≤ ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) )
54	53	ralrimivva	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( +𝑒 “ ( 𝑋 × 𝑌 ) ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝑥 +𝑒 𝑦 ) ≤ ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) )
55		fvelima	⊢ ( ( Fun +𝑒 ∧ 𝑧 ∈ ( +𝑒 “ ( 𝑋 × 𝑌 ) ) ) → ∃ 𝑢 ∈ ( 𝑋 × 𝑌 ) ( +𝑒 ‘ 𝑢 ) = 𝑧 )
56	21 55	mpan	⊢ ( 𝑧 ∈ ( +𝑒 “ ( 𝑋 × 𝑌 ) ) → ∃ 𝑢 ∈ ( 𝑋 × 𝑌 ) ( +𝑒 ‘ 𝑢 ) = 𝑧 )
57	56	adantl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( +𝑒 “ ( 𝑋 × 𝑌 ) ) ) → ∃ 𝑢 ∈ ( 𝑋 × 𝑌 ) ( +𝑒 ‘ 𝑢 ) = 𝑧 )
58	15	eqeq1d	⊢ ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( +𝑒 ‘ 𝑢 ) = 𝑧 ↔ ( 𝑥 +𝑒 𝑦 ) = 𝑧 ) )
59	58	rexxp	⊢ ( ∃ 𝑢 ∈ ( 𝑋 × 𝑌 ) ( +𝑒 ‘ 𝑢 ) = 𝑧 ↔ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 ( 𝑥 +𝑒 𝑦 ) = 𝑧 )
60	57 59	sylib	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( +𝑒 “ ( 𝑋 × 𝑌 ) ) ) → ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 ( 𝑥 +𝑒 𝑦 ) = 𝑧 )
61	54 60	r19.29d2r	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( +𝑒 “ ( 𝑋 × 𝑌 ) ) ) → ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 ( ( 𝑥 +𝑒 𝑦 ) ≤ ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) ∧ ( 𝑥 +𝑒 𝑦 ) = 𝑧 ) )
62		ancom	⊢ ( ( ( 𝑥 +𝑒 𝑦 ) ≤ ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) ∧ ( 𝑥 +𝑒 𝑦 ) = 𝑧 ) ↔ ( ( 𝑥 +𝑒 𝑦 ) = 𝑧 ∧ ( 𝑥 +𝑒 𝑦 ) ≤ ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) ) )
63	62	2rexbii	⊢ ( ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 ( ( 𝑥 +𝑒 𝑦 ) ≤ ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) ∧ ( 𝑥 +𝑒 𝑦 ) = 𝑧 ) ↔ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 ( ( 𝑥 +𝑒 𝑦 ) = 𝑧 ∧ ( 𝑥 +𝑒 𝑦 ) ≤ ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) ) )
64	61 63	sylib	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( +𝑒 “ ( 𝑋 × 𝑌 ) ) ) → ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 ( ( 𝑥 +𝑒 𝑦 ) = 𝑧 ∧ ( 𝑥 +𝑒 𝑦 ) ≤ ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) ) )
65		breq1	⊢ ( ( 𝑥 +𝑒 𝑦 ) = 𝑧 → ( ( 𝑥 +𝑒 𝑦 ) ≤ ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) ↔ 𝑧 ≤ ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) ) )
66	65	biimpa	⊢ ( ( ( 𝑥 +𝑒 𝑦 ) = 𝑧 ∧ ( 𝑥 +𝑒 𝑦 ) ≤ ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) ) → 𝑧 ≤ ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) )
67	66	reximi	⊢ ( ∃ 𝑦 ∈ 𝑌 ( ( 𝑥 +𝑒 𝑦 ) = 𝑧 ∧ ( 𝑥 +𝑒 𝑦 ) ≤ ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) ) → ∃ 𝑦 ∈ 𝑌 𝑧 ≤ ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) )
68	67	reximi	⊢ ( ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 ( ( 𝑥 +𝑒 𝑦 ) = 𝑧 ∧ ( 𝑥 +𝑒 𝑦 ) ≤ ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) ) → ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 𝑧 ≤ ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) )
69	64 68	syl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( +𝑒 “ ( 𝑋 × 𝑌 ) ) ) → ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 𝑧 ≤ ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) )
70	37 38 69	19.9d2r	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( +𝑒 “ ( 𝑋 × 𝑌 ) ) ) → 𝑧 ≤ ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) )
71	36 70	sylbi	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑍 ) → 𝑧 ≤ ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) )
72	71	ralrimiva	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑍 𝑧 ≤ ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) )
73	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑧 < ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) ) → 𝑋 ⊆ ℝ* )
74	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑧 < ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) ) → 𝑌 ⊆ ℝ* )
75		simplr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑧 < ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) ) → 𝑧 ∈ ℝ )
76	31	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑧 < ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) ) → sup ( 𝑋 , ℝ* , < ) ∈ ℝ* )
77	33	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑧 < ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) ) → sup ( 𝑌 , ℝ* , < ) ∈ ℝ* )
78	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑧 < ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) ) → sup ( 𝑋 , ℝ* , < ) ≠ -∞ )
79	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑧 < ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) ) → sup ( 𝑌 , ℝ* , < ) ≠ -∞ )
80		simpr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑧 < ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) ) → 𝑧 < ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) )
81	75 76 77 78 79 80	xlt2addrd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑧 < ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) ) → ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) )
82		nfv	⊢ Ⅎ 𝑏 ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* )
83		nfcv	⊢ Ⅎ 𝑏 ℝ*
84		nfre1	⊢ Ⅎ 𝑏 ∃ 𝑏 ∈ ℝ* ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) )
85	83 84	nfrexw	⊢ Ⅎ 𝑏 ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) )
86	82 85	nfan	⊢ Ⅎ 𝑏 ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) )
87		nfvd	⊢ ( ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) → Ⅎ 𝑎 ∃ 𝑣 ∈ 𝑋 ∃ 𝑤 ∈ 𝑌 𝑧 < ( 𝑣 +𝑒 𝑤 ) )
88		nfvd	⊢ ( ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) → Ⅎ 𝑏 ∃ 𝑣 ∈ 𝑋 ∃ 𝑤 ∈ 𝑌 𝑧 < ( 𝑣 +𝑒 𝑤 ) )
89		id	⊢ ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) → ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) )
90	89	ralrimivw	⊢ ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) → ∀ 𝑏 ∈ ℝ* ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) )
91	90	ralrimivw	⊢ ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) → ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) )
92	91	adantr	⊢ ( ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) → ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) )
93		simpr	⊢ ( ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) → ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) )
94	92 93	r19.29d2r	⊢ ( ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) → ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) )
95		simplrr	⊢ ( ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) ) ∧ ( 𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌 ∧ ( 𝑎 < 𝑣 ∧ 𝑏 < 𝑤 ) ) ) → ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) )
96	95	3anassrs	⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) ) ∧ 𝑣 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑌 ) ∧ ( 𝑎 < 𝑣 ∧ 𝑏 < 𝑤 ) ) → ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) )
97	96	simp1d	⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) ) ∧ 𝑣 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑌 ) ∧ ( 𝑎 < 𝑣 ∧ 𝑏 < 𝑤 ) ) → 𝑧 = ( 𝑎 +𝑒 𝑏 ) )
98		simp-4l	⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) ) ∧ 𝑣 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑌 ) ∧ ( 𝑎 < 𝑣 ∧ 𝑏 < 𝑤 ) ) → ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) )
99		simplrl	⊢ ( ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) ) ∧ ( 𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌 ∧ ( 𝑎 < 𝑣 ∧ 𝑏 < 𝑤 ) ) ) → ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) )
100	99	3anassrs	⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) ) ∧ 𝑣 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑌 ) ∧ ( 𝑎 < 𝑣 ∧ 𝑏 < 𝑤 ) ) → ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) )
101	100	simpld	⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) ) ∧ 𝑣 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑌 ) ∧ ( 𝑎 < 𝑣 ∧ 𝑏 < 𝑤 ) ) → 𝑋 ⊆ ℝ* )
102		simpllr	⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) ) ∧ 𝑣 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑌 ) ∧ ( 𝑎 < 𝑣 ∧ 𝑏 < 𝑤 ) ) → 𝑣 ∈ 𝑋 )
103	101 102	sseldd	⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) ) ∧ 𝑣 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑌 ) ∧ ( 𝑎 < 𝑣 ∧ 𝑏 < 𝑤 ) ) → 𝑣 ∈ ℝ* )
104	100	simprd	⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) ) ∧ 𝑣 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑌 ) ∧ ( 𝑎 < 𝑣 ∧ 𝑏 < 𝑤 ) ) → 𝑌 ⊆ ℝ* )
105		simplr	⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) ) ∧ 𝑣 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑌 ) ∧ ( 𝑎 < 𝑣 ∧ 𝑏 < 𝑤 ) ) → 𝑤 ∈ 𝑌 )
106	104 105	sseldd	⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) ) ∧ 𝑣 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑌 ) ∧ ( 𝑎 < 𝑣 ∧ 𝑏 < 𝑤 ) ) → 𝑤 ∈ ℝ* )
107	98 103 106	jca32	⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) ) ∧ 𝑣 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑌 ) ∧ ( 𝑎 < 𝑣 ∧ 𝑏 < 𝑤 ) ) → ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ ( 𝑣 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) ) )
108		simpr	⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) ) ∧ 𝑣 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑌 ) ∧ ( 𝑎 < 𝑣 ∧ 𝑏 < 𝑤 ) ) → ( 𝑎 < 𝑣 ∧ 𝑏 < 𝑤 ) )
109		xlt2add	⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ ( 𝑣 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) ) → ( ( 𝑎 < 𝑣 ∧ 𝑏 < 𝑤 ) → ( 𝑎 +𝑒 𝑏 ) < ( 𝑣 +𝑒 𝑤 ) ) )
110	109	imp	⊢ ( ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ ( 𝑣 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) ) ∧ ( 𝑎 < 𝑣 ∧ 𝑏 < 𝑤 ) ) → ( 𝑎 +𝑒 𝑏 ) < ( 𝑣 +𝑒 𝑤 ) )
111		breq1	⊢ ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) → ( 𝑧 < ( 𝑣 +𝑒 𝑤 ) ↔ ( 𝑎 +𝑒 𝑏 ) < ( 𝑣 +𝑒 𝑤 ) ) )
112	111	biimpar	⊢ ( ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ ( 𝑎 +𝑒 𝑏 ) < ( 𝑣 +𝑒 𝑤 ) ) → 𝑧 < ( 𝑣 +𝑒 𝑤 ) )
113	110 112	sylan2	⊢ ( ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ ( 𝑣 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) ) ∧ ( 𝑎 < 𝑣 ∧ 𝑏 < 𝑤 ) ) ) → 𝑧 < ( 𝑣 +𝑒 𝑤 ) )
114	97 107 108 113	syl12anc	⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) ) ∧ 𝑣 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑌 ) ∧ ( 𝑎 < 𝑣 ∧ 𝑏 < 𝑤 ) ) → 𝑧 < ( 𝑣 +𝑒 𝑤 ) )
115		simplll	⊢ ( ( ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) → 𝑋 ⊆ ℝ* )
116		simprl	⊢ ( ( ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) → 𝑎 ∈ ℝ* )
117		simplr2	⊢ ( ( ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) → 𝑎 < sup ( 𝑋 , ℝ* , < ) )
118		supxrlub	⊢ ( ( 𝑋 ⊆ ℝ* ∧ 𝑎 ∈ ℝ* ) → ( 𝑎 < sup ( 𝑋 , ℝ* , < ) ↔ ∃ 𝑣 ∈ 𝑋 𝑎 < 𝑣 ) )
119	118	biimpa	⊢ ( ( ( 𝑋 ⊆ ℝ* ∧ 𝑎 ∈ ℝ* ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ) → ∃ 𝑣 ∈ 𝑋 𝑎 < 𝑣 )
120	115 116 117 119	syl21anc	⊢ ( ( ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) → ∃ 𝑣 ∈ 𝑋 𝑎 < 𝑣 )
121		simpllr	⊢ ( ( ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) → 𝑌 ⊆ ℝ* )
122		simprr	⊢ ( ( ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) → 𝑏 ∈ ℝ* )
123		simplr3	⊢ ( ( ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) → 𝑏 < sup ( 𝑌 , ℝ* , < ) )
124		supxrlub	⊢ ( ( 𝑌 ⊆ ℝ* ∧ 𝑏 ∈ ℝ* ) → ( 𝑏 < sup ( 𝑌 , ℝ* , < ) ↔ ∃ 𝑤 ∈ 𝑌 𝑏 < 𝑤 ) )
125	124	biimpa	⊢ ( ( ( 𝑌 ⊆ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) → ∃ 𝑤 ∈ 𝑌 𝑏 < 𝑤 )
126	121 122 123 125	syl21anc	⊢ ( ( ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) → ∃ 𝑤 ∈ 𝑌 𝑏 < 𝑤 )
127		reeanv	⊢ ( ∃ 𝑣 ∈ 𝑋 ∃ 𝑤 ∈ 𝑌 ( 𝑎 < 𝑣 ∧ 𝑏 < 𝑤 ) ↔ ( ∃ 𝑣 ∈ 𝑋 𝑎 < 𝑣 ∧ ∃ 𝑤 ∈ 𝑌 𝑏 < 𝑤 ) )
128	120 126 127	sylanbrc	⊢ ( ( ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ) → ∃ 𝑣 ∈ 𝑋 ∃ 𝑤 ∈ 𝑌 ( 𝑎 < 𝑣 ∧ 𝑏 < 𝑤 ) )
129	128	ancoms	⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) ) → ∃ 𝑣 ∈ 𝑋 ∃ 𝑤 ∈ 𝑌 ( 𝑎 < 𝑣 ∧ 𝑏 < 𝑤 ) )
130	114 129	reximddv2	⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) ) → ∃ 𝑣 ∈ 𝑋 ∃ 𝑤 ∈ 𝑌 𝑧 < ( 𝑣 +𝑒 𝑤 ) )
131	130	ex	⊢ ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) → ( ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) → ∃ 𝑣 ∈ 𝑋 ∃ 𝑤 ∈ 𝑌 𝑧 < ( 𝑣 +𝑒 𝑤 ) ) )
132	131	reximdva	⊢ ( 𝑎 ∈ ℝ* → ( ∃ 𝑏 ∈ ℝ* ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) → ∃ 𝑏 ∈ ℝ* ∃ 𝑣 ∈ 𝑋 ∃ 𝑤 ∈ 𝑌 𝑧 < ( 𝑣 +𝑒 𝑤 ) ) )
133	132	reximia	⊢ ( ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) → ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* ∃ 𝑣 ∈ 𝑋 ∃ 𝑤 ∈ 𝑌 𝑧 < ( 𝑣 +𝑒 𝑤 ) )
134	94 133	syl	⊢ ( ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) → ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* ∃ 𝑣 ∈ 𝑋 ∃ 𝑤 ∈ 𝑌 𝑧 < ( 𝑣 +𝑒 𝑤 ) )
135	86 87 88 134	19.9d2rf	⊢ ( ( ( 𝑋 ⊆ ℝ* ∧ 𝑌 ⊆ ℝ* ) ∧ ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* ( 𝑧 = ( 𝑎 +𝑒 𝑏 ) ∧ 𝑎 < sup ( 𝑋 , ℝ* , < ) ∧ 𝑏 < sup ( 𝑌 , ℝ* , < ) ) ) → ∃ 𝑣 ∈ 𝑋 ∃ 𝑤 ∈ 𝑌 𝑧 < ( 𝑣 +𝑒 𝑤 ) )
136	73 74 81 135	syl21anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑧 < ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) ) → ∃ 𝑣 ∈ 𝑋 ∃ 𝑤 ∈ 𝑌 𝑧 < ( 𝑣 +𝑒 𝑤 ) )
137		simprl	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌 ) ) → 𝑣 ∈ 𝑋 )
138		simprr	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌 ) ) → 𝑤 ∈ 𝑌 )
139	21	a1i	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌 ) ) → Fun +𝑒 )
140	25	adantr	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌 ) ) → ( 𝑋 × 𝑌 ) ⊆ dom +𝑒 )
141	137 138 139 140	elovimad	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌 ) ) → ( 𝑣 +𝑒 𝑤 ) ∈ ( +𝑒 “ ( 𝑋 × 𝑌 ) ) )
142	5	eleq2d	⊢ ( 𝜑 → ( ( 𝑣 +𝑒 𝑤 ) ∈ 𝑍 ↔ ( 𝑣 +𝑒 𝑤 ) ∈ ( +𝑒 “ ( 𝑋 × 𝑌 ) ) ) )
143	142	adantr	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌 ) ) → ( ( 𝑣 +𝑒 𝑤 ) ∈ 𝑍 ↔ ( 𝑣 +𝑒 𝑤 ) ∈ ( +𝑒 “ ( 𝑋 × 𝑌 ) ) ) )
144	141 143	mpbird	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌 ) ) → ( 𝑣 +𝑒 𝑤 ) ∈ 𝑍 )
145		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌 ) ) ∧ 𝑘 = ( 𝑣 +𝑒 𝑤 ) ) → 𝑘 = ( 𝑣 +𝑒 𝑤 ) )
146	145	breq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌 ) ) ∧ 𝑘 = ( 𝑣 +𝑒 𝑤 ) ) → ( 𝑧 < 𝑘 ↔ 𝑧 < ( 𝑣 +𝑒 𝑤 ) ) )
147	144 146	rspcedv	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌 ) ) → ( 𝑧 < ( 𝑣 +𝑒 𝑤 ) → ∃ 𝑘 ∈ 𝑍 𝑧 < 𝑘 ) )
148	147	rexlimdvva	⊢ ( 𝜑 → ( ∃ 𝑣 ∈ 𝑋 ∃ 𝑤 ∈ 𝑌 𝑧 < ( 𝑣 +𝑒 𝑤 ) → ∃ 𝑘 ∈ 𝑍 𝑧 < 𝑘 ) )
149	148	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑧 < ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) ) → ( ∃ 𝑣 ∈ 𝑋 ∃ 𝑤 ∈ 𝑌 𝑧 < ( 𝑣 +𝑒 𝑤 ) → ∃ 𝑘 ∈ 𝑍 𝑧 < 𝑘 ) )
150	136 149	mpd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) ∧ 𝑧 < ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) ) → ∃ 𝑘 ∈ 𝑍 𝑧 < 𝑘 )
151	150	ex	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) → ( 𝑧 < ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) → ∃ 𝑘 ∈ 𝑍 𝑧 < 𝑘 ) )
152	151	ralrimiva	⊢ ( 𝜑 → ∀ 𝑧 ∈ ℝ ( 𝑧 < ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) → ∃ 𝑘 ∈ 𝑍 𝑧 < 𝑘 ) )
153		supxr2	⊢ ( ( ( 𝑍 ⊆ ℝ* ∧ ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) ∈ ℝ* ) ∧ ( ∀ 𝑧 ∈ 𝑍 𝑧 ≤ ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) ∧ ∀ 𝑧 ∈ ℝ ( 𝑧 < ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) → ∃ 𝑘 ∈ 𝑍 𝑧 < 𝑘 ) ) ) → sup ( 𝑍 , ℝ* , < ) = ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) )
154	29 34 72 152 153	syl22anc	⊢ ( 𝜑 → sup ( 𝑍 , ℝ* , < ) = ( sup ( 𝑋 , ℝ* , < ) +𝑒 sup ( 𝑌 , ℝ* , < ) ) )