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 adantr 
 |-  ( ( ph /\ x e. A ) -> L e. RR* )
6 5 3adant3 
 |-  ( ( ph /\ x e. A /\ B e. ( L (,) R ) ) -> L e. RR* )
7 3 adantr 
 |-  ( ( ph /\ x e. A ) -> R e. RR* )
8 7 3adant3 
 |-  ( ( ph /\ x e. A /\ B e. ( L (,) R ) ) -> R e. RR* )
9 simp3 
 |-  ( ( ph /\ x e. A /\ B e. ( L (,) R ) ) -> B e. ( L (,) R ) )
10 iooltub 
 |-  ( ( L e. RR* /\ R e. RR* /\ B e. ( L (,) R ) ) -> B < R )
11 6 8 9 10 syl3anc 
 |-  ( ( ph /\ x e. A /\ B e. ( L (,) R ) ) -> B < R )
12 11 3exp 
 |-  ( ph -> ( x e. A -> ( B e. ( L (,) R ) -> B < R ) ) )
13 1 12 ralrimi 
 |-  ( ph -> A. x e. A ( B e. ( L (,) R ) -> B < R ) )
14 ss2rab 
 |-  ( { x e. A | B e. ( L (,) R ) } C_ { x e. A | B < R } <-> A. x e. A ( B e. ( L (,) R ) -> B < R ) )
15 13 14 sylibr 
 |-  ( ph -> { x e. A | B e. ( L (,) R ) } C_ { x e. A | B < R } )
16 ioogtlb 
 |-  ( ( L e. RR* /\ R e. RR* /\ B e. ( L (,) R ) ) -> L < B )
17 6 8 9 16 syl3anc 
 |-  ( ( ph /\ x e. A /\ B e. ( L (,) R ) ) -> L < B )
18 17 3exp 
 |-  ( ph -> ( x e. A -> ( B e. ( L (,) R ) -> L < B ) ) )
19 1 18 ralrimi 
 |-  ( ph -> A. x e. A ( B e. ( L (,) R ) -> L < B ) )
20 ss2rab 
 |-  ( { x e. A | B e. ( L (,) R ) } C_ { x e. A | L < B } <-> A. x e. A ( B e. ( L (,) R ) -> L < B ) )
21 19 20 sylibr 
 |-  ( ph -> { x e. A | B e. ( L (,) R ) } C_ { x e. A | L < B } )
22 15 21 ssind 
 |-  ( ph -> { x e. A | B e. ( L (,) R ) } C_ ( { x e. A | B < R } i^i { x e. A | L < B } ) )
23 elinel1 
 |-  ( x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) -> x e. { x e. A | B < R } )
24 ssrab2 
 |-  { x e. A | B < R } C_ A
25 24 sseli 
 |-  ( x e. { x e. A | B < R } -> x e. A )
26 23 25 syl 
 |-  ( x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) -> x e. A )
27 26 adantl 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> x e. A )
28 27 5 syldan 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> L e. RR* )
29 27 7 syldan 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> R e. RR* )
30 27 4 syldan 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> B e. RR* )
31 mnfxr 
 |-  -oo e. RR*
32 31 a1i 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> -oo e. RR* )
33 28 mnfled 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> -oo <_ L )
34 elinel2 
 |-  ( x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) -> x e. { x e. A | L < B } )
35 rabidim2 
 |-  ( x e. { x e. A | L < B } -> L < B )
36 34 35 syl 
 |-  ( x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) -> L < B )
37 36 adantl 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> L < B )
38 32 28 30 33 37 xrlelttrd 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> -oo < B )
39 32 30 38 xrltned 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> -oo =/= B )
40 39 necomd 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> B =/= -oo )
41 pnfxr 
 |-  +oo e. RR*
42 41 a1i 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> +oo e. RR* )
43 rabidim2 
 |-  ( x e. { x e. A | B < R } -> B < R )
44 23 43 syl 
 |-  ( x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) -> B < R )
45 44 adantl 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> B < R )
46 pnfge 
 |-  ( R e. RR* -> R <_ +oo )
47 29 46 syl 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> R <_ +oo )
48 30 29 42 45 47 xrltletrd 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> B < +oo )
49 30 42 48 xrltned 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> B =/= +oo )
50 30 40 49 xrred 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> B e. RR )
51 28 29 50 37 45 eliood 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> B e. ( L (,) R ) )
52 27 51 jca 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> ( x e. A /\ B e. ( L (,) R ) ) )
53 rabid 
 |-  ( x e. { x e. A | B e. ( L (,) R ) } <-> ( x e. A /\ B e. ( L (,) R ) ) )
54 52 53 sylibr 
 |-  ( ( ph /\ x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) ) -> x e. { x e. A | B e. ( L (,) R ) } )
55 54 ex 
 |-  ( ph -> ( x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) -> x e. { x e. A | B e. ( L (,) R ) } ) )
56 1 55 ralrimi 
 |-  ( ph -> A. x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) x e. { x e. A | B e. ( L (,) R ) } )
57 nfrab1 
 |-  F/_ x { x e. A | B < R }
58 nfrab1 
 |-  F/_ x { x e. A | L < B }
59 57 58 nfin 
 |-  F/_ x ( { x e. A | B < R } i^i { x e. A | L < B } )
60 nfrab1 
 |-  F/_ x { x e. A | B e. ( L (,) R ) }
61 59 60 dfss3f 
 |-  ( ( { x e. A | B < R } i^i { x e. A | L < B } ) C_ { x e. A | B e. ( L (,) R ) } <-> A. x e. ( { x e. A | B < R } i^i { x e. A | L < B } ) x e. { x e. A | B e. ( L (,) R ) } )
62 56 61 sylibr 
 |-  ( ph -> ( { x e. A | B < R } i^i { x e. A | L < B } ) C_ { x e. A | B e. ( L (,) R ) } )
63 22 62 eqssd 
 |-  ( ph -> { x e. A | B e. ( L (,) R ) } = ( { x e. A | B < R } i^i { x e. A | L < B } ) )