Metamath Proof Explorer

Theorem rnmptbd

Description: Boundness above of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses rnmptbd.x ⊢ Ⅎ x φ
rnmptbd.b ⊢ φ ∧ x ∈ A → B ∈ V
Assertion rnmptbd ⊢ φ → ∃ y ∈ ℝ ∀ x ∈ A B ≤ y ↔ ∃ y ∈ ℝ ∀ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y

Proof

Step Hyp Ref Expression
1 rnmptbd.x ⊢ Ⅎ x φ
2 rnmptbd.b ⊢ φ ∧ x ∈ A → B ∈ V
3 breq2 ⊢ y = w → B ≤ y ↔ B ≤ w
4 3 ralbidv ⊢ y = w → ∀ x ∈ A B ≤ y ↔ ∀ x ∈ A B ≤ w
5 4 cbvrexvw ⊢ ∃ y ∈ ℝ ∀ x ∈ A B ≤ y ↔ ∃ w ∈ ℝ ∀ x ∈ A B ≤ w
6 5 a1i ⊢ φ → ∃ y ∈ ℝ ∀ x ∈ A B ≤ y ↔ ∃ w ∈ ℝ ∀ x ∈ A B ≤ w
7 nfv ⊢ Ⅎ w φ
8 1 7 2 rnmptbdlem ⊢ φ → ∃ w ∈ ℝ ∀ x ∈ A B ≤ w ↔ ∃ w ∈ ℝ ∀ u ∈ ran ⁡ x ∈ A ⟼ B u ≤ w
9 breq2 ⊢ w = y → u ≤ w ↔ u ≤ y
10 9 ralbidv ⊢ w = y → ∀ u ∈ ran ⁡ x ∈ A ⟼ B u ≤ w ↔ ∀ u ∈ ran ⁡ x ∈ A ⟼ B u ≤ y
11 breq1 ⊢ u = z → u ≤ y ↔ z ≤ y
12 11 cbvralvw ⊢ ∀ u ∈ ran ⁡ x ∈ A ⟼ B u ≤ y ↔ ∀ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y
13 10 12 bitrdi ⊢ w = y → ∀ u ∈ ran ⁡ x ∈ A ⟼ B u ≤ w ↔ ∀ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y
14 13 cbvrexvw ⊢ ∃ w ∈ ℝ ∀ u ∈ ran ⁡ x ∈ A ⟼ B u ≤ w ↔ ∃ y ∈ ℝ ∀ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y
15 14 a1i ⊢ φ → ∃ w ∈ ℝ ∀ u ∈ ran ⁡ x ∈ A ⟼ B u ≤ w ↔ ∃ y ∈ ℝ ∀ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y
16 6 8 15 3bitrd ⊢ φ → ∃ y ∈ ℝ ∀ x ∈ A B ≤ y ↔ ∃ y ∈ ℝ ∀ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y