Metamath Proof Explorer

Theorem suprnmpt

Description: An explicit bound for the range of a bounded function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses suprnmpt.a ⊢ φ → A ≠ ∅
suprnmpt.b ⊢ φ ∧ x ∈ A → B ∈ ℝ
suprnmpt.bnd ⊢ φ → ∃ y ∈ ℝ ∀ x ∈ A B ≤ y
suprnmpt.f ⊢ F = x ∈ A ⟼ B
suprnmpt.c ⊢ C = sup ran ⁡ F ℝ <
Assertion suprnmpt ⊢ φ → C ∈ ℝ ∧ ∀ x ∈ A B ≤ C

Proof

Step Hyp Ref Expression
1 suprnmpt.a ⊢ φ → A ≠ ∅
2 suprnmpt.b ⊢ φ ∧ x ∈ A → B ∈ ℝ
3 suprnmpt.bnd ⊢ φ → ∃ y ∈ ℝ ∀ x ∈ A B ≤ y
4 suprnmpt.f ⊢ F = x ∈ A ⟼ B
5 suprnmpt.c ⊢ C = sup ran ⁡ F ℝ <
6 2 ralrimiva ⊢ φ → ∀ x ∈ A B ∈ ℝ
7 4 rnmptss ⊢ ∀ x ∈ A B ∈ ℝ → ran ⁡ F ⊆ ℝ
8 6 7 syl ⊢ φ → ran ⁡ F ⊆ ℝ
9 nfv ⊢ Ⅎ x φ
10 9 2 4 1 rnmptn0 ⊢ φ → ran ⁡ F ≠ ∅
11 nfv ⊢ Ⅎ y φ
12 nfre1 ⊢ Ⅎ y ∃ y ∈ ℝ ∀ z ∈ ran ⁡ F z ≤ y
13 simp2 ⊢ φ ∧ y ∈ ℝ ∧ ∀ x ∈ A B ≤ y → y ∈ ℝ
14 simpl1 ⊢ φ ∧ y ∈ ℝ ∧ ∀ x ∈ A B ≤ y ∧ z ∈ ran ⁡ F → φ
15 simpl3 ⊢ φ ∧ y ∈ ℝ ∧ ∀ x ∈ A B ≤ y ∧ z ∈ ran ⁡ F → ∀ x ∈ A B ≤ y
16 vex ⊢ z ∈ V
17 4 elrnmpt ⊢ z ∈ V → z ∈ ran ⁡ F ↔ ∃ x ∈ A z = B
18 16 17 ax-mp ⊢ z ∈ ran ⁡ F ↔ ∃ x ∈ A z = B
19 18 bilani ⊢ φ ∧ y ∈ ℝ ∧ ∀ x ∈ A B ≤ y ∧ z ∈ ran ⁡ F → ∃ x ∈ A z = B
20 simp3 ⊢ φ ∧ ∀ x ∈ A B ≤ y ∧ ∃ x ∈ A z = B → ∃ x ∈ A z = B
21 nfra1 ⊢ Ⅎ x ∀ x ∈ A B ≤ y
22 nfre1 ⊢ Ⅎ x ∃ x ∈ A z = B
23 9 21 22 nf3an ⊢ Ⅎ x φ ∧ ∀ x ∈ A B ≤ y ∧ ∃ x ∈ A z = B
24 nfv ⊢ Ⅎ x z ≤ y
25 simp3 ⊢ ∀ x ∈ A B ≤ y ∧ x ∈ A ∧ z = B → z = B
26 rspa ⊢ ∀ x ∈ A B ≤ y ∧ x ∈ A → B ≤ y
27 26 3adant3 ⊢ ∀ x ∈ A B ≤ y ∧ x ∈ A ∧ z = B → B ≤ y
28 25 27 eqbrtrd ⊢ ∀ x ∈ A B ≤ y ∧ x ∈ A ∧ z = B → z ≤ y
29 28 3exp ⊢ ∀ x ∈ A B ≤ y → x ∈ A → z = B → z ≤ y
30 29 3ad2ant2 ⊢ φ ∧ ∀ x ∈ A B ≤ y ∧ ∃ x ∈ A z = B → x ∈ A → z = B → z ≤ y
31 23 24 30 rexlimd ⊢ φ ∧ ∀ x ∈ A B ≤ y ∧ ∃ x ∈ A z = B → ∃ x ∈ A z = B → z ≤ y
32 20 31 mpd ⊢ φ ∧ ∀ x ∈ A B ≤ y ∧ ∃ x ∈ A z = B → z ≤ y
33 14 15 19 32 syl3anc ⊢ φ ∧ y ∈ ℝ ∧ ∀ x ∈ A B ≤ y ∧ z ∈ ran ⁡ F → z ≤ y
34 33 ralrimiva ⊢ φ ∧ y ∈ ℝ ∧ ∀ x ∈ A B ≤ y → ∀ z ∈ ran ⁡ F z ≤ y
35 19.8a ⊢ y ∈ ℝ ∧ ∀ z ∈ ran ⁡ F z ≤ y → ∃ y y ∈ ℝ ∧ ∀ z ∈ ran ⁡ F z ≤ y
36 13 34 35 syl2anc ⊢ φ ∧ y ∈ ℝ ∧ ∀ x ∈ A B ≤ y → ∃ y y ∈ ℝ ∧ ∀ z ∈ ran ⁡ F z ≤ y
37 df-rex ⊢ ∃ y ∈ ℝ ∀ z ∈ ran ⁡ F z ≤ y ↔ ∃ y y ∈ ℝ ∧ ∀ z ∈ ran ⁡ F z ≤ y
38 36 37 sylibr ⊢ φ ∧ y ∈ ℝ ∧ ∀ x ∈ A B ≤ y → ∃ y ∈ ℝ ∀ z ∈ ran ⁡ F z ≤ y
39 38 3exp ⊢ φ → y ∈ ℝ → ∀ x ∈ A B ≤ y → ∃ y ∈ ℝ ∀ z ∈ ran ⁡ F z ≤ y
40 11 12 39 rexlimd ⊢ φ → ∃ y ∈ ℝ ∀ x ∈ A B ≤ y → ∃ y ∈ ℝ ∀ z ∈ ran ⁡ F z ≤ y
41 3 40 mpd ⊢ φ → ∃ y ∈ ℝ ∀ z ∈ ran ⁡ F z ≤ y
42 suprcl ⊢ ran ⁡ F ⊆ ℝ ∧ ran ⁡ F ≠ ∅ ∧ ∃ y ∈ ℝ ∀ z ∈ ran ⁡ F z ≤ y → sup ran ⁡ F ℝ < ∈ ℝ
43 8 10 41 42 syl3anc ⊢ φ → sup ran ⁡ F ℝ < ∈ ℝ
44 5 43 eqeltrid ⊢ φ → C ∈ ℝ
45 8 adantr ⊢ φ ∧ x ∈ A → ran ⁡ F ⊆ ℝ
46 simpr ⊢ φ ∧ x ∈ A → x ∈ A
47 4 elrnmpt1 ⊢ x ∈ A ∧ B ∈ ℝ → B ∈ ran ⁡ F
48 46 2 47 syl2anc ⊢ φ ∧ x ∈ A → B ∈ ran ⁡ F
49 48 ne0d ⊢ φ ∧ x ∈ A → ran ⁡ F ≠ ∅
50 41 adantr ⊢ φ ∧ x ∈ A → ∃ y ∈ ℝ ∀ z ∈ ran ⁡ F z ≤ y
51 suprub ⊢ ran ⁡ F ⊆ ℝ ∧ ran ⁡ F ≠ ∅ ∧ ∃ y ∈ ℝ ∀ z ∈ ran ⁡ F z ≤ y ∧ B ∈ ran ⁡ F → B ≤ sup ran ⁡ F ℝ <
52 45 49 50 48 51 syl31anc ⊢ φ ∧ x ∈ A → B ≤ sup ran ⁡ F ℝ <
53 52 5 breqtrrdi ⊢ φ ∧ x ∈ A → B ≤ C
54 53 ralrimiva ⊢ φ → ∀ x ∈ A B ≤ C
55 44 54 jca ⊢ φ → C ∈ ℝ ∧ ∀ x ∈ A B ≤ C