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 biimpi ⊢ z ∈ ran ⁡ F → ∃ x ∈ A z = B
20 19 adantl ⊢ φ ∧ y ∈ ℝ ∧ ∀ x ∈ A B ≤ y ∧ z ∈ ran ⁡ F → ∃ x ∈ A z = B
21 simp3 ⊢ φ ∧ ∀ x ∈ A B ≤ y ∧ ∃ x ∈ A z = B → ∃ x ∈ A z = B
22 nfra1 ⊢ Ⅎ x ∀ x ∈ A B ≤ y
23 nfre1 ⊢ Ⅎ x ∃ x ∈ A z = B
24 9 22 23 nf3an ⊢ Ⅎ x φ ∧ ∀ x ∈ A B ≤ y ∧ ∃ x ∈ A z = B
25 nfv ⊢ Ⅎ x z ≤ y
26 simp3 ⊢ ∀ x ∈ A B ≤ y ∧ x ∈ A ∧ z = B → z = B
27 rspa ⊢ ∀ x ∈ A B ≤ y ∧ x ∈ A → B ≤ y
28 27 3adant3 ⊢ ∀ x ∈ A B ≤ y ∧ x ∈ A ∧ z = B → B ≤ y
29 26 28 eqbrtrd ⊢ ∀ x ∈ A B ≤ y ∧ x ∈ A ∧ z = B → z ≤ y
30 29 3exp ⊢ ∀ x ∈ A B ≤ y → x ∈ A → z = B → z ≤ y
31 30 3ad2ant2 ⊢ φ ∧ ∀ x ∈ A B ≤ y ∧ ∃ x ∈ A z = B → x ∈ A → z = B → z ≤ y
32 24 25 31 rexlimd ⊢ φ ∧ ∀ x ∈ A B ≤ y ∧ ∃ x ∈ A z = B → ∃ x ∈ A z = B → z ≤ y
33 21 32 mpd ⊢ φ ∧ ∀ x ∈ A B ≤ y ∧ ∃ x ∈ A z = B → z ≤ y
34 14 15 20 33 syl3anc ⊢ φ ∧ y ∈ ℝ ∧ ∀ x ∈ A B ≤ y ∧ z ∈ ran ⁡ F → z ≤ y
35 34 ralrimiva ⊢ φ ∧ y ∈ ℝ ∧ ∀ x ∈ A B ≤ y → ∀ z ∈ ran ⁡ F z ≤ y
36 19.8a ⊢ y ∈ ℝ ∧ ∀ z ∈ ran ⁡ F z ≤ y → ∃ y y ∈ ℝ ∧ ∀ z ∈ ran ⁡ F z ≤ y
37 13 35 36 syl2anc ⊢ φ ∧ y ∈ ℝ ∧ ∀ x ∈ A B ≤ y → ∃ y y ∈ ℝ ∧ ∀ z ∈ ran ⁡ F z ≤ y
38 df-rex ⊢ ∃ y ∈ ℝ ∀ z ∈ ran ⁡ F z ≤ y ↔ ∃ y y ∈ ℝ ∧ ∀ z ∈ ran ⁡ F z ≤ y
39 37 38 sylibr ⊢ φ ∧ y ∈ ℝ ∧ ∀ x ∈ A B ≤ y → ∃ y ∈ ℝ ∀ z ∈ ran ⁡ F z ≤ y
40 39 3exp ⊢ φ → y ∈ ℝ → ∀ x ∈ A B ≤ y → ∃ y ∈ ℝ ∀ z ∈ ran ⁡ F z ≤ y
41 11 12 40 rexlimd ⊢ φ → ∃ y ∈ ℝ ∀ x ∈ A B ≤ y → ∃ y ∈ ℝ ∀ z ∈ ran ⁡ F z ≤ y
42 3 41 mpd ⊢ φ → ∃ y ∈ ℝ ∀ z ∈ ran ⁡ F z ≤ y
43 suprcl ⊢ ran ⁡ F ⊆ ℝ ∧ ran ⁡ F ≠ ∅ ∧ ∃ y ∈ ℝ ∀ z ∈ ran ⁡ F z ≤ y → sup ran ⁡ F ℝ < ∈ ℝ
44 8 10 42 43 syl3anc ⊢ φ → sup ran ⁡ F ℝ < ∈ ℝ
45 5 44 eqeltrid ⊢ φ → C ∈ ℝ
46 8 adantr ⊢ φ ∧ x ∈ A → ran ⁡ F ⊆ ℝ
47 simpr ⊢ φ ∧ x ∈ A → x ∈ A
48 4 elrnmpt1 ⊢ x ∈ A ∧ B ∈ ℝ → B ∈ ran ⁡ F
49 47 2 48 syl2anc ⊢ φ ∧ x ∈ A → B ∈ ran ⁡ F
50 49 ne0d ⊢ φ ∧ x ∈ A → ran ⁡ F ≠ ∅
51 42 adantr ⊢ φ ∧ x ∈ A → ∃ y ∈ ℝ ∀ z ∈ ran ⁡ F z ≤ y
52 suprub ⊢ ran ⁡ F ⊆ ℝ ∧ ran ⁡ F ≠ ∅ ∧ ∃ y ∈ ℝ ∀ z ∈ ran ⁡ F z ≤ y ∧ B ∈ ran ⁡ F → B ≤ sup ran ⁡ F ℝ <
53 46 50 51 49 52 syl31anc ⊢ φ ∧ x ∈ A → B ≤ sup ran ⁡ F ℝ <
54 53 5 breqtrrdi ⊢ φ ∧ x ∈ A → B ≤ C
55 54 ralrimiva ⊢ φ → ∀ x ∈ A B ≤ C
56 45 55 jca ⊢ φ → C ∈ ℝ ∧ ∀ x ∈ A B ≤ C