Metamath Proof Explorer

Theorem rnmptbd2

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

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

Proof

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