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