Metamath Proof Explorer

Theorem iinhoiicclem

Description: A n-dimensional closed interval expressed as the indexed intersection of half-open intervals. One side of the double inclusion. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses iinhoiicclem.k ⊢ Ⅎ 𝑘 𝜑
iinhoiicclem.a ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ )
iinhoiicclem.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐵 ∈ ℝ )
iinhoiicclem.f ⊢ ( 𝜑 → 𝐹 ∈ ∩ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) )
Assertion iinhoiicclem ( 𝜑 → 𝐹 ∈ X 𝑘 ∈ 𝑋 ( 𝐴 [,] 𝐵 ) )

Proof

Step Hyp Ref Expression
1 iinhoiicclem.k ⊢ Ⅎ 𝑘 𝜑
2 iinhoiicclem.a ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ )
3 iinhoiicclem.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐵 ∈ ℝ )
4 iinhoiicclem.f ⊢ ( 𝜑 → 𝐹 ∈ ∩ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) )
5 4 elexd ⊢ ( 𝜑 → 𝐹 ∈ V )
6 1nn ⊢ 1 ∈ ℕ
7 6 a1i ⊢ ( 𝜑 → 1 ∈ ℕ )
8 peano2re ⊢ ( 𝐵 ∈ ℝ → ( 𝐵 + 1 ) ∈ ℝ )
9 3 8 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 + 1 ) ∈ ℝ )
10 9 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 + 1 ) ∈ ℝ* )
11 icossre ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 + 1 ) ∈ ℝ* ) → ( 𝐴 [,) ( 𝐵 + 1 ) ) ⊆ ℝ )
12 2 10 11 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 [,) ( 𝐵 + 1 ) ) ⊆ ℝ )
13 1 12 ixpssixp ⊢ ( 𝜑 → X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + 1 ) ) ⊆ X 𝑘 ∈ 𝑋 ℝ )
14 oveq2 ⊢ ( 𝑛 = 1 → ( 1 / 𝑛 ) = ( 1 / 1 ) )
15 1div1e1 ⊢ ( 1 / 1 ) = 1
16 15 a1i ⊢ ( 𝑛 = 1 → ( 1 / 1 ) = 1 )
17 14 16 eqtrd ⊢ ( 𝑛 = 1 → ( 1 / 𝑛 ) = 1 )
18 17 oveq2d ⊢ ( 𝑛 = 1 → ( 𝐵 + ( 1 / 𝑛 ) ) = ( 𝐵 + 1 ) )
19 18 oveq2d ⊢ ( 𝑛 = 1 → ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) = ( 𝐴 [,) ( 𝐵 + 1 ) ) )
20 19 ixpeq2dv ⊢ ( 𝑛 = 1 → X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) = X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + 1 ) ) )
21 20 sseq1d ⊢ ( 𝑛 = 1 → ( X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) ⊆ X 𝑘 ∈ 𝑋 ℝ ↔ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + 1 ) ) ⊆ X 𝑘 ∈ 𝑋 ℝ ) )
22 21 rspcev ⊢ ( ( 1 ∈ ℕ ∧ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + 1 ) ) ⊆ X 𝑘 ∈ 𝑋 ℝ ) → ∃ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) ⊆ X 𝑘 ∈ 𝑋 ℝ )
23 7 13 22 syl2anc ⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) ⊆ X 𝑘 ∈ 𝑋 ℝ )
24 iinss ⊢ ( ∃ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) ⊆ X 𝑘 ∈ 𝑋 ℝ → ∩ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) ⊆ X 𝑘 ∈ 𝑋 ℝ )
25 23 24 syl ⊢ ( 𝜑 → ∩ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) ⊆ X 𝑘 ∈ 𝑋 ℝ )
26 25 4 sseldd ⊢ ( 𝜑 → 𝐹 ∈ X 𝑘 ∈ 𝑋 ℝ )
27 elixpconstg ⊢ ( 𝐹 ∈ ∩ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) → ( 𝐹 ∈ X 𝑘 ∈ 𝑋 ℝ ↔ 𝐹 : 𝑋 ⟶ ℝ ) )
28 4 27 syl ⊢ ( 𝜑 → ( 𝐹 ∈ X 𝑘 ∈ 𝑋 ℝ ↔ 𝐹 : 𝑋 ⟶ ℝ ) )
29 26 28 mpbid ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℝ )
30 29 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝑋 )
31 29 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
32 2 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ* )
33 ssid ⊢ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + 1 ) ) ⊆ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + 1 ) )
34 33 a1i ⊢ ( 𝜑 → X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + 1 ) ) ⊆ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + 1 ) ) )
35 20 sseq1d ⊢ ( 𝑛 = 1 → ( X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) ⊆ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + 1 ) ) ↔ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + 1 ) ) ⊆ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + 1 ) ) ) )
36 35 rspcev ⊢ ( ( 1 ∈ ℕ ∧ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + 1 ) ) ⊆ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + 1 ) ) ) → ∃ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) ⊆ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + 1 ) ) )
37 7 34 36 syl2anc ⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) ⊆ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + 1 ) ) )
38 iinss ⊢ ( ∃ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) ⊆ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + 1 ) ) → ∩ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) ⊆ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + 1 ) ) )
39 37 38 syl ⊢ ( 𝜑 → ∩ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) ⊆ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + 1 ) ) )
40 39 4 sseldd ⊢ ( 𝜑 → 𝐹 ∈ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + 1 ) ) )
41 40 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐹 ∈ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + 1 ) ) )
42 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝑘 ∈ 𝑋 )
43 fvixp2 ⊢ ( ( 𝐹 ∈ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + 1 ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 𝐴 [,) ( 𝐵 + 1 ) ) )
44 41 42 43 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 𝐴 [,) ( 𝐵 + 1 ) ) )
45 icogelb ⊢ ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 + 1 ) ∈ ℝ* ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝐴 [,) ( 𝐵 + 1 ) ) ) → 𝐴 ≤ ( 𝐹 ‘ 𝑘 ) )
46 32 10 44 45 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ≤ ( 𝐹 ‘ 𝑘 ) )
47 31 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
48 3 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑛 ∈ ℕ ) → 𝐵 ∈ ℝ )
49 nnrecre ⊢ ( 𝑛 ∈ ℕ → ( 1 / 𝑛 ) ∈ ℝ )
50 49 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑛 ∈ ℕ ) → ( 1 / 𝑛 ) ∈ ℝ )
51 48 50 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑛 ∈ ℕ ) → ( 𝐵 + ( 1 / 𝑛 ) ) ∈ ℝ )
52 32 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑛 ∈ ℕ ) → 𝐴 ∈ ℝ* )
53 ressxr ⊢ ℝ ⊆ ℝ*
54 53 51 sselid ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑛 ∈ ℕ ) → ( 𝐵 + ( 1 / 𝑛 ) ) ∈ ℝ* )
55 eliin ⊢ ( 𝐹 ∈ V → ( 𝐹 ∈ ∩ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) ↔ ∀ 𝑛 ∈ ℕ 𝐹 ∈ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) ) )
56 5 55 syl ⊢ ( 𝜑 → ( 𝐹 ∈ ∩ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) ↔ ∀ 𝑛 ∈ ℕ 𝐹 ∈ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) ) )
57 4 56 mpbid ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ 𝐹 ∈ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) )
58 57 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐹 ∈ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) )
59 elixp2 ⊢ ( 𝐹 ∈ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) ↔ ( 𝐹 ∈ V ∧ 𝐹 Fn 𝑋 ∧ ∀ 𝑘 ∈ 𝑋 ( 𝐹 ‘ 𝑘 ) ∈ ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) ) )
60 58 59 sylib ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ∈ V ∧ 𝐹 Fn 𝑋 ∧ ∀ 𝑘 ∈ 𝑋 ( 𝐹 ‘ 𝑘 ) ∈ ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) ) )
61 60 simp3d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∀ 𝑘 ∈ 𝑋 ( 𝐹 ‘ 𝑘 ) ∈ ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) )
62 61 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) )
63 62 an32s ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) )
64 icoltub ⊢ ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 + ( 1 / 𝑛 ) ) ∈ ℝ* ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) ) → ( 𝐹 ‘ 𝑘 ) < ( 𝐵 + ( 1 / 𝑛 ) ) )
65 52 54 63 64 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) < ( 𝐵 + ( 1 / 𝑛 ) ) )
66 47 51 65 ltled ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐵 + ( 1 / 𝑛 ) ) )
67 66 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐵 + ( 1 / 𝑛 ) ) )
68 nfv ⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑘 ∈ 𝑋 )
69 53 31 sselid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ* )
70 68 69 3 xrralrecnnle ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑘 ) ≤ 𝐵 ↔ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐵 + ( 1 / 𝑛 ) ) ) )
71 67 70 mpbird ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑘 ) ≤ 𝐵 )
72 2 3 31 46 71 eliccd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 𝐴 [,] 𝐵 ) )
73 72 ex ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑋 → ( 𝐹 ‘ 𝑘 ) ∈ ( 𝐴 [,] 𝐵 ) ) )
74 1 73 ralrimi ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑋 ( 𝐹 ‘ 𝑘 ) ∈ ( 𝐴 [,] 𝐵 ) )
75 5 30 74 3jca ⊢ ( 𝜑 → ( 𝐹 ∈ V ∧ 𝐹 Fn 𝑋 ∧ ∀ 𝑘 ∈ 𝑋 ( 𝐹 ‘ 𝑘 ) ∈ ( 𝐴 [,] 𝐵 ) ) )
76 elixp2 ⊢ ( 𝐹 ∈ X 𝑘 ∈ 𝑋 ( 𝐴 [,] 𝐵 ) ↔ ( 𝐹 ∈ V ∧ 𝐹 Fn 𝑋 ∧ ∀ 𝑘 ∈ 𝑋 ( 𝐹 ‘ 𝑘 ) ∈ ( 𝐴 [,] 𝐵 ) ) )
77 75 76 sylibr ⊢ ( 𝜑 → 𝐹 ∈ X 𝑘 ∈ 𝑋 ( 𝐴 [,] 𝐵 ) )