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	⊢ Ⅎ 𝑥 𝜑
	pimiooltgt.2	⊢ ( 𝜑 → 𝐿 ∈ ℝ* )
	pimiooltgt.3	⊢ ( 𝜑 → 𝑅 ∈ ℝ* )
	pimiooltgt.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
Assertion	pimiooltgt	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) } = ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) )

Proof

Step	Hyp	Ref	Expression
1		pimiooltgt.1	⊢ Ⅎ 𝑥 𝜑
2		pimiooltgt.2	⊢ ( 𝜑 → 𝐿 ∈ ℝ* )
3		pimiooltgt.3	⊢ ( 𝜑 → 𝑅 ∈ ℝ* )
4		pimiooltgt.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
5	2	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) ) → 𝐿 ∈ ℝ* )
6	3	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) ) → 𝑅 ∈ ℝ* )
7		simp3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) ) → 𝐵 ∈ ( 𝐿 (,) 𝑅 ) )
8	5 6 7	iooltubd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) ) → 𝐵 < 𝑅 )
9	8	3exp	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝐵 ∈ ( 𝐿 (,) 𝑅 ) → 𝐵 < 𝑅 ) ) )
10	1 9	ralrimi	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∈ ( 𝐿 (,) 𝑅 ) → 𝐵 < 𝑅 ) )
11	10	ss2rabd	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } )
12	5 6 7	ioogtlbd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) ) → 𝐿 < 𝐵 )
13	12	3exp	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝐵 ∈ ( 𝐿 (,) 𝑅 ) → 𝐿 < 𝐵 ) ) )
14	1 13	ralrimi	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∈ ( 𝐿 (,) 𝑅 ) → 𝐿 < 𝐵 ) )
15	14	ss2rabd	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } )
16	11 15	ssind	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) } ⊆ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) )
17		nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 }
18		nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 }
19	17 18	nfin	⊢ Ⅎ 𝑥 ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } )
20		nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) }
21		elinel1	⊢ ( 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) → 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } )
22		rabidim1	⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } → 𝑥 ∈ 𝐴 )
23	21 22	syl	⊢ ( 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) → 𝑥 ∈ 𝐴 )
24	23	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → 𝑥 ∈ 𝐴 )
25	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → 𝐿 ∈ ℝ* )
26	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → 𝑅 ∈ ℝ* )
27	23 4	sylan2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → 𝐵 ∈ ℝ* )
28		mnfxr	⊢ -∞ ∈ ℝ*
29	28	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → -∞ ∈ ℝ* )
30	25	mnfled	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → -∞ ≤ 𝐿 )
31		elinel2	⊢ ( 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) → 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } )
32		rabidim2	⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } → 𝐿 < 𝐵 )
33	31 32	syl	⊢ ( 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) → 𝐿 < 𝐵 )
34	33	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → 𝐿 < 𝐵 )
35	29 25 27 30 34	xrlelttrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → -∞ < 𝐵 )
36	29 27 35	xrgtned	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → 𝐵 ≠ -∞ )
37		pnfxr	⊢ +∞ ∈ ℝ*
38	37	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → +∞ ∈ ℝ* )
39		rabidim2	⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } → 𝐵 < 𝑅 )
40	21 39	syl	⊢ ( 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) → 𝐵 < 𝑅 )
41	40	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → 𝐵 < 𝑅 )
42	26	pnfged	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → 𝑅 ≤ +∞ )
43	27 26 38 41 42	xrltletrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → 𝐵 < +∞ )
44	27 38 43	xrltned	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → 𝐵 ≠ +∞ )
45	27 36 44	xrred	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → 𝐵 ∈ ℝ )
46	25 26 45 34 41	eliood	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → 𝐵 ∈ ( 𝐿 (,) 𝑅 ) )
47	24 46	rabidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) } )
48	1 19 20 47	ssdf2	⊢ ( 𝜑 → ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ⊆ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) } )
49	16 48	eqssd	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) } = ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) )