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 ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
suprnmpt.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
suprnmpt.bnd ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 )
suprnmpt.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
suprnmpt.c ⊢ 𝐶 = sup ( ran 𝐹 , ℝ , < )
Assertion suprnmpt ( 𝜑 → ( 𝐶 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 suprnmpt.a ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
2 suprnmpt.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
3 suprnmpt.bnd ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 )
4 suprnmpt.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
5 suprnmpt.c ⊢ 𝐶 = sup ( ran 𝐹 , ℝ , < )
6 2 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ℝ )
7 4 rnmptss ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ℝ → ran 𝐹 ⊆ ℝ )
8 6 7 syl ⊢ ( 𝜑 → ran 𝐹 ⊆ ℝ )
9 nfv ⊢ Ⅎ 𝑥 𝜑
10 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
11 4 10 nfcxfr ⊢ Ⅎ 𝑥 𝐹
12 11 nfrn ⊢ Ⅎ 𝑥 ran 𝐹
13 nfcv ⊢ Ⅎ 𝑥 ∅
14 12 13 nfne ⊢ Ⅎ 𝑥 ran 𝐹 ≠ ∅
15 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
16 1 15 sylib ⊢ ( 𝜑 → ∃ 𝑥 𝑥 ∈ 𝐴 )
17 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
18 4 elrnmpt1 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ran 𝐹 )
19 17 2 18 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ran 𝐹 )
20 19 ne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ran 𝐹 ≠ ∅ )
21 9 14 16 20 exlimdd ⊢ ( 𝜑 → ran 𝐹 ≠ ∅ )
22 nfv ⊢ Ⅎ 𝑦 𝜑
23 nfre1 ⊢ Ⅎ 𝑦 ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦
24 simp2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) → 𝑦 ∈ ℝ )
25 simpl1 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) ∧ 𝑧 ∈ ran 𝐹 ) → 𝜑 )
26 simpl3 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) ∧ 𝑧 ∈ ran 𝐹 ) → ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 )
27 vex ⊢ 𝑧 ∈ V
28 4 elrnmpt ⊢ ( 𝑧 ∈ V → ( 𝑧 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) )
29 27 28 ax-mp ⊢ ( 𝑧 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 )
30 29 biimpi ⊢ ( 𝑧 ∈ ran 𝐹 → ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 )
31 30 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) ∧ 𝑧 ∈ ran 𝐹 ) → ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 )
32 simp3 ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 )
33 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦
34 nfre1 ⊢ Ⅎ 𝑥 ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵
35 9 33 34 nf3an ⊢ Ⅎ 𝑥 ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 )
36 nfv ⊢ Ⅎ 𝑥 𝑧 ≤ 𝑦
37 simp3 ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵 ) → 𝑧 = 𝐵 )
38 rspa ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ 𝑦 )
39 38 3adant3 ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵 ) → 𝐵 ≤ 𝑦 )
40 37 39 eqbrtrd ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵 ) → 𝑧 ≤ 𝑦 )
41 40 3exp ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 → ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝑧 ≤ 𝑦 ) ) )
42 41 3ad2ant2 ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) → ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝑧 ≤ 𝑦 ) ) )
43 35 36 42 rexlimd ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) → ( ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑧 ≤ 𝑦 ) )
44 32 43 mpd ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) → 𝑧 ≤ 𝑦 )
45 25 26 31 44 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) ∧ 𝑧 ∈ ran 𝐹 ) → 𝑧 ≤ 𝑦 )
46 45 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) → ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦 )
47 19.8a ⊢ ( ( 𝑦 ∈ ℝ ∧ ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦 ) → ∃ 𝑦 ( 𝑦 ∈ ℝ ∧ ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦 ) )
48 24 46 47 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) → ∃ 𝑦 ( 𝑦 ∈ ℝ ∧ ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦 ) )
49 df-rex ⊢ ( ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦 ↔ ∃ 𝑦 ( 𝑦 ∈ ℝ ∧ ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦 ) )
50 48 49 sylibr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦 )
51 50 3exp ⊢ ( 𝜑 → ( 𝑦 ∈ ℝ → ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦 ) ) )
52 22 23 51 rexlimd ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦 ) )
53 3 52 mpd ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦 )
54 suprcl ⊢ ( ( ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦 ) → sup ( ran 𝐹 , ℝ , < ) ∈ ℝ )
55 8 21 53 54 syl3anc ⊢ ( 𝜑 → sup ( ran 𝐹 , ℝ , < ) ∈ ℝ )
56 5 55 eqeltrid ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
57 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ran 𝐹 ⊆ ℝ )
58 53 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦 )
59 suprub ⊢ ( ( ( ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦 ) ∧ 𝐵 ∈ ran 𝐹 ) → 𝐵 ≤ sup ( ran 𝐹 , ℝ , < ) )
60 57 20 58 19 59 syl31anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ sup ( ran 𝐹 , ℝ , < ) )
61 60 5 breqtrrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ 𝐶 )
62 61 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 )
63 56 62 jca ⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 ) )