This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( 𝑌 , ℝ* , < ) ) )