Metamath Proof Explorer

Theorem iinhoiicc

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

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

Proof

Step Hyp Ref Expression
1 iunhoiicc.k ⊢ Ⅎ 𝑘 𝜑
2 iunhoiicc.a ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ )
3 iunhoiicc.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐵 ∈ ℝ )
4 oveq2 ⊢ ( 𝑛 = 𝑚 → ( 1 / 𝑛 ) = ( 1 / 𝑚 ) )
5 4 oveq2d ⊢ ( 𝑛 = 𝑚 → ( 𝐵 + ( 1 / 𝑛 ) ) = ( 𝐵 + ( 1 / 𝑚 ) ) )
6 5 oveq2d ⊢ ( 𝑛 = 𝑚 → ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) = ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑚 ) ) ) )
7 6 ixpeq2dv ⊢ ( 𝑛 = 𝑚 → X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) = X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑚 ) ) ) )
8 7 cbviinv ⊢ ∩ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) = ∩ 𝑚 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑚 ) ) )
9 8 eleq2i ⊢ ( 𝑓 ∈ ∩ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) ↔ 𝑓 ∈ ∩ 𝑚 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑚 ) ) ) )
10 9 biimpi ⊢ ( 𝑓 ∈ ∩ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) → 𝑓 ∈ ∩ 𝑚 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑚 ) ) ) )
11 10 adantl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) ) → 𝑓 ∈ ∩ 𝑚 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑚 ) ) ) )
12 nfcv ⊢ Ⅎ 𝑘 𝑓
13 nfcv ⊢ Ⅎ 𝑘 ℕ
14 nfixp1 ⊢ Ⅎ 𝑘 X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑚 ) ) )
15 13 14 nfiin ⊢ Ⅎ 𝑘 ∩ 𝑚 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑚 ) ) )
16 12 15 nfel ⊢ Ⅎ 𝑘 𝑓 ∈ ∩ 𝑚 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑚 ) ) )
17 1 16 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑚 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑚 ) ) ) )
18 2 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑚 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑚 ) ) ) ) ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ )
19 3 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑚 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑚 ) ) ) ) ∧ 𝑘 ∈ 𝑋 ) → 𝐵 ∈ ℝ )
20 9 biimpri ⊢ ( 𝑓 ∈ ∩ 𝑚 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑚 ) ) ) → 𝑓 ∈ ∩ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) )
21 20 adantl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑚 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑚 ) ) ) ) → 𝑓 ∈ ∩ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) )
22 17 18 19 21 iinhoiicclem ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑚 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑚 ) ) ) ) → 𝑓 ∈ X 𝑘 ∈ 𝑋 ( 𝐴 [,] 𝐵 ) )
23 11 22 syldan ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) ) → 𝑓 ∈ X 𝑘 ∈ 𝑋 ( 𝐴 [,] 𝐵 ) )
24 23 ralrimiva ⊢ ( 𝜑 → ∀ 𝑓 ∈ ∩ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) 𝑓 ∈ X 𝑘 ∈ 𝑋 ( 𝐴 [,] 𝐵 ) )
25 dfss3 ⊢ ( ∩ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) ⊆ X 𝑘 ∈ 𝑋 ( 𝐴 [,] 𝐵 ) ↔ ∀ 𝑓 ∈ ∩ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) 𝑓 ∈ X 𝑘 ∈ 𝑋 ( 𝐴 [,] 𝐵 ) )
26 24 25 sylibr ⊢ ( 𝜑 → ∩ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) ⊆ X 𝑘 ∈ 𝑋 ( 𝐴 [,] 𝐵 ) )
27 nfv ⊢ Ⅎ 𝑘 𝑛 ∈ ℕ
28 1 27 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑛 ∈ ℕ )
29 2 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ* )
30 29 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ* )
31 3 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → 𝐵 ∈ ℝ )
32 nnrp ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ+ )
33 32 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → 𝑛 ∈ ℝ+ )
34 33 rpreccld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 1 / 𝑛 ) ∈ ℝ+ )
35 34 rpred ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 1 / 𝑛 ) ∈ ℝ )
36 31 35 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 + ( 1 / 𝑛 ) ) ∈ ℝ )
37 36 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 + ( 1 / 𝑛 ) ) ∈ ℝ* )
38 2 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ )
39 38 leidd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ≤ 𝐴 )
40 31 34 ltaddrpd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → 𝐵 < ( 𝐵 + ( 1 / 𝑛 ) ) )
41 iccssico ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 + ( 1 / 𝑛 ) ) ∈ ℝ* ) ∧ ( 𝐴 ≤ 𝐴 ∧ 𝐵 < ( 𝐵 + ( 1 / 𝑛 ) ) ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) )
42 30 37 39 40 41 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 [,] 𝐵 ) ⊆ ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) )
43 28 42 ixpssixp ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → X 𝑘 ∈ 𝑋 ( 𝐴 [,] 𝐵 ) ⊆ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) )
44 43 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,] 𝐵 ) ⊆ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) )
45 ssiin ⊢ ( X 𝑘 ∈ 𝑋 ( 𝐴 [,] 𝐵 ) ⊆ ∩ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) ↔ ∀ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,] 𝐵 ) ⊆ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) )
46 44 45 sylibr ⊢ ( 𝜑 → X 𝑘 ∈ 𝑋 ( 𝐴 [,] 𝐵 ) ⊆ ∩ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) )
47 26 46 eqssd ⊢ ( 𝜑 → ∩ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) = X 𝑘 ∈ 𝑋 ( 𝐴 [,] 𝐵 ) )