Metamath Proof Explorer

Theorem supxrleubrnmpt

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

Ref Expression
Hypotheses supxrleubrnmpt.x ⊢ Ⅎ x φ
supxrleubrnmpt.b ⊢ φ ∧ x ∈ A → B ∈ ℝ *
supxrleubrnmpt.c ⊢ φ → C ∈ ℝ *
Assertion supxrleubrnmpt ⊢ φ → sup ran ⁡ x ∈ A ⟼ B ℝ * < ≤ C ↔ ∀ x ∈ A B ≤ C

Proof

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