# 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 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
pimiooltgt.2 ${⊢}{\phi }\to {L}\in {ℝ}^{*}$
pimiooltgt.3 ${⊢}{\phi }\to {R}\in {ℝ}^{*}$
pimiooltgt.4 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in {ℝ}^{*}$
Assertion pimiooltgt ${⊢}{\phi }\to \left\{{x}\in {A}|{B}\in \left({L},{R}\right)\right\}=\left\{{x}\in {A}|{B}<{R}\right\}\cap \left\{{x}\in {A}|{L}<{B}\right\}$

### Proof

Step Hyp Ref Expression
1 pimiooltgt.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 pimiooltgt.2 ${⊢}{\phi }\to {L}\in {ℝ}^{*}$
3 pimiooltgt.3 ${⊢}{\phi }\to {R}\in {ℝ}^{*}$
4 pimiooltgt.4 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in {ℝ}^{*}$
5 2 adantr ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {L}\in {ℝ}^{*}$
6 5 3adant3 ${⊢}\left({\phi }\wedge {x}\in {A}\wedge {B}\in \left({L},{R}\right)\right)\to {L}\in {ℝ}^{*}$
7 3 adantr ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {R}\in {ℝ}^{*}$
8 7 3adant3 ${⊢}\left({\phi }\wedge {x}\in {A}\wedge {B}\in \left({L},{R}\right)\right)\to {R}\in {ℝ}^{*}$
9 simp3 ${⊢}\left({\phi }\wedge {x}\in {A}\wedge {B}\in \left({L},{R}\right)\right)\to {B}\in \left({L},{R}\right)$
10 iooltub ${⊢}\left({L}\in {ℝ}^{*}\wedge {R}\in {ℝ}^{*}\wedge {B}\in \left({L},{R}\right)\right)\to {B}<{R}$
11 6 8 9 10 syl3anc ${⊢}\left({\phi }\wedge {x}\in {A}\wedge {B}\in \left({L},{R}\right)\right)\to {B}<{R}$
12 11 3exp ${⊢}{\phi }\to \left({x}\in {A}\to \left({B}\in \left({L},{R}\right)\to {B}<{R}\right)\right)$
13 1 12 ralrimi ${⊢}{\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\in \left({L},{R}\right)\to {B}<{R}\right)$
14 ss2rab ${⊢}\left\{{x}\in {A}|{B}\in \left({L},{R}\right)\right\}\subseteq \left\{{x}\in {A}|{B}<{R}\right\}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\in \left({L},{R}\right)\to {B}<{R}\right)$
15 13 14 sylibr ${⊢}{\phi }\to \left\{{x}\in {A}|{B}\in \left({L},{R}\right)\right\}\subseteq \left\{{x}\in {A}|{B}<{R}\right\}$
16 ioogtlb ${⊢}\left({L}\in {ℝ}^{*}\wedge {R}\in {ℝ}^{*}\wedge {B}\in \left({L},{R}\right)\right)\to {L}<{B}$
17 6 8 9 16 syl3anc ${⊢}\left({\phi }\wedge {x}\in {A}\wedge {B}\in \left({L},{R}\right)\right)\to {L}<{B}$
18 17 3exp ${⊢}{\phi }\to \left({x}\in {A}\to \left({B}\in \left({L},{R}\right)\to {L}<{B}\right)\right)$
19 1 18 ralrimi ${⊢}{\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\in \left({L},{R}\right)\to {L}<{B}\right)$
20 ss2rab ${⊢}\left\{{x}\in {A}|{B}\in \left({L},{R}\right)\right\}\subseteq \left\{{x}\in {A}|{L}<{B}\right\}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\in \left({L},{R}\right)\to {L}<{B}\right)$
21 19 20 sylibr ${⊢}{\phi }\to \left\{{x}\in {A}|{B}\in \left({L},{R}\right)\right\}\subseteq \left\{{x}\in {A}|{L}<{B}\right\}$
22 15 21 ssind ${⊢}{\phi }\to \left\{{x}\in {A}|{B}\in \left({L},{R}\right)\right\}\subseteq \left\{{x}\in {A}|{B}<{R}\right\}\cap \left\{{x}\in {A}|{L}<{B}\right\}$
23 elinel1 ${⊢}{x}\in \left(\left\{{x}\in {A}|{B}<{R}\right\}\cap \left\{{x}\in {A}|{L}<{B}\right\}\right)\to {x}\in \left\{{x}\in {A}|{B}<{R}\right\}$
24 ssrab2 ${⊢}\left\{{x}\in {A}|{B}<{R}\right\}\subseteq {A}$
25 24 sseli ${⊢}{x}\in \left\{{x}\in {A}|{B}<{R}\right\}\to {x}\in {A}$
26 23 25 syl ${⊢}{x}\in \left(\left\{{x}\in {A}|{B}<{R}\right\}\cap \left\{{x}\in {A}|{L}<{B}\right\}\right)\to {x}\in {A}$
27 26 adantl ${⊢}\left({\phi }\wedge {x}\in \left(\left\{{x}\in {A}|{B}<{R}\right\}\cap \left\{{x}\in {A}|{L}<{B}\right\}\right)\right)\to {x}\in {A}$
28 27 5 syldan ${⊢}\left({\phi }\wedge {x}\in \left(\left\{{x}\in {A}|{B}<{R}\right\}\cap \left\{{x}\in {A}|{L}<{B}\right\}\right)\right)\to {L}\in {ℝ}^{*}$
29 27 7 syldan ${⊢}\left({\phi }\wedge {x}\in \left(\left\{{x}\in {A}|{B}<{R}\right\}\cap \left\{{x}\in {A}|{L}<{B}\right\}\right)\right)\to {R}\in {ℝ}^{*}$
30 27 4 syldan ${⊢}\left({\phi }\wedge {x}\in \left(\left\{{x}\in {A}|{B}<{R}\right\}\cap \left\{{x}\in {A}|{L}<{B}\right\}\right)\right)\to {B}\in {ℝ}^{*}$
31 mnfxr ${⊢}\mathrm{-\infty }\in {ℝ}^{*}$
32 31 a1i ${⊢}\left({\phi }\wedge {x}\in \left(\left\{{x}\in {A}|{B}<{R}\right\}\cap \left\{{x}\in {A}|{L}<{B}\right\}\right)\right)\to \mathrm{-\infty }\in {ℝ}^{*}$
33 28 mnfled ${⊢}\left({\phi }\wedge {x}\in \left(\left\{{x}\in {A}|{B}<{R}\right\}\cap \left\{{x}\in {A}|{L}<{B}\right\}\right)\right)\to \mathrm{-\infty }\le {L}$
34 elinel2 ${⊢}{x}\in \left(\left\{{x}\in {A}|{B}<{R}\right\}\cap \left\{{x}\in {A}|{L}<{B}\right\}\right)\to {x}\in \left\{{x}\in {A}|{L}<{B}\right\}$
35 rabidim2 ${⊢}{x}\in \left\{{x}\in {A}|{L}<{B}\right\}\to {L}<{B}$
36 34 35 syl ${⊢}{x}\in \left(\left\{{x}\in {A}|{B}<{R}\right\}\cap \left\{{x}\in {A}|{L}<{B}\right\}\right)\to {L}<{B}$
37 36 adantl ${⊢}\left({\phi }\wedge {x}\in \left(\left\{{x}\in {A}|{B}<{R}\right\}\cap \left\{{x}\in {A}|{L}<{B}\right\}\right)\right)\to {L}<{B}$
38 32 28 30 33 37 xrlelttrd ${⊢}\left({\phi }\wedge {x}\in \left(\left\{{x}\in {A}|{B}<{R}\right\}\cap \left\{{x}\in {A}|{L}<{B}\right\}\right)\right)\to \mathrm{-\infty }<{B}$
39 32 30 38 xrltned ${⊢}\left({\phi }\wedge {x}\in \left(\left\{{x}\in {A}|{B}<{R}\right\}\cap \left\{{x}\in {A}|{L}<{B}\right\}\right)\right)\to \mathrm{-\infty }\ne {B}$
40 39 necomd ${⊢}\left({\phi }\wedge {x}\in \left(\left\{{x}\in {A}|{B}<{R}\right\}\cap \left\{{x}\in {A}|{L}<{B}\right\}\right)\right)\to {B}\ne \mathrm{-\infty }$
41 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
42 41 a1i ${⊢}\left({\phi }\wedge {x}\in \left(\left\{{x}\in {A}|{B}<{R}\right\}\cap \left\{{x}\in {A}|{L}<{B}\right\}\right)\right)\to \mathrm{+\infty }\in {ℝ}^{*}$
43 rabidim2 ${⊢}{x}\in \left\{{x}\in {A}|{B}<{R}\right\}\to {B}<{R}$
44 23 43 syl ${⊢}{x}\in \left(\left\{{x}\in {A}|{B}<{R}\right\}\cap \left\{{x}\in {A}|{L}<{B}\right\}\right)\to {B}<{R}$
45 44 adantl ${⊢}\left({\phi }\wedge {x}\in \left(\left\{{x}\in {A}|{B}<{R}\right\}\cap \left\{{x}\in {A}|{L}<{B}\right\}\right)\right)\to {B}<{R}$
46 pnfge ${⊢}{R}\in {ℝ}^{*}\to {R}\le \mathrm{+\infty }$
47 29 46 syl ${⊢}\left({\phi }\wedge {x}\in \left(\left\{{x}\in {A}|{B}<{R}\right\}\cap \left\{{x}\in {A}|{L}<{B}\right\}\right)\right)\to {R}\le \mathrm{+\infty }$
48 30 29 42 45 47 xrltletrd ${⊢}\left({\phi }\wedge {x}\in \left(\left\{{x}\in {A}|{B}<{R}\right\}\cap \left\{{x}\in {A}|{L}<{B}\right\}\right)\right)\to {B}<\mathrm{+\infty }$
49 30 42 48 xrltned ${⊢}\left({\phi }\wedge {x}\in \left(\left\{{x}\in {A}|{B}<{R}\right\}\cap \left\{{x}\in {A}|{L}<{B}\right\}\right)\right)\to {B}\ne \mathrm{+\infty }$
50 30 40 49 xrred ${⊢}\left({\phi }\wedge {x}\in \left(\left\{{x}\in {A}|{B}<{R}\right\}\cap \left\{{x}\in {A}|{L}<{B}\right\}\right)\right)\to {B}\in ℝ$
51 28 29 50 37 45 eliood ${⊢}\left({\phi }\wedge {x}\in \left(\left\{{x}\in {A}|{B}<{R}\right\}\cap \left\{{x}\in {A}|{L}<{B}\right\}\right)\right)\to {B}\in \left({L},{R}\right)$
52 27 51 jca ${⊢}\left({\phi }\wedge {x}\in \left(\left\{{x}\in {A}|{B}<{R}\right\}\cap \left\{{x}\in {A}|{L}<{B}\right\}\right)\right)\to \left({x}\in {A}\wedge {B}\in \left({L},{R}\right)\right)$
53 rabid ${⊢}{x}\in \left\{{x}\in {A}|{B}\in \left({L},{R}\right)\right\}↔\left({x}\in {A}\wedge {B}\in \left({L},{R}\right)\right)$
54 52 53 sylibr ${⊢}\left({\phi }\wedge {x}\in \left(\left\{{x}\in {A}|{B}<{R}\right\}\cap \left\{{x}\in {A}|{L}<{B}\right\}\right)\right)\to {x}\in \left\{{x}\in {A}|{B}\in \left({L},{R}\right)\right\}$
55 54 ex ${⊢}{\phi }\to \left({x}\in \left(\left\{{x}\in {A}|{B}<{R}\right\}\cap \left\{{x}\in {A}|{L}<{B}\right\}\right)\to {x}\in \left\{{x}\in {A}|{B}\in \left({L},{R}\right)\right\}\right)$
56 1 55 ralrimi ${⊢}{\phi }\to \forall {x}\in \left(\left\{{x}\in {A}|{B}<{R}\right\}\cap \left\{{x}\in {A}|{L}<{B}\right\}\right)\phantom{\rule{.4em}{0ex}}{x}\in \left\{{x}\in {A}|{B}\in \left({L},{R}\right)\right\}$
57 nfrab1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{{x}\in {A}|{B}<{R}\right\}$
58 nfrab1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{{x}\in {A}|{L}<{B}\right\}$
59 57 58 nfin ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left(\left\{{x}\in {A}|{B}<{R}\right\}\cap \left\{{x}\in {A}|{L}<{B}\right\}\right)$
60 nfrab1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{{x}\in {A}|{B}\in \left({L},{R}\right)\right\}$
61 59 60 dfss3f ${⊢}\left\{{x}\in {A}|{B}<{R}\right\}\cap \left\{{x}\in {A}|{L}<{B}\right\}\subseteq \left\{{x}\in {A}|{B}\in \left({L},{R}\right)\right\}↔\forall {x}\in \left(\left\{{x}\in {A}|{B}<{R}\right\}\cap \left\{{x}\in {A}|{L}<{B}\right\}\right)\phantom{\rule{.4em}{0ex}}{x}\in \left\{{x}\in {A}|{B}\in \left({L},{R}\right)\right\}$
62 56 61 sylibr ${⊢}{\phi }\to \left\{{x}\in {A}|{B}<{R}\right\}\cap \left\{{x}\in {A}|{L}<{B}\right\}\subseteq \left\{{x}\in {A}|{B}\in \left({L},{R}\right)\right\}$
63 22 62 eqssd ${⊢}{\phi }\to \left\{{x}\in {A}|{B}\in \left({L},{R}\right)\right\}=\left\{{x}\in {A}|{B}<{R}\right\}\cap \left\{{x}\in {A}|{L}<{B}\right\}$