Theorem supadd

Description: The supremum function distributes over addition in a sense similar to that in supmul . (Contributed by Brendan Leahy, 26-Sep-2017)

	Ref	Expression
Hypotheses	supadd.a1	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	supadd.a2	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
	supadd.a3	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
	supadd.b1	⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
	supadd.b2	⊢ ( 𝜑 → 𝐵 ≠ ∅ )
	supadd.b3	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑦 ≤ 𝑥 )
	supadd.c	⊢ 𝐶 = { 𝑧 ∣ ∃ 𝑣 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑣 + 𝑏 ) }
Assertion	supadd	⊢ ( 𝜑 → ( sup ( 𝐴 , ℝ , < ) + sup ( 𝐵 , ℝ , < ) ) = sup ( 𝐶 , ℝ , < ) )

Proof

Step	Hyp	Ref	Expression
1		supadd.a1	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2		supadd.a2	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
3		supadd.a3	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
4		supadd.b1	⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
5		supadd.b2	⊢ ( 𝜑 → 𝐵 ≠ ∅ )
6		supadd.b3	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑦 ≤ 𝑥 )
7		supadd.c	⊢ 𝐶 = { 𝑧 ∣ ∃ 𝑣 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑣 + 𝑏 ) }
8	4 5 6	suprcld	⊢ ( 𝜑 → sup ( 𝐵 , ℝ , < ) ∈ ℝ )
9		eqid	⊢ { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = ( 𝑎 + sup ( 𝐵 , ℝ , < ) ) } = { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = ( 𝑎 + sup ( 𝐵 , ℝ , < ) ) }
10	1 2 3 8 9	supaddc	⊢ ( 𝜑 → ( sup ( 𝐴 , ℝ , < ) + sup ( 𝐵 , ℝ , < ) ) = sup ( { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = ( 𝑎 + sup ( 𝐵 , ℝ , < ) ) } , ℝ , < ) )
11	1	sselda	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ ℝ )
12	11	recnd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ ℂ )
13	8	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → sup ( 𝐵 , ℝ , < ) ∈ ℝ )
14	13	recnd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → sup ( 𝐵 , ℝ , < ) ∈ ℂ )
15	12 14	addcomd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑎 + sup ( 𝐵 , ℝ , < ) ) = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) )
16	15	eqeq2d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑧 = ( 𝑎 + sup ( 𝐵 , ℝ , < ) ) ↔ 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) ) )
17	16	rexbidva	⊢ ( 𝜑 → ( ∃ 𝑎 ∈ 𝐴 𝑧 = ( 𝑎 + sup ( 𝐵 , ℝ , < ) ) ↔ ∃ 𝑎 ∈ 𝐴 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) ) )
18	17	abbidv	⊢ ( 𝜑 → { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = ( 𝑎 + sup ( 𝐵 , ℝ , < ) ) } = { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) } )
19	18	supeq1d	⊢ ( 𝜑 → sup ( { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = ( 𝑎 + sup ( 𝐵 , ℝ , < ) ) } , ℝ , < ) = sup ( { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) } , ℝ , < ) )
20	10 19	eqtrd	⊢ ( 𝜑 → ( sup ( 𝐴 , ℝ , < ) + sup ( 𝐵 , ℝ , < ) ) = sup ( { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) } , ℝ , < ) )
21		vex	⊢ 𝑤 ∈ V
22		eqeq1	⊢ ( 𝑧 = 𝑤 → ( 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) ↔ 𝑤 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) ) )
23	22	rexbidv	⊢ ( 𝑧 = 𝑤 → ( ∃ 𝑎 ∈ 𝐴 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) ↔ ∃ 𝑎 ∈ 𝐴 𝑤 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) ) )
24	21 23	elab	⊢ ( 𝑤 ∈ { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) } ↔ ∃ 𝑎 ∈ 𝐴 𝑤 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) )
25	4	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝐵 ⊆ ℝ )
26	5	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝐵 ≠ ∅ )
27	6	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑦 ≤ 𝑥 )
28		eqid	⊢ { 𝑧 ∣ ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑏 + 𝑎 ) } = { 𝑧 ∣ ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑏 + 𝑎 ) }
29	25 26 27 11 28	supaddc	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) = sup ( { 𝑧 ∣ ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑏 + 𝑎 ) } , ℝ , < ) )
30	4	sselda	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ ℝ )
31	30	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ ℝ )
32	31	recnd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ ℂ )
33	11	adantr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ) → 𝑎 ∈ ℝ )
34	33	recnd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ) → 𝑎 ∈ ℂ )
35	32 34	addcomd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 + 𝑎 ) = ( 𝑎 + 𝑏 ) )
36	35	eqeq2d	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑧 = ( 𝑏 + 𝑎 ) ↔ 𝑧 = ( 𝑎 + 𝑏 ) ) )
37	36	rexbidva	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑏 + 𝑎 ) ↔ ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 + 𝑏 ) ) )
38	37	abbidv	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → { 𝑧 ∣ ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑏 + 𝑎 ) } = { 𝑧 ∣ ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 + 𝑏 ) } )
39	38	supeq1d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → sup ( { 𝑧 ∣ ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑏 + 𝑎 ) } , ℝ , < ) = sup ( { 𝑧 ∣ ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 + 𝑏 ) } , ℝ , < ) )
40	29 39	eqtrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) = sup ( { 𝑧 ∣ ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 + 𝑏 ) } , ℝ , < ) )
41		eqeq1	⊢ ( 𝑧 = 𝑤 → ( 𝑧 = ( 𝑎 + 𝑏 ) ↔ 𝑤 = ( 𝑎 + 𝑏 ) ) )
42	41	rexbidv	⊢ ( 𝑧 = 𝑤 → ( ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 + 𝑏 ) ↔ ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 + 𝑏 ) ) )
43	21 42	elab	⊢ ( 𝑤 ∈ { 𝑧 ∣ ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 + 𝑏 ) } ↔ ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 + 𝑏 ) )
44		rspe	⊢ ( ( 𝑎 ∈ 𝐴 ∧ ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 + 𝑏 ) ) → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 + 𝑏 ) )
45		oveq1	⊢ ( 𝑣 = 𝑎 → ( 𝑣 + 𝑏 ) = ( 𝑎 + 𝑏 ) )
46	45	eqeq2d	⊢ ( 𝑣 = 𝑎 → ( 𝑧 = ( 𝑣 + 𝑏 ) ↔ 𝑧 = ( 𝑎 + 𝑏 ) ) )
47	46	rexbidv	⊢ ( 𝑣 = 𝑎 → ( ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑣 + 𝑏 ) ↔ ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 + 𝑏 ) ) )
48	47	cbvrexvw	⊢ ( ∃ 𝑣 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑣 + 𝑏 ) ↔ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 + 𝑏 ) )
49	41	2rexbidv	⊢ ( 𝑧 = 𝑤 → ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 + 𝑏 ) ↔ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 + 𝑏 ) ) )
50	48 49	bitrid	⊢ ( 𝑧 = 𝑤 → ( ∃ 𝑣 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑣 + 𝑏 ) ↔ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 + 𝑏 ) ) )
51	21 50 7	elab2	⊢ ( 𝑤 ∈ 𝐶 ↔ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 + 𝑏 ) )
52	44 51	sylibr	⊢ ( ( 𝑎 ∈ 𝐴 ∧ ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 + 𝑏 ) ) → 𝑤 ∈ 𝐶 )
53	52	ex	⊢ ( 𝑎 ∈ 𝐴 → ( ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 + 𝑏 ) → 𝑤 ∈ 𝐶 ) )
54	1	sseld	⊢ ( 𝜑 → ( 𝑎 ∈ 𝐴 → 𝑎 ∈ ℝ ) )
55	4	sseld	⊢ ( 𝜑 → ( 𝑏 ∈ 𝐵 → 𝑏 ∈ ℝ ) )
56	54 55	anim12d	⊢ ( 𝜑 → ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) )
57		readdcl	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( 𝑎 + 𝑏 ) ∈ ℝ )
58	56 57	syl6	⊢ ( 𝜑 → ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 + 𝑏 ) ∈ ℝ ) )
59		eleq1a	⊢ ( ( 𝑎 + 𝑏 ) ∈ ℝ → ( 𝑤 = ( 𝑎 + 𝑏 ) → 𝑤 ∈ ℝ ) )
60	58 59	syl6	⊢ ( 𝜑 → ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑤 = ( 𝑎 + 𝑏 ) → 𝑤 ∈ ℝ ) ) )
61	60	rexlimdvv	⊢ ( 𝜑 → ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 + 𝑏 ) → 𝑤 ∈ ℝ ) )
62	51 61	biimtrid	⊢ ( 𝜑 → ( 𝑤 ∈ 𝐶 → 𝑤 ∈ ℝ ) )
63	62	ssrdv	⊢ ( 𝜑 → 𝐶 ⊆ ℝ )
64		ovex	⊢ ( 𝑎 + 𝑏 ) ∈ V
65	64	isseti	⊢ ∃ 𝑤 𝑤 = ( 𝑎 + 𝑏 )
66	65	rgenw	⊢ ∀ 𝑏 ∈ 𝐵 ∃ 𝑤 𝑤 = ( 𝑎 + 𝑏 )
67		r19.2z	⊢ ( ( 𝐵 ≠ ∅ ∧ ∀ 𝑏 ∈ 𝐵 ∃ 𝑤 𝑤 = ( 𝑎 + 𝑏 ) ) → ∃ 𝑏 ∈ 𝐵 ∃ 𝑤 𝑤 = ( 𝑎 + 𝑏 ) )
68	5 66 67	sylancl	⊢ ( 𝜑 → ∃ 𝑏 ∈ 𝐵 ∃ 𝑤 𝑤 = ( 𝑎 + 𝑏 ) )
69		rexcom4	⊢ ( ∃ 𝑏 ∈ 𝐵 ∃ 𝑤 𝑤 = ( 𝑎 + 𝑏 ) ↔ ∃ 𝑤 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 + 𝑏 ) )
70	68 69	sylib	⊢ ( 𝜑 → ∃ 𝑤 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 + 𝑏 ) )
71	70	ralrimivw	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐴 ∃ 𝑤 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 + 𝑏 ) )
72		r19.2z	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑎 ∈ 𝐴 ∃ 𝑤 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 + 𝑏 ) ) → ∃ 𝑎 ∈ 𝐴 ∃ 𝑤 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 + 𝑏 ) )
73	2 71 72	syl2anc	⊢ ( 𝜑 → ∃ 𝑎 ∈ 𝐴 ∃ 𝑤 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 + 𝑏 ) )
74		rexcom4	⊢ ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑤 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 + 𝑏 ) ↔ ∃ 𝑤 ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 + 𝑏 ) )
75	73 74	sylib	⊢ ( 𝜑 → ∃ 𝑤 ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 + 𝑏 ) )
76		n0	⊢ ( 𝐶 ≠ ∅ ↔ ∃ 𝑤 𝑤 ∈ 𝐶 )
77	51	exbii	⊢ ( ∃ 𝑤 𝑤 ∈ 𝐶 ↔ ∃ 𝑤 ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 + 𝑏 ) )
78	76 77	bitri	⊢ ( 𝐶 ≠ ∅ ↔ ∃ 𝑤 ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 + 𝑏 ) )
79	75 78	sylibr	⊢ ( 𝜑 → 𝐶 ≠ ∅ )
80	1 2 3	suprcld	⊢ ( 𝜑 → sup ( 𝐴 , ℝ , < ) ∈ ℝ )
81	80 8	readdcld	⊢ ( 𝜑 → ( sup ( 𝐴 , ℝ , < ) + sup ( 𝐵 , ℝ , < ) ) ∈ ℝ )
82	11	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑎 ∈ ℝ )
83	30	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑏 ∈ ℝ )
84	80	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → sup ( 𝐴 , ℝ , < ) ∈ ℝ )
85	8	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → sup ( 𝐵 , ℝ , < ) ∈ ℝ )
86	1 2 3	3jca	⊢ ( 𝜑 → ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) )
87		suprub	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ≤ sup ( 𝐴 , ℝ , < ) )
88	86 87	sylan	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ≤ sup ( 𝐴 , ℝ , < ) )
89	88	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑎 ≤ sup ( 𝐴 , ℝ , < ) )
90	4 5 6	3jca	⊢ ( 𝜑 → ( 𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑦 ≤ 𝑥 ) )
91		suprub	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑦 ≤ 𝑥 ) ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ≤ sup ( 𝐵 , ℝ , < ) )
92	90 91	sylan	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ≤ sup ( 𝐵 , ℝ , < ) )
93	92	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑏 ≤ sup ( 𝐵 , ℝ , < ) )
94	82 83 84 85 89 93	le2addd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 + 𝑏 ) ≤ ( sup ( 𝐴 , ℝ , < ) + sup ( 𝐵 , ℝ , < ) ) )
95	94	ex	⊢ ( 𝜑 → ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 + 𝑏 ) ≤ ( sup ( 𝐴 , ℝ , < ) + sup ( 𝐵 , ℝ , < ) ) ) )
96		breq1	⊢ ( 𝑤 = ( 𝑎 + 𝑏 ) → ( 𝑤 ≤ ( sup ( 𝐴 , ℝ , < ) + sup ( 𝐵 , ℝ , < ) ) ↔ ( 𝑎 + 𝑏 ) ≤ ( sup ( 𝐴 , ℝ , < ) + sup ( 𝐵 , ℝ , < ) ) ) )
97	96	biimprcd	⊢ ( ( 𝑎 + 𝑏 ) ≤ ( sup ( 𝐴 , ℝ , < ) + sup ( 𝐵 , ℝ , < ) ) → ( 𝑤 = ( 𝑎 + 𝑏 ) → 𝑤 ≤ ( sup ( 𝐴 , ℝ , < ) + sup ( 𝐵 , ℝ , < ) ) ) )
98	95 97	syl6	⊢ ( 𝜑 → ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑤 = ( 𝑎 + 𝑏 ) → 𝑤 ≤ ( sup ( 𝐴 , ℝ , < ) + sup ( 𝐵 , ℝ , < ) ) ) ) )
99	98	rexlimdvv	⊢ ( 𝜑 → ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 + 𝑏 ) → 𝑤 ≤ ( sup ( 𝐴 , ℝ , < ) + sup ( 𝐵 , ℝ , < ) ) ) )
100	51 99	biimtrid	⊢ ( 𝜑 → ( 𝑤 ∈ 𝐶 → 𝑤 ≤ ( sup ( 𝐴 , ℝ , < ) + sup ( 𝐵 , ℝ , < ) ) ) )
101	100	ralrimiv	⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝐶 𝑤 ≤ ( sup ( 𝐴 , ℝ , < ) + sup ( 𝐵 , ℝ , < ) ) )
102		brralrspcev	⊢ ( ( ( sup ( 𝐴 , ℝ , < ) + sup ( 𝐵 , ℝ , < ) ) ∈ ℝ ∧ ∀ 𝑤 ∈ 𝐶 𝑤 ≤ ( sup ( 𝐴 , ℝ , < ) + sup ( 𝐵 , ℝ , < ) ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝐶 𝑤 ≤ 𝑥 )
103	81 101 102	syl2anc	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝐶 𝑤 ≤ 𝑥 )
104		suprub	⊢ ( ( ( 𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝐶 𝑤 ≤ 𝑥 ) ∧ 𝑤 ∈ 𝐶 ) → 𝑤 ≤ sup ( 𝐶 , ℝ , < ) )
105	104	ex	⊢ ( ( 𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝐶 𝑤 ≤ 𝑥 ) → ( 𝑤 ∈ 𝐶 → 𝑤 ≤ sup ( 𝐶 , ℝ , < ) ) )
106	63 79 103 105	syl3anc	⊢ ( 𝜑 → ( 𝑤 ∈ 𝐶 → 𝑤 ≤ sup ( 𝐶 , ℝ , < ) ) )
107	53 106	sylan9r	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 + 𝑏 ) → 𝑤 ≤ sup ( 𝐶 , ℝ , < ) ) )
108	43 107	biimtrid	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑤 ∈ { 𝑧 ∣ ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 + 𝑏 ) } → 𝑤 ≤ sup ( 𝐶 , ℝ , < ) ) )
109	108	ralrimiv	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ∀ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 + 𝑏 ) } 𝑤 ≤ sup ( 𝐶 , ℝ , < ) )
110	33 31	readdcld	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 + 𝑏 ) ∈ ℝ )
111		eleq1a	⊢ ( ( 𝑎 + 𝑏 ) ∈ ℝ → ( 𝑧 = ( 𝑎 + 𝑏 ) → 𝑧 ∈ ℝ ) )
112	110 111	syl	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑧 = ( 𝑎 + 𝑏 ) → 𝑧 ∈ ℝ ) )
113	112	rexlimdva	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 + 𝑏 ) → 𝑧 ∈ ℝ ) )
114	113	abssdv	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → { 𝑧 ∣ ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 + 𝑏 ) } ⊆ ℝ )
115	64	isseti	⊢ ∃ 𝑧 𝑧 = ( 𝑎 + 𝑏 )
116	115	rgenw	⊢ ∀ 𝑏 ∈ 𝐵 ∃ 𝑧 𝑧 = ( 𝑎 + 𝑏 )
117		r19.2z	⊢ ( ( 𝐵 ≠ ∅ ∧ ∀ 𝑏 ∈ 𝐵 ∃ 𝑧 𝑧 = ( 𝑎 + 𝑏 ) ) → ∃ 𝑏 ∈ 𝐵 ∃ 𝑧 𝑧 = ( 𝑎 + 𝑏 ) )
118	5 116 117	sylancl	⊢ ( 𝜑 → ∃ 𝑏 ∈ 𝐵 ∃ 𝑧 𝑧 = ( 𝑎 + 𝑏 ) )
119		rexcom4	⊢ ( ∃ 𝑏 ∈ 𝐵 ∃ 𝑧 𝑧 = ( 𝑎 + 𝑏 ) ↔ ∃ 𝑧 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 + 𝑏 ) )
120	118 119	sylib	⊢ ( 𝜑 → ∃ 𝑧 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 + 𝑏 ) )
121		abn0	⊢ ( { 𝑧 ∣ ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 + 𝑏 ) } ≠ ∅ ↔ ∃ 𝑧 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 + 𝑏 ) )
122	120 121	sylibr	⊢ ( 𝜑 → { 𝑧 ∣ ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 + 𝑏 ) } ≠ ∅ )
123	122	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → { 𝑧 ∣ ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 + 𝑏 ) } ≠ ∅ )
124	63 79 103	suprcld	⊢ ( 𝜑 → sup ( 𝐶 , ℝ , < ) ∈ ℝ )
125	124	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → sup ( 𝐶 , ℝ , < ) ∈ ℝ )
126		brralrspcev	⊢ ( ( sup ( 𝐶 , ℝ , < ) ∈ ℝ ∧ ∀ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 + 𝑏 ) } 𝑤 ≤ sup ( 𝐶 , ℝ , < ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 + 𝑏 ) } 𝑤 ≤ 𝑥 )
127	125 109 126	syl2anc	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 + 𝑏 ) } 𝑤 ≤ 𝑥 )
128		suprleub	⊢ ( ( ( { 𝑧 ∣ ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 + 𝑏 ) } ⊆ ℝ ∧ { 𝑧 ∣ ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 + 𝑏 ) } ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 + 𝑏 ) } 𝑤 ≤ 𝑥 ) ∧ sup ( 𝐶 , ℝ , < ) ∈ ℝ ) → ( sup ( { 𝑧 ∣ ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 + 𝑏 ) } , ℝ , < ) ≤ sup ( 𝐶 , ℝ , < ) ↔ ∀ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 + 𝑏 ) } 𝑤 ≤ sup ( 𝐶 , ℝ , < ) ) )
129	114 123 127 125 128	syl31anc	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( sup ( { 𝑧 ∣ ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 + 𝑏 ) } , ℝ , < ) ≤ sup ( 𝐶 , ℝ , < ) ↔ ∀ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 + 𝑏 ) } 𝑤 ≤ sup ( 𝐶 , ℝ , < ) ) )
130	109 129	mpbird	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → sup ( { 𝑧 ∣ ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 + 𝑏 ) } , ℝ , < ) ≤ sup ( 𝐶 , ℝ , < ) )
131	40 130	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) ≤ sup ( 𝐶 , ℝ , < ) )
132		breq1	⊢ ( 𝑤 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) → ( 𝑤 ≤ sup ( 𝐶 , ℝ , < ) ↔ ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) ≤ sup ( 𝐶 , ℝ , < ) ) )
133	131 132	syl5ibrcom	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑤 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) → 𝑤 ≤ sup ( 𝐶 , ℝ , < ) ) )
134	133	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑎 ∈ 𝐴 𝑤 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) → 𝑤 ≤ sup ( 𝐶 , ℝ , < ) ) )
135	24 134	biimtrid	⊢ ( 𝜑 → ( 𝑤 ∈ { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) } → 𝑤 ≤ sup ( 𝐶 , ℝ , < ) ) )
136	135	ralrimiv	⊢ ( 𝜑 → ∀ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) } 𝑤 ≤ sup ( 𝐶 , ℝ , < ) )
137	13 11	readdcld	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) ∈ ℝ )
138		eleq1a	⊢ ( ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) ∈ ℝ → ( 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) → 𝑧 ∈ ℝ ) )
139	137 138	syl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) → 𝑧 ∈ ℝ ) )
140	139	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑎 ∈ 𝐴 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) → 𝑧 ∈ ℝ ) )
141	140	abssdv	⊢ ( 𝜑 → { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) } ⊆ ℝ )
142		ovex	⊢ ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) ∈ V
143	142	isseti	⊢ ∃ 𝑧 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 )
144	143	rgenw	⊢ ∀ 𝑎 ∈ 𝐴 ∃ 𝑧 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 )
145		r19.2z	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑎 ∈ 𝐴 ∃ 𝑧 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) ) → ∃ 𝑎 ∈ 𝐴 ∃ 𝑧 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) )
146	2 144 145	sylancl	⊢ ( 𝜑 → ∃ 𝑎 ∈ 𝐴 ∃ 𝑧 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) )
147		rexcom4	⊢ ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑧 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) ↔ ∃ 𝑧 ∃ 𝑎 ∈ 𝐴 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) )
148	146 147	sylib	⊢ ( 𝜑 → ∃ 𝑧 ∃ 𝑎 ∈ 𝐴 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) )
149		abn0	⊢ ( { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) } ≠ ∅ ↔ ∃ 𝑧 ∃ 𝑎 ∈ 𝐴 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) )
150	148 149	sylibr	⊢ ( 𝜑 → { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) } ≠ ∅ )
151		brralrspcev	⊢ ( ( sup ( 𝐶 , ℝ , < ) ∈ ℝ ∧ ∀ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) } 𝑤 ≤ sup ( 𝐶 , ℝ , < ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) } 𝑤 ≤ 𝑥 )
152	124 136 151	syl2anc	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) } 𝑤 ≤ 𝑥 )
153		suprleub	⊢ ( ( ( { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) } ⊆ ℝ ∧ { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) } ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) } 𝑤 ≤ 𝑥 ) ∧ sup ( 𝐶 , ℝ , < ) ∈ ℝ ) → ( sup ( { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) } , ℝ , < ) ≤ sup ( 𝐶 , ℝ , < ) ↔ ∀ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) } 𝑤 ≤ sup ( 𝐶 , ℝ , < ) ) )
154	141 150 152 124 153	syl31anc	⊢ ( 𝜑 → ( sup ( { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) } , ℝ , < ) ≤ sup ( 𝐶 , ℝ , < ) ↔ ∀ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) } 𝑤 ≤ sup ( 𝐶 , ℝ , < ) ) )
155	136 154	mpbird	⊢ ( 𝜑 → sup ( { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = ( sup ( 𝐵 , ℝ , < ) + 𝑎 ) } , ℝ , < ) ≤ sup ( 𝐶 , ℝ , < ) )
156	20 155	eqbrtrd	⊢ ( 𝜑 → ( sup ( 𝐴 , ℝ , < ) + sup ( 𝐵 , ℝ , < ) ) ≤ sup ( 𝐶 , ℝ , < ) )
157		suprleub	⊢ ( ( ( 𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝐶 𝑤 ≤ 𝑥 ) ∧ ( sup ( 𝐴 , ℝ , < ) + sup ( 𝐵 , ℝ , < ) ) ∈ ℝ ) → ( sup ( 𝐶 , ℝ , < ) ≤ ( sup ( 𝐴 , ℝ , < ) + sup ( 𝐵 , ℝ , < ) ) ↔ ∀ 𝑤 ∈ 𝐶 𝑤 ≤ ( sup ( 𝐴 , ℝ , < ) + sup ( 𝐵 , ℝ , < ) ) ) )
158	63 79 103 81 157	syl31anc	⊢ ( 𝜑 → ( sup ( 𝐶 , ℝ , < ) ≤ ( sup ( 𝐴 , ℝ , < ) + sup ( 𝐵 , ℝ , < ) ) ↔ ∀ 𝑤 ∈ 𝐶 𝑤 ≤ ( sup ( 𝐴 , ℝ , < ) + sup ( 𝐵 , ℝ , < ) ) ) )
159	101 158	mpbird	⊢ ( 𝜑 → sup ( 𝐶 , ℝ , < ) ≤ ( sup ( 𝐴 , ℝ , < ) + sup ( 𝐵 , ℝ , < ) ) )
160	81 124	letri3d	⊢ ( 𝜑 → ( ( sup ( 𝐴 , ℝ , < ) + sup ( 𝐵 , ℝ , < ) ) = sup ( 𝐶 , ℝ , < ) ↔ ( ( sup ( 𝐴 , ℝ , < ) + sup ( 𝐵 , ℝ , < ) ) ≤ sup ( 𝐶 , ℝ , < ) ∧ sup ( 𝐶 , ℝ , < ) ≤ ( sup ( 𝐴 , ℝ , < ) + sup ( 𝐵 , ℝ , < ) ) ) ) )
161	156 159 160	mpbir2and	⊢ ( 𝜑 → ( sup ( 𝐴 , ℝ , < ) + sup ( 𝐵 , ℝ , < ) ) = sup ( 𝐶 , ℝ , < ) )