Metamath Proof Explorer

Theorem preimaioomnf

Description: Preimage of an open interval, unbounded below. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses preimaioomnf.1 
|- ( ph -> F : A --> RR )
preimaioomnf.2 
|- ( ph -> B e. RR* )
Assertion preimaioomnf 
|- ( ph -> ( `' F " ( -oo (,) B ) ) = { x e. A | ( F ` x ) < B } )

Proof

Step Hyp Ref Expression
1 preimaioomnf.1 
 |-  ( ph -> F : A --> RR )
2 preimaioomnf.2 
 |-  ( ph -> B e. RR* )
3 1 ffund 
 |-  ( ph -> Fun F )
4 1 frnd 
 |-  ( ph -> ran F C_ RR )
5 fimacnvinrn2 
 |-  ( ( Fun F /\ ran F C_ RR ) -> ( `' F " ( -oo [,) B ) ) = ( `' F " ( ( -oo [,) B ) i^i RR ) ) )
6 3 4 5 syl2anc 
 |-  ( ph -> ( `' F " ( -oo [,) B ) ) = ( `' F " ( ( -oo [,) B ) i^i RR ) ) )
7 2 icomnfinre 
 |-  ( ph -> ( ( -oo [,) B ) i^i RR ) = ( -oo (,) B ) )
8 7 imaeq2d 
 |-  ( ph -> ( `' F " ( ( -oo [,) B ) i^i RR ) ) = ( `' F " ( -oo (,) B ) ) )
9 6 8 eqtr2d 
 |-  ( ph -> ( `' F " ( -oo (,) B ) ) = ( `' F " ( -oo [,) B ) ) )
10 1 frexr 
 |-  ( ph -> F : A --> RR* )
11 10 2 preimaicomnf 
 |-  ( ph -> ( `' F " ( -oo [,) B ) ) = { x e. A | ( F ` x ) < B } )
12 9 11 eqtrd 
 |-  ( ph -> ( `' F " ( -oo (,) B ) ) = { x e. A | ( F ` x ) < B } )