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 ⊢ Ⅎ 𝑥 𝜑
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 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐿 ∈ ℝ* )
6 5 3adant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) ) → 𝐿 ∈ ℝ* )
7 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑅 ∈ ℝ* )
8 7 3adant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) ) → 𝑅 ∈ ℝ* )
9 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) ) → 𝐵 ∈ ( 𝐿 (,) 𝑅 ) )
10 iooltub ⊢ ( ( 𝐿 ∈ ℝ* ∧ 𝑅 ∈ ℝ* ∧ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) ) → 𝐵 < 𝑅 )
11 6 8 9 10 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) ) → 𝐵 < 𝑅 )
12 11 3exp ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝐵 ∈ ( 𝐿 (,) 𝑅 ) → 𝐵 < 𝑅 ) ) )
13 1 12 ralrimi ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∈ ( 𝐿 (,) 𝑅 ) → 𝐵 < 𝑅 ) )
14 ss2rab ⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∈ ( 𝐿 (,) 𝑅 ) → 𝐵 < 𝑅 ) )
15 13 14 sylibr ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } )
16 ioogtlb ⊢ ( ( 𝐿 ∈ ℝ* ∧ 𝑅 ∈ ℝ* ∧ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) ) → 𝐿 < 𝐵 )
17 6 8 9 16 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) ) → 𝐿 < 𝐵 )
18 17 3exp ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝐵 ∈ ( 𝐿 (,) 𝑅 ) → 𝐿 < 𝐵 ) ) )
19 1 18 ralrimi ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∈ ( 𝐿 (,) 𝑅 ) → 𝐿 < 𝐵 ) )
20 ss2rab ⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∈ ( 𝐿 (,) 𝑅 ) → 𝐿 < 𝐵 ) )
21 19 20 sylibr ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } )
22 15 21 ssind ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) } ⊆ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) )
23 elinel1 ⊢ ( 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) → 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } )
24 ssrab2 ⊢ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ⊆ 𝐴
25 24 sseli ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } → 𝑥 ∈ 𝐴 )
26 23 25 syl ⊢ ( 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) → 𝑥 ∈ 𝐴 )
27 26 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → 𝑥 ∈ 𝐴 )
28 27 5 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → 𝐿 ∈ ℝ* )
29 27 7 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → 𝑅 ∈ ℝ* )
30 27 4 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → 𝐵 ∈ ℝ* )
31 mnfxr ⊢ -∞ ∈ ℝ*
32 31 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → -∞ ∈ ℝ* )
33 28 mnfled ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → -∞ ≤ 𝐿 )
34 elinel2 ⊢ ( 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) → 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } )
35 rabidim2 ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } → 𝐿 < 𝐵 )
36 34 35 syl ⊢ ( 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) → 𝐿 < 𝐵 )
37 36 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → 𝐿 < 𝐵 )
38 32 28 30 33 37 xrlelttrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → -∞ < 𝐵 )
39 32 30 38 xrltned ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → -∞ ≠ 𝐵 )
40 39 necomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → 𝐵 ≠ -∞ )
41 pnfxr ⊢ +∞ ∈ ℝ*
42 41 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → +∞ ∈ ℝ* )
43 rabidim2 ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } → 𝐵 < 𝑅 )
44 23 43 syl ⊢ ( 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) → 𝐵 < 𝑅 )
45 44 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → 𝐵 < 𝑅 )
46 pnfge ⊢ ( 𝑅 ∈ ℝ* → 𝑅 ≤ +∞ )
47 29 46 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → 𝑅 ≤ +∞ )
48 30 29 42 45 47 xrltletrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → 𝐵 < +∞ )
49 30 42 48 xrltned ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → 𝐵 ≠ +∞ )
50 30 40 49 xrred ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → 𝐵 ∈ ℝ )
51 28 29 50 37 45 eliood ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → 𝐵 ∈ ( 𝐿 (,) 𝑅 ) )
52 27 51 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) ) )
53 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) } ↔ ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) ) )
54 52 53 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ) → 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) } )
55 54 ex ⊢ ( 𝜑 → ( 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) → 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) } ) )
56 1 55 ralrimi ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) } )
57 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 }
58 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 }
59 57 58 nfin ⊢ Ⅎ 𝑥 ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } )
60 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) }
61 59 60 dfss3f ⊢ ( ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ⊆ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) } ↔ ∀ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) } )
62 56 61 sylibr ⊢ ( 𝜑 → ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ⊆ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) } )
63 22 62 eqssd ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) } = ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) )