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 nfmpt1 ⊢ Ⅎ _ x x ∈ A ⟼ B
11 4 10 nfcxfr ⊢ Ⅎ _ x F
12 11 nfrn ⊢ Ⅎ _ x ran ⁡ F
13 nfcv ⊢ Ⅎ _ x ∅
14 12 13 nfne ⊢ Ⅎ x ran ⁡ F ≠ ∅
15 n0 ⊢ A ≠ ∅ ↔ ∃ x x ∈ A
16 1 15 sylib ⊢ φ → ∃ x x ∈ A
17 simpr ⊢ φ ∧ x ∈ A → x ∈ A
18 4 elrnmpt1 ⊢ x ∈ A ∧ B ∈ ℝ → B ∈ ran ⁡ F
19 17 2 18 syl2anc ⊢ φ ∧ x ∈ A → B ∈ ran ⁡ F
20 19 ne0d ⊢ φ ∧ x ∈ A → ran ⁡ F ≠ ∅
21 9 14 16 20 exlimdd ⊢ φ → ran ⁡ F ≠ ∅
22 nfv ⊢ Ⅎ y φ
23 nfre1 ⊢ Ⅎ y ∃ y ∈ ℝ ∀ z ∈ ran ⁡ F z ≤ y
24 simp2 ⊢ φ ∧ y ∈ ℝ ∧ ∀ x ∈ A B ≤ y → y ∈ ℝ
25 simpl1 ⊢ φ ∧ y ∈ ℝ ∧ ∀ x ∈ A B ≤ y ∧ z ∈ ran ⁡ F → φ
26 simpl3 ⊢ φ ∧ y ∈ ℝ ∧ ∀ x ∈ A B ≤ y ∧ z ∈ ran ⁡ F → ∀ x ∈ A B ≤ y
27 vex ⊢ z ∈ V
28 4 elrnmpt ⊢ z ∈ V → z ∈ ran ⁡ F ↔ ∃ x ∈ A z = B
29 27 28 ax-mp ⊢ z ∈ ran ⁡ F ↔ ∃ x ∈ A z = B
30 29 biimpi ⊢ z ∈ ran ⁡ F → ∃ x ∈ A z = B
31 30 adantl ⊢ φ ∧ y ∈ ℝ ∧ ∀ x ∈ A B ≤ y ∧ z ∈ ran ⁡ F → ∃ x ∈ A z = B
32 simp3 ⊢ φ ∧ ∀ x ∈ A B ≤ y ∧ ∃ x ∈ A z = B → ∃ x ∈ A z = B
33 nfra1 ⊢ Ⅎ x ∀ x ∈ A B ≤ y
34 nfre1 ⊢ Ⅎ x ∃ x ∈ A z = B
35 9 33 34 nf3an ⊢ Ⅎ x φ ∧ ∀ x ∈ A B ≤ y ∧ ∃ x ∈ A z = B
36 nfv ⊢ Ⅎ x z ≤ y
37 simp3 ⊢ ∀ x ∈ A B ≤ y ∧ x ∈ A ∧ z = B → z = B
38 rspa ⊢ ∀ x ∈ A B ≤ y ∧ x ∈ A → B ≤ y
39 38 3adant3 ⊢ ∀ x ∈ A B ≤ y ∧ x ∈ A ∧ z = B → B ≤ y
40 37 39 eqbrtrd ⊢ ∀ x ∈ A B ≤ y ∧ x ∈ A ∧ z = B → z ≤ y
41 40 3exp ⊢ ∀ x ∈ A B ≤ y → x ∈ A → z = B → z ≤ y
42 41 3ad2ant2 ⊢ φ ∧ ∀ x ∈ A B ≤ y ∧ ∃ x ∈ A z = B → x ∈ A → z = B → z ≤ y
43 35 36 42 rexlimd ⊢ φ ∧ ∀ x ∈ A B ≤ y ∧ ∃ x ∈ A z = B → ∃ x ∈ A z = B → z ≤ y
44 32 43 mpd ⊢ φ ∧ ∀ x ∈ A B ≤ y ∧ ∃ x ∈ A z = B → z ≤ y
45 25 26 31 44 syl3anc ⊢ φ ∧ y ∈ ℝ ∧ ∀ x ∈ A B ≤ y ∧ z ∈ ran ⁡ F → z ≤ y
46 45 ralrimiva ⊢ φ ∧ y ∈ ℝ ∧ ∀ x ∈ A B ≤ y → ∀ z ∈ ran ⁡ F z ≤ y
47 19.8a ⊢ y ∈ ℝ ∧ ∀ z ∈ ran ⁡ F z ≤ y → ∃ y y ∈ ℝ ∧ ∀ z ∈ ran ⁡ F z ≤ y
48 24 46 47 syl2anc ⊢ φ ∧ y ∈ ℝ ∧ ∀ x ∈ A B ≤ y → ∃ y y ∈ ℝ ∧ ∀ z ∈ ran ⁡ F z ≤ y
49 df-rex ⊢ ∃ y ∈ ℝ ∀ z ∈ ran ⁡ F z ≤ y ↔ ∃ y y ∈ ℝ ∧ ∀ z ∈ ran ⁡ F z ≤ y
50 48 49 sylibr ⊢ φ ∧ y ∈ ℝ ∧ ∀ x ∈ A B ≤ y → ∃ y ∈ ℝ ∀ z ∈ ran ⁡ F z ≤ y
51 50 3exp ⊢ φ → y ∈ ℝ → ∀ x ∈ A B ≤ y → ∃ y ∈ ℝ ∀ z ∈ ran ⁡ F z ≤ y
52 22 23 51 rexlimd ⊢ φ → ∃ y ∈ ℝ ∀ x ∈ A B ≤ y → ∃ y ∈ ℝ ∀ z ∈ ran ⁡ F z ≤ y
53 3 52 mpd ⊢ φ → ∃ y ∈ ℝ ∀ z ∈ ran ⁡ F z ≤ y
54 suprcl ⊢ ran ⁡ F ⊆ ℝ ∧ ran ⁡ F ≠ ∅ ∧ ∃ y ∈ ℝ ∀ z ∈ ran ⁡ F z ≤ y → sup ran ⁡ F ℝ < ∈ ℝ
55 8 21 53 54 syl3anc ⊢ φ → sup ran ⁡ F ℝ < ∈ ℝ
56 5 55 eqeltrid ⊢ φ → C ∈ ℝ
57 8 adantr ⊢ φ ∧ x ∈ A → ran ⁡ F ⊆ ℝ
58 53 adantr ⊢ φ ∧ x ∈ A → ∃ y ∈ ℝ ∀ z ∈ ran ⁡ F z ≤ y
59 suprub ⊢ ran ⁡ F ⊆ ℝ ∧ ran ⁡ F ≠ ∅ ∧ ∃ y ∈ ℝ ∀ z ∈ ran ⁡ F z ≤ y ∧ B ∈ ran ⁡ F → B ≤ sup ran ⁡ F ℝ <
60 57 20 58 19 59 syl31anc ⊢ φ ∧ x ∈ A → B ≤ sup ran ⁡ F ℝ <
61 60 5 breqtrrdi ⊢ φ ∧ x ∈ A → B ≤ C
62 61 ralrimiva ⊢ φ → ∀ x ∈ A B ≤ C
63 56 62 jca ⊢ φ → C ∈ ℝ ∧ ∀ x ∈ A B ≤ C