Theorem upbdrech

Description: Choice of an upper bound for a nonempty bunded set (image set version). (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	upbdrech.a	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
	upbdrech.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
	upbdrech.bd	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 )
	upbdrech.c	⊢ 𝐶 = sup ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } , ℝ , < )
Assertion	upbdrech	⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		upbdrech.a	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
2		upbdrech.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
3		upbdrech.bd	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 )
4		upbdrech.c	⊢ 𝐶 = sup ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } , ℝ , < )
5	2	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ℝ )
6		nfra1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ℝ
7		nfv	⊢ Ⅎ 𝑥 𝑧 ∈ ℝ
8		simp3	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵 ) → 𝑧 = 𝐵 )
9		rspa	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
10	9	3adant3	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵 ) → 𝐵 ∈ ℝ )
11	8 10	eqeltrd	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵 ) → 𝑧 ∈ ℝ )
12	11	3exp	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ℝ → ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝑧 ∈ ℝ ) ) )
13	6 7 12	rexlimd	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ℝ → ( ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑧 ∈ ℝ ) )
14	13	abssdv	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ℝ → { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ⊆ ℝ )
15	5 14	syl	⊢ ( 𝜑 → { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ⊆ ℝ )
16		eqidd	⊢ ( 𝑥 ∈ 𝐴 → 𝐵 = 𝐵 )
17	16	rgen	⊢ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐵
18		r19.2z	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝐵 = 𝐵 )
19	1 17 18	sylancl	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 𝐵 = 𝐵 )
20		nfv	⊢ Ⅎ 𝑥 𝜑
21		nfre1	⊢ Ⅎ 𝑥 ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵
22	21	nfex	⊢ Ⅎ 𝑥 ∃ 𝑧 ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵
23		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
24		elex	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ V )
25	2 24	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ V )
26		isset	⊢ ( 𝐵 ∈ V ↔ ∃ 𝑧 𝑧 = 𝐵 )
27	25 26	sylib	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑧 𝑧 = 𝐵 )
28		rspe	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑧 𝑧 = 𝐵 ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑧 𝑧 = 𝐵 )
29	23 27 28	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑧 𝑧 = 𝐵 )
30		rexcom4	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑧 𝑧 = 𝐵 ↔ ∃ 𝑧 ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 )
31	29 30	sylib	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑧 ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 )
32	31	3adant3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 = 𝐵 ) → ∃ 𝑧 ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 )
33	32	3exp	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝐵 = 𝐵 → ∃ 𝑧 ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) ) )
34	20 22 33	rexlimd	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝐵 = 𝐵 → ∃ 𝑧 ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) )
35	19 34	mpd	⊢ ( 𝜑 → ∃ 𝑧 ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 )
36		abn0	⊢ ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ≠ ∅ ↔ ∃ 𝑧 ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 )
37	35 36	sylibr	⊢ ( 𝜑 → { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ≠ ∅ )
38		vex	⊢ 𝑤 ∈ V
39		eqeq1	⊢ ( 𝑧 = 𝑤 → ( 𝑧 = 𝐵 ↔ 𝑤 = 𝐵 ) )
40	39	rexbidv	⊢ ( 𝑧 = 𝑤 → ( ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑤 = 𝐵 ) )
41	38 40	elab	⊢ ( 𝑤 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ↔ ∃ 𝑥 ∈ 𝐴 𝑤 = 𝐵 )
42	41	bilani	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) ∧ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ) → ∃ 𝑥 ∈ 𝐴 𝑤 = 𝐵 )
43		nfra1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦
44	20 43	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 )
45	21	nfsab	⊢ Ⅎ 𝑥 𝑤 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 }
46	44 45	nfan	⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) ∧ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } )
47		nfv	⊢ Ⅎ 𝑥 𝑤 ≤ 𝑦
48		simp3	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑤 = 𝐵 ) → 𝑤 = 𝐵 )
49		simp1r	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑤 = 𝐵 ) → ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 )
50		simp2	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑤 = 𝐵 ) → 𝑥 ∈ 𝐴 )
51		rspa	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ 𝑦 )
52	49 50 51	syl2anc	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑤 = 𝐵 ) → 𝐵 ≤ 𝑦 )
53	48 52	eqbrtrd	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑤 = 𝐵 ) → 𝑤 ≤ 𝑦 )
54	53	3exp	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) → ( 𝑥 ∈ 𝐴 → ( 𝑤 = 𝐵 → 𝑤 ≤ 𝑦 ) ) )
55	54	adantr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) ∧ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ) → ( 𝑥 ∈ 𝐴 → ( 𝑤 = 𝐵 → 𝑤 ≤ 𝑦 ) ) )
56	46 47 55	rexlimd	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) ∧ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ) → ( ∃ 𝑥 ∈ 𝐴 𝑤 = 𝐵 → 𝑤 ≤ 𝑦 ) )
57	42 56	mpd	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) ∧ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ) → 𝑤 ≤ 𝑦 )
58	57	ralrimiva	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) → ∀ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } 𝑤 ≤ 𝑦 )
59	58	3adant2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) → ∀ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } 𝑤 ≤ 𝑦 )
60	59	3exp	⊢ ( 𝜑 → ( 𝑦 ∈ ℝ → ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 → ∀ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } 𝑤 ≤ 𝑦 ) ) )
61	60	reximdvai	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 → ∃ 𝑦 ∈ ℝ ∀ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } 𝑤 ≤ 𝑦 ) )
62	3 61	mpd	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } 𝑤 ≤ 𝑦 )
63		suprcl	⊢ ( ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ⊆ ℝ ∧ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } 𝑤 ≤ 𝑦 ) → sup ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } , ℝ , < ) ∈ ℝ )
64	15 37 62 63	syl3anc	⊢ ( 𝜑 → sup ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } , ℝ , < ) ∈ ℝ )
65	4 64	eqeltrid	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
66	15	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ⊆ ℝ )
67	31 36	sylibr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ≠ ∅ )
68	62	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } 𝑤 ≤ 𝑦 )
69		elabrexg	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } )
70	23 2 69	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } )
71		suprub	⊢ ( ( ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ⊆ ℝ ∧ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } 𝑤 ≤ 𝑦 ) ∧ 𝐵 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ) → 𝐵 ≤ sup ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } , ℝ , < ) )
72	66 67 68 70 71	syl31anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ sup ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } , ℝ , < ) )
73	72 4	breqtrrdi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ 𝐶 )
74	73	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 )
75	65 74	jca	⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 ) )