Metamath Proof Explorer

Theorem preimaicomnf

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

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

Proof

Step Hyp Ref Expression
1 preimaicomnf.1 
 |-  ( ph -> F : A --> RR* )
2 preimaicomnf.2 
 |-  ( ph -> B e. RR* )
3 1 ffnd 
 |-  ( ph -> F Fn A )
4 fncnvima2 
 |-  ( F Fn A -> ( `' F " ( -oo [,) B ) ) = { x e. A | ( F ` x ) e. ( -oo [,) B ) } )
5 3 4 syl 
 |-  ( ph -> ( `' F " ( -oo [,) B ) ) = { x e. A | ( F ` x ) e. ( -oo [,) B ) } )
6 mnfxr 
 |-  -oo e. RR*
7 6 a1i 
 |-  ( ( ( ph /\ x e. A ) /\ ( F ` x ) e. ( -oo [,) B ) ) -> -oo e. RR* )
8 2 ad2antrr 
 |-  ( ( ( ph /\ x e. A ) /\ ( F ` x ) e. ( -oo [,) B ) ) -> B e. RR* )
9 simpr 
 |-  ( ( ( ph /\ x e. A ) /\ ( F ` x ) e. ( -oo [,) B ) ) -> ( F ` x ) e. ( -oo [,) B ) )
10 icoltub 
 |-  ( ( -oo e. RR* /\ B e. RR* /\ ( F ` x ) e. ( -oo [,) B ) ) -> ( F ` x ) < B )
11 7 8 9 10 syl3anc 
 |-  ( ( ( ph /\ x e. A ) /\ ( F ` x ) e. ( -oo [,) B ) ) -> ( F ` x ) < B )
12 11 ex 
 |-  ( ( ph /\ x e. A ) -> ( ( F ` x ) e. ( -oo [,) B ) -> ( F ` x ) < B ) )
13 6 a1i 
 |-  ( ( ( ph /\ x e. A ) /\ ( F ` x ) < B ) -> -oo e. RR* )
14 2 ad2antrr 
 |-  ( ( ( ph /\ x e. A ) /\ ( F ` x ) < B ) -> B e. RR* )
15 1 ffvelrnda 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) e. RR* )
16 15 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ ( F ` x ) < B ) -> ( F ` x ) e. RR* )
17 15 mnfled 
 |-  ( ( ph /\ x e. A ) -> -oo <_ ( F ` x ) )
18 17 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ ( F ` x ) < B ) -> -oo <_ ( F ` x ) )
19 simpr 
 |-  ( ( ( ph /\ x e. A ) /\ ( F ` x ) < B ) -> ( F ` x ) < B )
20 13 14 16 18 19 elicod 
 |-  ( ( ( ph /\ x e. A ) /\ ( F ` x ) < B ) -> ( F ` x ) e. ( -oo [,) B ) )
21 20 ex 
 |-  ( ( ph /\ x e. A ) -> ( ( F ` x ) < B -> ( F ` x ) e. ( -oo [,) B ) ) )
22 12 21 impbid 
 |-  ( ( ph /\ x e. A ) -> ( ( F ` x ) e. ( -oo [,) B ) <-> ( F ` x ) < B ) )
23 22 rabbidva 
 |-  ( ph -> { x e. A | ( F ` x ) e. ( -oo [,) B ) } = { x e. A | ( F ` x ) < B } )
24 5 23 eqtrd 
 |-  ( ph -> ( `' F " ( -oo [,) B ) ) = { x e. A | ( F ` x ) < B } )