This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lo1mptrcl

Description: Reverse closure for an eventually upper bounded function. (Contributed by Mario Carneiro, 26-May-2016)

Ref Expression
Hypotheses o1add2.1 ⊢ φ ∧ x ∈ A → B ∈ V
lo1mptrcl.3 ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1
Assertion lo1mptrcl ⊢ φ ∧ x ∈ A → B ∈ ℝ

Proof

Step Hyp Ref Expression
1 o1add2.1 ⊢ φ ∧ x ∈ A → B ∈ V
2 lo1mptrcl.3 ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1
3 lo1f ⊢ x ∈ A ⟼ B ∈ ≤𝑂⁡1 → x ∈ A ⟼ B : dom ⁡ x ∈ A ⟼ B ⟶ ℝ
4 2 3 syl ⊢ φ → x ∈ A ⟼ B : dom ⁡ x ∈ A ⟼ B ⟶ ℝ
5 1 ralrimiva ⊢ φ → ∀ x ∈ A B ∈ V
6 dmmptg ⊢ ∀ x ∈ A B ∈ V → dom ⁡ x ∈ A ⟼ B = A
7 5 6 syl ⊢ φ → dom ⁡ x ∈ A ⟼ B = A
8 7 feq2d ⊢ φ → x ∈ A ⟼ B : dom ⁡ x ∈ A ⟼ B ⟶ ℝ ↔ x ∈ A ⟼ B : A ⟶ ℝ
9 4 8 mpbid ⊢ φ → x ∈ A ⟼ B : A ⟶ ℝ
10 9 fvmptelcdm ⊢ φ ∧ x ∈ A → B ∈ ℝ