Metamath Proof Explorer

Theorem suprleubrnmpt

Description: The supremum of a nonempty bounded indexed set of reals is less than or equal to an upper bound. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses suprleubrnmpt.x ⊢ Ⅎ 𝑥 𝜑
suprleubrnmpt.a ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
suprleubrnmpt.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
suprleubrnmpt.e ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 )
suprleubrnmpt.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
Assertion suprleubrnmpt ( 𝜑 → ( sup ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ , < ) ≤ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 suprleubrnmpt.x ⊢ Ⅎ 𝑥 𝜑
2 suprleubrnmpt.a ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
3 suprleubrnmpt.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
4 suprleubrnmpt.e ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 )
5 suprleubrnmpt.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
6 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
7 1 6 3 rnmptssd ⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ )
8 1 3 6 2 rnmptn0 ⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≠ ∅ )
9 1 4 rnmptbdd ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑤 ≤ 𝑦 )
10 suprleub ⊢ ( ( ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ ∧ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑤 ≤ 𝑦 ) ∧ 𝐶 ∈ ℝ ) → ( sup ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ , < ) ≤ 𝐶 ↔ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝐶 ) )
11 7 8 9 5 10 syl31anc ⊢ ( 𝜑 → ( sup ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ , < ) ≤ 𝐶 ↔ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝐶 ) )
12 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
13 12 nfrn ⊢ Ⅎ 𝑥 ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
14 nfv ⊢ Ⅎ 𝑥 𝑧 ≤ 𝐶
15 13 14 nfralw ⊢ Ⅎ 𝑥 ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝐶
16 1 15 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝐶 )
17 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
18 6 elrnmpt1 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
19 17 3 18 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
20 19 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
21 simplr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝐶 )
22 breq1 ⊢ ( 𝑧 = 𝐵 → ( 𝑧 ≤ 𝐶 ↔ 𝐵 ≤ 𝐶 ) )
23 22 rspcva ⊢ ( ( 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝐶 ) → 𝐵 ≤ 𝐶 )
24 20 21 23 syl2anc ⊢ ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ 𝐶 )
25 24 ex ⊢ ( ( 𝜑 ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝐶 ) → ( 𝑥 ∈ 𝐴 → 𝐵 ≤ 𝐶 ) )
26 16 25 ralrimi ⊢ ( ( 𝜑 ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝐶 ) → ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 )
27 26 ex ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝐶 → ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 ) )
28 vex ⊢ 𝑧 ∈ V
29 6 elrnmpt ⊢ ( 𝑧 ∈ V → ( 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) )
30 28 29 ax-mp ⊢ ( 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 )
31 30 biimpi ⊢ ( 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 )
32 31 adantl ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 ∧ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 )
33 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶
34 rspa ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ 𝐶 )
35 22 biimprcd ⊢ ( 𝐵 ≤ 𝐶 → ( 𝑧 = 𝐵 → 𝑧 ≤ 𝐶 ) )
36 34 35 syl ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑧 = 𝐵 → 𝑧 ≤ 𝐶 ) )
37 36 ex ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 → ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝑧 ≤ 𝐶 ) ) )
38 33 14 37 rexlimd ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 → ( ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑧 ≤ 𝐶 ) )
39 38 adantr ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 ∧ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → ( ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑧 ≤ 𝐶 ) )
40 32 39 mpd ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 ∧ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → 𝑧 ≤ 𝐶 )
41 40 ralrimiva ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 → ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝐶 )
42 41 a1i ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 → ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝐶 ) )
43 27 42 impbid ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 ) )
44 11 43 bitrd ⊢ ( 𝜑 → ( sup ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ , < ) ≤ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 ) )