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 ⊢ Ⅎ x φ
suprleubrnmpt.a ⊢ φ → A ≠ ∅
suprleubrnmpt.b ⊢ φ ∧ x ∈ A → B ∈ ℝ
suprleubrnmpt.e ⊢ φ → ∃ y ∈ ℝ ∀ x ∈ A B ≤ y
suprleubrnmpt.c ⊢ φ → C ∈ ℝ
Assertion suprleubrnmpt ⊢ φ → sup ran ⁡ x ∈ A ⟼ B ℝ < ≤ C ↔ ∀ x ∈ A B ≤ C

Proof

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