Metamath Proof Explorer

Theorem preimaiocmnf

Description: Preimage of a right-closed interval, unbounded below. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step Hyp Ref Expression
1 preimaiocmnf.1 
 |-  ( ph -> F : A --> RR )
2 preimaiocmnf.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 /\ ( F ` x ) e. ( -oo (,] B ) ) -> -oo e. RR* )
8 2 adantr 
 |-  ( ( ph /\ ( F ` x ) e. ( -oo (,] B ) ) -> B e. RR* )
9 simpr 
 |-  ( ( ph /\ ( F ` x ) e. ( -oo (,] B ) ) -> ( F ` x ) e. ( -oo (,] B ) )
10 7 8 9 iocleubd 
 |-  ( ( ph /\ ( F ` x ) e. ( -oo (,] B ) ) -> ( F ` x ) <_ B )
11 10 ex 
 |-  ( ph -> ( ( F ` x ) e. ( -oo (,] B ) -> ( F ` x ) <_ B ) )
12 11 adantr 
 |-  ( ( 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 adantr 
 |-  ( ( ph /\ ( F ` x ) <_ B ) -> B e. RR* )
15 14 adantlr 
 |-  ( ( ( ph /\ x e. A ) /\ ( F ` x ) <_ B ) -> B e. RR* )
16 1 ffvelrnda 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) e. RR )
17 16 rexrd 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) e. RR* )
18 17 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ ( F ` x ) <_ B ) -> ( F ` x ) e. RR* )
19 16 mnfltd 
 |-  ( ( ph /\ x e. A ) -> -oo < ( F ` x ) )
20 19 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ ( F ` x ) <_ B ) -> -oo < ( F ` x ) )
21 simpr 
 |-  ( ( ( ph /\ x e. A ) /\ ( F ` x ) <_ B ) -> ( F ` x ) <_ B )
22 13 15 18 20 21 eliocd 
 |-  ( ( ( ph /\ x e. A ) /\ ( F ` x ) <_ B ) -> ( F ` x ) e. ( -oo (,] B ) )
23 22 ex 
 |-  ( ( ph /\ x e. A ) -> ( ( F ` x ) <_ B -> ( F ` x ) e. ( -oo (,] B ) ) )
24 12 23 impbid 
 |-  ( ( ph /\ x e. A ) -> ( ( F ` x ) e. ( -oo (,] B ) <-> ( F ` x ) <_ B ) )
25 24 rabbidva 
 |-  ( ph -> { x e. A | ( F ` x ) e. ( -oo (,] B ) } = { x e. A | ( F ` x ) <_ B } )
26 5 25 eqtrd 
 |-  ( ph -> ( `' F " ( -oo (,] B ) ) = { x e. A | ( F ` x ) <_ B } )