Metamath Proof Explorer

Theorem pimiooltgt

Description: The preimage of an open interval is the intersection of the preimage of an unbounded below open interval and an unbounded above open interval. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses pimiooltgt.1 
|- F/ x ph
pimiooltgt.2 
|- ( ph -> L e. RR* )
pimiooltgt.3 
|- ( ph -> R e. RR* )
pimiooltgt.4 
|- ( ( ph /\ x e. A ) -> B e. RR* )
Assertion pimiooltgt 
|- ( ph -> { x e. A | B e. ( L (,) R ) } = ( { x e. A | B < R } i^i { x e. A | L < B } ) )

Proof

Step Hyp Ref Expression
1 pimiooltgt.1 
 |-  F/ x ph
2 pimiooltgt.2 
 |-  ( ph -> L e. RR* )
3 pimiooltgt.3 
 |-  ( ph -> R e. RR* )
4 pimiooltgt.4 
 |-  ( ( ph /\ x e. A ) -> B e. RR* )
5 2 3ad2ant1 
 |-  ( ( ph /\ x e. A /\ B e. ( L (,) R ) ) -> L e. RR* )
6 3 3ad2ant1 
 |-  ( ( ph /\ x e. A /\ B e. ( L (,) R ) ) -> R e. RR* )
7 simp3 
 |-  ( ( ph /\ x e. A /\ B e. ( L (,) R ) ) -> B e. ( L (,) R ) )
8 5 6 7 iooltubd 
 |-  ( ( ph /\ x e. A /\ B e. ( L (,) R ) ) -> B < R )
9 8 3exp 
 |-  ( ph -> ( x e. A -> ( B e. ( L (,) R ) -> B < R ) ) )
10 1 9 ralrimi 
 |-  ( ph -> A. x e. A ( B e. ( L (,) R ) -> B < R ) )
11 10 ss2rabd 
 |-  ( ph -> { x e. A | B e. ( L (,) R ) } C_ { x e. A | B < R } )
12 5 6 7 ioogtlbd 
 |-  ( ( ph /\ x e. A /\ B e. ( L (,) R ) ) -> L < B )
13 12 3exp 
 |-  ( ph -> ( x e. A -> ( B e. ( L (,) R ) -> L < B ) ) )
14 1 13 ralrimi 
 |-  ( ph -> A. x e. A ( B e. ( L (,) R ) -> L < B ) )
15 14 ss2rabd 
 |-  ( ph -> { x e. A | B e. ( L (,) R ) } C_ { x e. A | L < B } )
16 11 15 ssind 
 |-  ( ph -> { x e. A | B e. ( L (,) R ) } C_ ( { x e. A | B < R } i^i { x e. A | L < B } ) )
17 nfrab1 
 |-  F/_ x { x e. A | B < R }
18 nfrab1 
 |-  F/_ x { x e. A | L < B }
19 17 18 nfin 
 |-  F/_ x ( { x e. A | B < R } i^i { x e. A | L < B } )
20 nfrab1 
 |-  F/_ x { x e. A | B e. ( L (,) R ) }
21 elinel1 
 |-  ( x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) -> x e. { x e. A | B < R } )
22 rabidim1 
 |-  ( x e. { x e. A | B < R } -> x e. A )
23 21 22 syl 
 |-  ( x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) -> x e. A )
24 23 adantl 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> x e. A )
25 2 adantr 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> L e. RR* )
26 3 adantr 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> R e. RR* )
27 23 4 sylan2 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> B e. RR* )
28 mnfxr 
 |-  -oo e. RR*
29 28 a1i 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> -oo e. RR* )
30 25 mnfled 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> -oo <_ L )
31 elinel2 
 |-  ( x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) -> x e. { x e. A | L < B } )
32 rabidim2 
 |-  ( x e. { x e. A | L < B } -> L < B )
33 31 32 syl 
 |-  ( x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) -> L < B )
34 33 adantl 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> L < B )
35 29 25 27 30 34 xrlelttrd 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> -oo < B )
36 29 27 35 xrgtned 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> B =/= -oo )
37 pnfxr 
 |-  +oo e. RR*
38 37 a1i 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> +oo e. RR* )
39 rabidim2 
 |-  ( x e. { x e. A | B < R } -> B < R )
40 21 39 syl 
 |-  ( x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) -> B < R )
41 40 adantl 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> B < R )
42 26 pnfged 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> R <_ +oo )
43 27 26 38 41 42 xrltletrd 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> B < +oo )
44 27 38 43 xrltned 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> B =/= +oo )
45 27 36 44 xrred 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> B e. RR )
46 25 26 45 34 41 eliood 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> B e. ( L (,) R ) )
47 24 46 rabidd 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> x e. { x e. A | B e. ( L (,) R ) } )
48 1 19 20 47 ssdf2 
 |-  ( ph -> ( { x e. A | B < R } i^i { x e. A | L < B } ) C_ { x e. A | B e. ( L (,) R ) } )
49 16 48 eqssd 
 |-  ( ph -> { x e. A | B e. ( L (,) R ) } = ( { x e. A | B < R } i^i { x e. A | L < B } ) )