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 9 2 4 1 rnmptn0 ⊢ ( 𝜑 → ran 𝐹 ≠ ∅ )
11 nfv ⊢ Ⅎ 𝑦 𝜑
12 nfre1 ⊢ Ⅎ 𝑦 ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦
13 simp2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) → 𝑦 ∈ ℝ )
14 simpl1 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) ∧ 𝑧 ∈ ran 𝐹 ) → 𝜑 )
15 simpl3 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) ∧ 𝑧 ∈ ran 𝐹 ) → ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 )
16 vex ⊢ 𝑧 ∈ V
17 4 elrnmpt ⊢ ( 𝑧 ∈ V → ( 𝑧 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) )
18 16 17 ax-mp ⊢ ( 𝑧 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 )
19 18 biimpi ⊢ ( 𝑧 ∈ ran 𝐹 → ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 )
20 19 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) ∧ 𝑧 ∈ ran 𝐹 ) → ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 )
21 simp3 ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 )
22 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦
23 nfre1 ⊢ Ⅎ 𝑥 ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵
24 9 22 23 nf3an ⊢ Ⅎ 𝑥 ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 )
25 nfv ⊢ Ⅎ 𝑥 𝑧 ≤ 𝑦
26 simp3 ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵 ) → 𝑧 = 𝐵 )
27 rspa ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ 𝑦 )
28 27 3adant3 ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵 ) → 𝐵 ≤ 𝑦 )
29 26 28 eqbrtrd ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵 ) → 𝑧 ≤ 𝑦 )
30 29 3exp ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 → ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝑧 ≤ 𝑦 ) ) )
31 30 3ad2ant2 ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) → ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝑧 ≤ 𝑦 ) ) )
32 24 25 31 rexlimd ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) → ( ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑧 ≤ 𝑦 ) )
33 21 32 mpd ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) → 𝑧 ≤ 𝑦 )
34 14 15 20 33 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) ∧ 𝑧 ∈ ran 𝐹 ) → 𝑧 ≤ 𝑦 )
35 34 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) → ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦 )
36 19.8a ⊢ ( ( 𝑦 ∈ ℝ ∧ ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦 ) → ∃ 𝑦 ( 𝑦 ∈ ℝ ∧ ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦 ) )
37 13 35 36 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) → ∃ 𝑦 ( 𝑦 ∈ ℝ ∧ ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦 ) )
38 df-rex ⊢ ( ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦 ↔ ∃ 𝑦 ( 𝑦 ∈ ℝ ∧ ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦 ) )
39 37 38 sylibr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦 )
40 39 3exp ⊢ ( 𝜑 → ( 𝑦 ∈ ℝ → ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦 ) ) )
41 11 12 40 rexlimd ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦 ) )
42 3 41 mpd ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦 )
43 suprcl ⊢ ( ( ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦 ) → sup ( ran 𝐹 , ℝ , < ) ∈ ℝ )
44 8 10 42 43 syl3anc ⊢ ( 𝜑 → sup ( ran 𝐹 , ℝ , < ) ∈ ℝ )
45 5 44 eqeltrid ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
46 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ran 𝐹 ⊆ ℝ )
47 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
48 4 elrnmpt1 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ran 𝐹 )
49 47 2 48 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ran 𝐹 )
50 49 ne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ran 𝐹 ≠ ∅ )
51 42 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦 )
52 suprub ⊢ ( ( ( ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦 ) ∧ 𝐵 ∈ ran 𝐹 ) → 𝐵 ≤ sup ( ran 𝐹 , ℝ , < ) )
53 46 50 51 49 52 syl31anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ sup ( ran 𝐹 , ℝ , < ) )
54 53 5 breqtrrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ 𝐶 )
55 54 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 )
56 45 55 jca ⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 ) )