Metamath Proof Explorer

Theorem rnmptbdlem

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

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

Proof

Step Hyp Ref Expression
1 rnmptbdlem.x ⊢ Ⅎ x φ
2 rnmptbdlem.y ⊢ Ⅎ y φ
3 rnmptbdlem.b ⊢ φ ∧ x ∈ A → B ∈ V
4 nfcv ⊢ Ⅎ _ x ℝ
5 nfra1 ⊢ Ⅎ x ∀ x ∈ A B ≤ y
6 4 5 nfrexw ⊢ Ⅎ x ∃ y ∈ ℝ ∀ x ∈ A B ≤ y
7 1 6 nfan ⊢ Ⅎ x φ ∧ ∃ y ∈ ℝ ∀ x ∈ A B ≤ y
8 simpr ⊢ φ ∧ ∃ y ∈ ℝ ∀ x ∈ A B ≤ y → ∃ y ∈ ℝ ∀ x ∈ A B ≤ y
9 7 8 rnmptbdd ⊢ φ ∧ ∃ y ∈ ℝ ∀ x ∈ A B ≤ y → ∃ y ∈ ℝ ∀ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y
10 9 ex ⊢ φ → ∃ y ∈ ℝ ∀ x ∈ A B ≤ y → ∃ y ∈ ℝ ∀ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y
11 nfmpt1 ⊢ Ⅎ _ x x ∈ A ⟼ B
12 11 nfrn ⊢ Ⅎ _ x ran ⁡ x ∈ A ⟼ B
13 nfv ⊢ Ⅎ x z ≤ y
14 12 13 nfralw ⊢ Ⅎ x ∀ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y
15 1 14 nfan ⊢ Ⅎ x φ ∧ ∀ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y
16 breq1 ⊢ z = B → z ≤ y ↔ B ≤ y
17 simplr ⊢ φ ∧ ∀ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y ∧ x ∈ A → ∀ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y
18 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
19 simpr ⊢ φ ∧ ∀ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y ∧ x ∈ A → x ∈ A
20 3 adantlr ⊢ φ ∧ ∀ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y ∧ x ∈ A → B ∈ V
21 18 19 20 elrnmpt1d ⊢ φ ∧ ∀ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y ∧ x ∈ A → B ∈ ran ⁡ x ∈ A ⟼ B
22 16 17 21 rspcdva ⊢ φ ∧ ∀ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y ∧ x ∈ A → B ≤ y
23 15 22 ralrimia ⊢ φ ∧ ∀ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y → ∀ x ∈ A B ≤ y
24 23 ex ⊢ φ → ∀ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y → ∀ x ∈ A B ≤ y
25 24 a1d ⊢ φ → y ∈ ℝ → ∀ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y → ∀ x ∈ A B ≤ y
26 2 25 reximdai ⊢ φ → ∃ y ∈ ℝ ∀ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y → ∃ y ∈ ℝ ∀ x ∈ A B ≤ y
27 10 26 impbid ⊢ φ → ∃ y ∈ ℝ ∀ x ∈ A B ≤ y ↔ ∃ y ∈ ℝ ∀ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y