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∈AB≤y↔∃y∈ℝ∀z∈ran⁡x∈A⟼Bz≤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∈AB≤y
6 4 5 nfrexw ⊢Ⅎx∃y∈ℝ∀x∈AB≤y
7 1 6 nfan ⊢Ⅎxφ∧∃y∈ℝ∀x∈AB≤y
8 simpr ⊢φ∧∃y∈ℝ∀x∈AB≤y→∃y∈ℝ∀x∈AB≤y
9 7 8 rnmptbdd ⊢φ∧∃y∈ℝ∀x∈AB≤y→∃y∈ℝ∀z∈ran⁡x∈A⟼Bz≤y
10 9 ex ⊢φ→∃y∈ℝ∀x∈AB≤y→∃y∈ℝ∀z∈ran⁡x∈A⟼Bz≤y
11 nfmpt1 ⊢Ⅎ_xx∈A⟼B
12 11 nfrn ⊢Ⅎ_xran⁡x∈A⟼B
13 nfv ⊢Ⅎxz≤y
14 12 13 nfralw ⊢Ⅎx∀z∈ran⁡x∈A⟼Bz≤y
15 1 14 nfan ⊢Ⅎxφ∧∀z∈ran⁡x∈A⟼Bz≤y
16 breq1 ⊢z=B→z≤y↔B≤y
17 simplr ⊢φ∧∀z∈ran⁡x∈A⟼Bz≤y∧x∈A→∀z∈ran⁡x∈A⟼Bz≤y
18 eqid ⊢x∈A⟼B=x∈A⟼B
19 simpr ⊢φ∧∀z∈ran⁡x∈A⟼Bz≤y∧x∈A→x∈A
20 3 adantlr ⊢φ∧∀z∈ran⁡x∈A⟼Bz≤y∧x∈A→B∈V
21 18 19 20 elrnmpt1d ⊢φ∧∀z∈ran⁡x∈A⟼Bz≤y∧x∈A→B∈ran⁡x∈A⟼B
22 16 17 21 rspcdva ⊢φ∧∀z∈ran⁡x∈A⟼Bz≤y∧x∈A→B≤y
23 15 22 ralrimia ⊢φ∧∀z∈ran⁡x∈A⟼Bz≤y→∀x∈AB≤y
24 23 ex ⊢φ→∀z∈ran⁡x∈A⟼Bz≤y→∀x∈AB≤y
25 24 a1d ⊢φ→y∈ℝ→∀z∈ran⁡x∈A⟼Bz≤y→∀x∈AB≤y
26 2 25 reximdai ⊢φ→∃y∈ℝ∀z∈ran⁡x∈A⟼Bz≤y→∃y∈ℝ∀x∈AB≤y
27 10 26 impbid ⊢φ→∃y∈ℝ∀x∈AB≤y↔∃y∈ℝ∀z∈ran⁡x∈A⟼Bz≤y