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 bilani ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) ) → 𝑓 ∈ ∩ 𝑚 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑚 ) ) ) )
11 nfcv ⊢ Ⅎ 𝑘 𝑓
12 nfcv ⊢ Ⅎ 𝑘 ℕ
13 nfixp1 ⊢ Ⅎ 𝑘 X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑚 ) ) )
14 12 13 nfiin ⊢ Ⅎ 𝑘 ∩ 𝑚 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑚 ) ) )
15 11 14 nfel ⊢ Ⅎ 𝑘 𝑓 ∈ ∩ 𝑚 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑚 ) ) )
16 1 15 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑚 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑚 ) ) ) )
17 2 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑚 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑚 ) ) ) ) ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ )
18 3 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑚 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑚 ) ) ) ) ∧ 𝑘 ∈ 𝑋 ) → 𝐵 ∈ ℝ )
19 9 bilanri ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑚 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑚 ) ) ) ) → 𝑓 ∈ ∩ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) )
20 16 17 18 19 iinhoiicclem ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑚 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑚 ) ) ) ) → 𝑓 ∈ X 𝑘 ∈ 𝑋 ( 𝐴 [,] 𝐵 ) )
21 10 20 syldan ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) ) → 𝑓 ∈ X 𝑘 ∈ 𝑋 ( 𝐴 [,] 𝐵 ) )
22 21 ralrimiva ⊢ ( 𝜑 → ∀ 𝑓 ∈ ∩ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) 𝑓 ∈ X 𝑘 ∈ 𝑋 ( 𝐴 [,] 𝐵 ) )
23 dfss3 ⊢ ( ∩ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) ⊆ X 𝑘 ∈ 𝑋 ( 𝐴 [,] 𝐵 ) ↔ ∀ 𝑓 ∈ ∩ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) 𝑓 ∈ X 𝑘 ∈ 𝑋 ( 𝐴 [,] 𝐵 ) )
24 22 23 sylibr ⊢ ( 𝜑 → ∩ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) ⊆ X 𝑘 ∈ 𝑋 ( 𝐴 [,] 𝐵 ) )
25 nfv ⊢ Ⅎ 𝑘 𝑛 ∈ ℕ
26 1 25 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑛 ∈ ℕ )
27 2 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ* )
28 27 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ* )
29 3 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → 𝐵 ∈ ℝ )
30 nnrp ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ+ )
31 30 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → 𝑛 ∈ ℝ+ )
32 31 rpreccld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 1 / 𝑛 ) ∈ ℝ+ )
33 32 rpred ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 1 / 𝑛 ) ∈ ℝ )
34 29 33 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 + ( 1 / 𝑛 ) ) ∈ ℝ )
35 34 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 + ( 1 / 𝑛 ) ) ∈ ℝ* )
36 2 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ )
37 36 leidd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ≤ 𝐴 )
38 29 32 ltaddrpd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → 𝐵 < ( 𝐵 + ( 1 / 𝑛 ) ) )
39 iccssico ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 + ( 1 / 𝑛 ) ) ∈ ℝ* ) ∧ ( 𝐴 ≤ 𝐴 ∧ 𝐵 < ( 𝐵 + ( 1 / 𝑛 ) ) ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) )
40 28 35 37 38 39 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 [,] 𝐵 ) ⊆ ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) )
41 26 40 ixpssixp ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → X 𝑘 ∈ 𝑋 ( 𝐴 [,] 𝐵 ) ⊆ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) )
42 41 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,] 𝐵 ) ⊆ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) )
43 ssiin ⊢ ( X 𝑘 ∈ 𝑋 ( 𝐴 [,] 𝐵 ) ⊆ ∩ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) ↔ ∀ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,] 𝐵 ) ⊆ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) )
44 42 43 sylibr ⊢ ( 𝜑 → X 𝑘 ∈ 𝑋 ( 𝐴 [,] 𝐵 ) ⊆ ∩ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) )
45 24 44 eqssd ⊢ ( 𝜑 → ∩ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( 𝐴 [,) ( 𝐵 + ( 1 / 𝑛 ) ) ) = X 𝑘 ∈ 𝑋 ( 𝐴 [,] 𝐵 ) )