Metamath Proof Explorer

Theorem rnmptbd2lem

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

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

Proof

Step Hyp Ref Expression
1 rnmptbd2lem.x ⊢ Ⅎ x φ
2 rnmptbd2lem.b ⊢ φ ∧ x ∈ A → B ∈ V
3 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
4 3 elrnmpt ⊢ z ∈ V → z ∈ ran ⁡ x ∈ A ⟼ B ↔ ∃ x ∈ A z = B
5 4 elv ⊢ z ∈ ran ⁡ x ∈ A ⟼ B ↔ ∃ x ∈ A z = B
6 nfra1 ⊢ Ⅎ x ∀ x ∈ A y ≤ B
7 nfv ⊢ Ⅎ x y ≤ z
8 rspa ⊢ ∀ x ∈ A y ≤ B ∧ x ∈ A → y ≤ B
9 simpl ⊢ y ≤ B ∧ z = B → y ≤ B
10 id ⊢ z = B → z = B
11 10 eqcomd ⊢ z = B → B = z
12 11 adantl ⊢ y ≤ B ∧ z = B → B = z
13 9 12 breqtrd ⊢ y ≤ B ∧ z = B → y ≤ z
14 13 ex ⊢ y ≤ B → z = B → y ≤ z
15 8 14 syl ⊢ ∀ x ∈ A y ≤ B ∧ x ∈ A → z = B → y ≤ z
16 15 ex ⊢ ∀ x ∈ A y ≤ B → x ∈ A → z = B → y ≤ z
17 6 7 16 rexlimd ⊢ ∀ x ∈ A y ≤ B → ∃ x ∈ A z = B → y ≤ z
18 17 imp ⊢ ∀ x ∈ A y ≤ B ∧ ∃ x ∈ A z = B → y ≤ z
19 18 adantll ⊢ φ ∧ ∀ x ∈ A y ≤ B ∧ ∃ x ∈ A z = B → y ≤ z
20 5 19 sylan2b ⊢ φ ∧ ∀ x ∈ A y ≤ B ∧ z ∈ ran ⁡ x ∈ A ⟼ B → y ≤ z
21 20 ralrimiva ⊢ φ ∧ ∀ x ∈ A y ≤ B → ∀ z ∈ ran ⁡ x ∈ A ⟼ B y ≤ z
22 21 ex ⊢ φ → ∀ x ∈ A y ≤ B → ∀ z ∈ ran ⁡ x ∈ A ⟼ B y ≤ z
23 22 reximdv ⊢ φ → ∃ y ∈ ℝ ∀ x ∈ A y ≤ B → ∃ y ∈ ℝ ∀ z ∈ ran ⁡ x ∈ A ⟼ B y ≤ z
24 nfmpt1 ⊢ Ⅎ _ x x ∈ A ⟼ B
25 24 nfrn ⊢ Ⅎ _ x ran ⁡ x ∈ A ⟼ B
26 25 7 nfralw ⊢ Ⅎ x ∀ z ∈ ran ⁡ x ∈ A ⟼ B y ≤ z
27 1 26 nfan ⊢ Ⅎ x φ ∧ ∀ z ∈ ran ⁡ x ∈ A ⟼ B y ≤ z
28 breq2 ⊢ z = B → y ≤ z ↔ y ≤ B
29 simplr ⊢ φ ∧ ∀ z ∈ ran ⁡ x ∈ A ⟼ B y ≤ z ∧ x ∈ A → ∀ z ∈ ran ⁡ x ∈ A ⟼ B y ≤ z
30 simpr ⊢ φ ∧ ∀ z ∈ ran ⁡ x ∈ A ⟼ B y ≤ z ∧ x ∈ A → x ∈ A
31 2 adantlr ⊢ φ ∧ ∀ z ∈ ran ⁡ x ∈ A ⟼ B y ≤ z ∧ x ∈ A → B ∈ V
32 3 30 31 elrnmpt1d ⊢ φ ∧ ∀ z ∈ ran ⁡ x ∈ A ⟼ B y ≤ z ∧ x ∈ A → B ∈ ran ⁡ x ∈ A ⟼ B
33 28 29 32 rspcdva ⊢ φ ∧ ∀ z ∈ ran ⁡ x ∈ A ⟼ B y ≤ z ∧ x ∈ A → y ≤ B
34 27 33 ralrimia ⊢ φ ∧ ∀ z ∈ ran ⁡ x ∈ A ⟼ B y ≤ z → ∀ x ∈ A y ≤ B
35 34 ex ⊢ φ → ∀ z ∈ ran ⁡ x ∈ A ⟼ B y ≤ z → ∀ x ∈ A y ≤ B
36 35 reximdv ⊢ φ → ∃ y ∈ ℝ ∀ z ∈ ran ⁡ x ∈ A ⟼ B y ≤ z → ∃ y ∈ ℝ ∀ x ∈ A y ≤ B
37 23 36 impbid ⊢ φ → ∃ y ∈ ℝ ∀ x ∈ A y ≤ B ↔ ∃ y ∈ ℝ ∀ z ∈ ran ⁡ x ∈ A ⟼ B y ≤ z