Metamath Proof Explorer


Theorem o1mptrcl

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

Ref Expression
Hypotheses o1add2.1 ( ( 𝜑𝑥𝐴 ) → 𝐵𝑉 )
o1mptrcl.3 ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ 𝑂(1) )
Assertion o1mptrcl ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℂ )

Proof

Step Hyp Ref Expression
1 o1add2.1 ( ( 𝜑𝑥𝐴 ) → 𝐵𝑉 )
2 o1mptrcl.3 ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ 𝑂(1) )
3 o1f ( ( 𝑥𝐴𝐵 ) ∈ 𝑂(1) → ( 𝑥𝐴𝐵 ) : dom ( 𝑥𝐴𝐵 ) ⟶ ℂ )
4 2 3 syl ( 𝜑 → ( 𝑥𝐴𝐵 ) : dom ( 𝑥𝐴𝐵 ) ⟶ ℂ )
5 1 ralrimiva ( 𝜑 → ∀ 𝑥𝐴 𝐵𝑉 )
6 dmmptg ( ∀ 𝑥𝐴 𝐵𝑉 → dom ( 𝑥𝐴𝐵 ) = 𝐴 )
7 5 6 syl ( 𝜑 → dom ( 𝑥𝐴𝐵 ) = 𝐴 )
8 7 feq2d ( 𝜑 → ( ( 𝑥𝐴𝐵 ) : dom ( 𝑥𝐴𝐵 ) ⟶ ℂ ↔ ( 𝑥𝐴𝐵 ) : 𝐴 ⟶ ℂ ) )
9 4 8 mpbid ( 𝜑 → ( 𝑥𝐴𝐵 ) : 𝐴 ⟶ ℂ )
10 9 fvmptelrn ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℂ )