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