Metamath Proof Explorer

Theorem rrxsnicc

Description: A multidimensional singleton expressed as a multidimensional closed interval. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypothesis rrxsnicc.1 ⊢ φ → A ∈ ℝ X
Assertion rrxsnicc ⊢ φ → ⨉ k ∈ X A ⁡ k A ⁡ k = A

Proof

Step Hyp Ref Expression
1 rrxsnicc.1 ⊢ φ → A ∈ ℝ X
2 ixpfn ⊢ f ∈ ⨉ k ∈ X A ⁡ k A ⁡ k → f Fn X
3 2 adantl ⊢ φ ∧ f ∈ ⨉ k ∈ X A ⁡ k A ⁡ k → f Fn X
4 elmapfn ⊢ A ∈ ℝ X → A Fn X
5 1 4 syl ⊢ φ → A Fn X
6 5 adantr ⊢ φ ∧ f ∈ ⨉ k ∈ X A ⁡ k A ⁡ k → A Fn X
7 simpll ⊢ φ ∧ f ∈ ⨉ k ∈ X A ⁡ k A ⁡ k ∧ j ∈ X → φ
8 fveq2 ⊢ k = j → A ⁡ k = A ⁡ j
9 8 8 oveq12d ⊢ k = j → A ⁡ k A ⁡ k = A ⁡ j A ⁡ j
10 9 cbvixpv ⊢ ⨉ k ∈ X A ⁡ k A ⁡ k = ⨉ j ∈ X A ⁡ j A ⁡ j
11 10 eleq2i ⊢ f ∈ ⨉ k ∈ X A ⁡ k A ⁡ k ↔ f ∈ ⨉ j ∈ X A ⁡ j A ⁡ j
12 11 biimpi ⊢ f ∈ ⨉ k ∈ X A ⁡ k A ⁡ k → f ∈ ⨉ j ∈ X A ⁡ j A ⁡ j
13 12 ad2antlr ⊢ φ ∧ f ∈ ⨉ k ∈ X A ⁡ k A ⁡ k ∧ j ∈ X → f ∈ ⨉ j ∈ X A ⁡ j A ⁡ j
14 simpr ⊢ φ ∧ f ∈ ⨉ k ∈ X A ⁡ k A ⁡ k ∧ j ∈ X → j ∈ X
15 elmapi ⊢ A ∈ ℝ X → A : X ⟶ ℝ
16 1 15 syl ⊢ φ → A : X ⟶ ℝ
17 16 ffvelcdmda ⊢ φ ∧ j ∈ X → A ⁡ j ∈ ℝ
18 17 adantlr ⊢ φ ∧ f ∈ ⨉ j ∈ X A ⁡ j A ⁡ j ∧ j ∈ X → A ⁡ j ∈ ℝ
19 18 18 iccssred ⊢ φ ∧ f ∈ ⨉ j ∈ X A ⁡ j A ⁡ j ∧ j ∈ X → A ⁡ j A ⁡ j ⊆ ℝ
20 fvixp2 ⊢ f ∈ ⨉ j ∈ X A ⁡ j A ⁡ j ∧ j ∈ X → f ⁡ j ∈ A ⁡ j A ⁡ j
21 20 adantll ⊢ φ ∧ f ∈ ⨉ j ∈ X A ⁡ j A ⁡ j ∧ j ∈ X → f ⁡ j ∈ A ⁡ j A ⁡ j
22 19 21 sseldd ⊢ φ ∧ f ∈ ⨉ j ∈ X A ⁡ j A ⁡ j ∧ j ∈ X → f ⁡ j ∈ ℝ
23 22 rexrd ⊢ φ ∧ f ∈ ⨉ j ∈ X A ⁡ j A ⁡ j ∧ j ∈ X → f ⁡ j ∈ ℝ *
24 18 rexrd ⊢ φ ∧ f ∈ ⨉ j ∈ X A ⁡ j A ⁡ j ∧ j ∈ X → A ⁡ j ∈ ℝ *
25 iccleub ⊢ A ⁡ j ∈ ℝ * ∧ A ⁡ j ∈ ℝ * ∧ f ⁡ j ∈ A ⁡ j A ⁡ j → f ⁡ j ≤ A ⁡ j
26 24 24 21 25 syl3anc ⊢ φ ∧ f ∈ ⨉ j ∈ X A ⁡ j A ⁡ j ∧ j ∈ X → f ⁡ j ≤ A ⁡ j
27 iccgelb ⊢ A ⁡ j ∈ ℝ * ∧ A ⁡ j ∈ ℝ * ∧ f ⁡ j ∈ A ⁡ j A ⁡ j → A ⁡ j ≤ f ⁡ j
28 24 24 21 27 syl3anc ⊢ φ ∧ f ∈ ⨉ j ∈ X A ⁡ j A ⁡ j ∧ j ∈ X → A ⁡ j ≤ f ⁡ j
29 23 24 26 28 xrletrid ⊢ φ ∧ f ∈ ⨉ j ∈ X A ⁡ j A ⁡ j ∧ j ∈ X → f ⁡ j = A ⁡ j
30 7 13 14 29 syl21anc ⊢ φ ∧ f ∈ ⨉ k ∈ X A ⁡ k A ⁡ k ∧ j ∈ X → f ⁡ j = A ⁡ j
31 3 6 30 eqfnfvd ⊢ φ ∧ f ∈ ⨉ k ∈ X A ⁡ k A ⁡ k → f = A
32 velsn ⊢ f ∈ A ↔ f = A
33 32 bicomi ⊢ f = A ↔ f ∈ A
34 33 biimpi ⊢ f = A → f ∈ A
35 31 34 syl ⊢ φ ∧ f ∈ ⨉ k ∈ X A ⁡ k A ⁡ k → f ∈ A
36 35 ssd ⊢ φ → ⨉ k ∈ X A ⁡ k A ⁡ k ⊆ A
37 1 elexd ⊢ φ → A ∈ V
38 16 ffvelcdmda ⊢ φ ∧ k ∈ X → A ⁡ k ∈ ℝ
39 38 leidd ⊢ φ ∧ k ∈ X → A ⁡ k ≤ A ⁡ k
40 38 38 38 39 39 eliccd ⊢ φ ∧ k ∈ X → A ⁡ k ∈ A ⁡ k A ⁡ k
41 40 ralrimiva ⊢ φ → ∀ k ∈ X A ⁡ k ∈ A ⁡ k A ⁡ k
42 37 5 41 3jca ⊢ φ → A ∈ V ∧ A Fn X ∧ ∀ k ∈ X A ⁡ k ∈ A ⁡ k A ⁡ k
43 elixp2 ⊢ A ∈ ⨉ k ∈ X A ⁡ k A ⁡ k ↔ A ∈ V ∧ A Fn X ∧ ∀ k ∈ X A ⁡ k ∈ A ⁡ k A ⁡ k
44 42 43 sylibr ⊢ φ → A ∈ ⨉ k ∈ X A ⁡ k A ⁡ k
45 snssg ⊢ A ∈ ℝ X → A ∈ ⨉ k ∈ X A ⁡ k A ⁡ k ↔ A ⊆ ⨉ k ∈ X A ⁡ k A ⁡ k
46 1 45 syl ⊢ φ → A ∈ ⨉ k ∈ X A ⁡ k A ⁡ k ↔ A ⊆ ⨉ k ∈ X A ⁡ k A ⁡ k
47 44 46 mpbid ⊢ φ → A ⊆ ⨉ k ∈ X A ⁡ k A ⁡ k
48 36 47 eqssd ⊢ φ → ⨉ k ∈ X A ⁡ k A ⁡ k = A