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 φ$
	pimiooltgt.2	$⊢ φ \to L \in ℝ^{*}$
	pimiooltgt.3	$⊢ φ \to R \in ℝ^{*}$
	pimiooltgt.4	$⊢ (φ \land x \in A) \to B \in ℝ^{*}$
Assertion	pimiooltgt	$⊢ φ \to \{x \in A \| B \in (L, R)\} = \{x \in A \| B < R\} \cap \{x \in A \| L < B\}$

Proof

Step	Hyp	Ref	Expression
1		pimiooltgt.1	$⊢ Ⅎ x φ$
2		pimiooltgt.2	$⊢ φ \to L \in ℝ^{*}$
3		pimiooltgt.3	$⊢ φ \to R \in ℝ^{*}$
4		pimiooltgt.4	$⊢ (φ \land x \in A) \to B \in ℝ^{*}$
5	2	3ad2ant1	$⊢ (φ \land x \in A \land B \in (L, R)) \to L \in ℝ^{*}$
6	3	3ad2ant1	$⊢ (φ \land x \in A \land B \in (L, R)) \to R \in ℝ^{*}$
7		simp3	$⊢ (φ \land x \in A \land B \in (L, R)) \to B \in (L, R)$
8	5 6 7	iooltubd	$⊢ (φ \land x \in A \land B \in (L, R)) \to B < R$
9	8	3exp	$⊢ φ \to (x \in A \to (B \in (L, R) \to B < R))$
10	1 9	ralrimi	$⊢ φ \to \forall x \in A (B \in (L, R) \to B < R)$
11	10	ss2rabd	$⊢ φ \to \{x \in A \| B \in (L, R)\} \subseteq \{x \in A \| B < R\}$
12	5 6 7	ioogtlbd	$⊢ (φ \land x \in A \land B \in (L, R)) \to L < B$
13	12	3exp	$⊢ φ \to (x \in A \to (B \in (L, R) \to L < B))$
14	1 13	ralrimi	$⊢ φ \to \forall x \in A (B \in (L, R) \to L < B)$
15	14	ss2rabd	$⊢ φ \to \{x \in A \| B \in (L, R)\} \subseteq \{x \in A \| L < B\}$
16	11 15	ssind	$⊢ φ \to \{x \in A \| B \in (L, R)\} \subseteq \{x \in A \| B < R\} \cap \{x \in A \| L < B\}$
17		nfrab1	$⊢ \underline{Ⅎ} x \{x \in A \| B < R\}$
18		nfrab1	$⊢ \underline{Ⅎ} x \{x \in A \| L < B\}$
19	17 18	nfin	$⊢ \underline{Ⅎ} x (\{x \in A \| B < R\} \cap \{x \in A \| L < B\})$
20		nfrab1	$⊢ \underline{Ⅎ} x \{x \in A \| B \in (L, R)\}$
21		elinel1	$⊢ x \in (\{x \in A \| B < R\} \cap \{x \in A \| L < B\}) \to x \in \{x \in A \| B < R\}$
22		rabidim1	$⊢ x \in \{x \in A \| B < R\} \to x \in A$
23	21 22	syl	$⊢ x \in (\{x \in A \| B < R\} \cap \{x \in A \| L < B\}) \to x \in A$
24	23	adantl	$⊢ (φ \land x \in (\{x \in A \| B < R\} \cap \{x \in A \| L < B\})) \to x \in A$
25	2	adantr	$⊢ (φ \land x \in (\{x \in A \| B < R\} \cap \{x \in A \| L < B\})) \to L \in ℝ^{*}$
26	3	adantr	$⊢ (φ \land x \in (\{x \in A \| B < R\} \cap \{x \in A \| L < B\})) \to R \in ℝ^{*}$
27	23 4	sylan2	$⊢ (φ \land x \in (\{x \in A \| B < R\} \cap \{x \in A \| L < B\})) \to B \in ℝ^{*}$
28		mnfxr	$⊢ −∞ \in ℝ^{*}$
29	28	a1i	$⊢ (φ \land x \in (\{x \in A \| B < R\} \cap \{x \in A \| L < B\})) \to −∞ \in ℝ^{*}$
30	25	mnfled	$⊢ (φ \land x \in (\{x \in A \| B < R\} \cap \{x \in A \| L < B\})) \to −∞ \leq L$
31		elinel2	$⊢ x \in (\{x \in A \| B < R\} \cap \{x \in A \| L < B\}) \to x \in \{x \in A \| L < B\}$
32		rabidim2	$⊢ x \in \{x \in A \| L < B\} \to L < B$
33	31 32	syl	$⊢ x \in (\{x \in A \| B < R\} \cap \{x \in A \| L < B\}) \to L < B$
34	33	adantl	$⊢ (φ \land x \in (\{x \in A \| B < R\} \cap \{x \in A \| L < B\})) \to L < B$
35	29 25 27 30 34	xrlelttrd	$⊢ (φ \land x \in (\{x \in A \| B < R\} \cap \{x \in A \| L < B\})) \to −∞ < B$
36	29 27 35	xrgtned	$⊢ (φ \land x \in (\{x \in A \| B < R\} \cap \{x \in A \| L < B\})) \to B \neq −∞$
37		pnfxr	$⊢ +∞ \in ℝ^{*}$
38	37	a1i	$⊢ (φ \land x \in (\{x \in A \| B < R\} \cap \{x \in A \| L < B\})) \to +∞ \in ℝ^{*}$
39		rabidim2	$⊢ x \in \{x \in A \| B < R\} \to B < R$
40	21 39	syl	$⊢ x \in (\{x \in A \| B < R\} \cap \{x \in A \| L < B\}) \to B < R$
41	40	adantl	$⊢ (φ \land x \in (\{x \in A \| B < R\} \cap \{x \in A \| L < B\})) \to B < R$
42	26	pnfged	$⊢ (φ \land x \in (\{x \in A \| B < R\} \cap \{x \in A \| L < B\})) \to R \leq +∞$
43	27 26 38 41 42	xrltletrd	$⊢ (φ \land x \in (\{x \in A \| B < R\} \cap \{x \in A \| L < B\})) \to B < +∞$
44	27 38 43	xrltned	$⊢ (φ \land x \in (\{x \in A \| B < R\} \cap \{x \in A \| L < B\})) \to B \neq +∞$
45	27 36 44	xrred	$⊢ (φ \land x \in (\{x \in A \| B < R\} \cap \{x \in A \| L < B\})) \to B \in ℝ$
46	25 26 45 34 41	eliood	$⊢ (φ \land x \in (\{x \in A \| B < R\} \cap \{x \in A \| L < B\})) \to B \in (L, R)$
47	24 46	rabidd	$⊢ (φ \land x \in (\{x \in A \| B < R\} \cap \{x \in A \| L < B\})) \to x \in \{x \in A \| B \in (L, R)\}$
48	1 19 20 47	ssdf2	$⊢ φ \to \{x \in A \| B < R\} \cap \{x \in A \| L < B\} \subseteq \{x \in A \| B \in (L, R)\}$
49	16 48	eqssd	$⊢ φ \to \{x \in A \| B \in (L, R)\} = \{x \in A \| B < R\} \cap \{x \in A \| L < B\}$

Metamath Proof Explorer

Theorem pimiooltgt

Proof