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∈XA⁡kA⁡k=A

Proof

Step Hyp Ref Expression
1 rrxsnicc.1 ⊢φ→A∈ℝX
2 ixpfn ⊢f∈⨉k∈XA⁡kA⁡k→fFnX
3 2 adantl ⊢φ∧f∈⨉k∈XA⁡kA⁡k→fFnX
4 elmapfn ⊢A∈ℝX→AFnX
5 1 4 syl ⊢φ→AFnX
6 5 adantr ⊢φ∧f∈⨉k∈XA⁡kA⁡k→AFnX
7 simpll ⊢φ∧f∈⨉k∈XA⁡kA⁡k∧j∈X→φ
8 fveq2 ⊢k=j→A⁡k=A⁡j
9 8 8 oveq12d ⊢k=j→A⁡kA⁡k=A⁡jA⁡j
10 9 cbvixpv ⊢⨉k∈XA⁡kA⁡k=⨉j∈XA⁡jA⁡j
11 10 eleq2i ⊢f∈⨉k∈XA⁡kA⁡k↔f∈⨉j∈XA⁡jA⁡j
12 11 biimpi ⊢f∈⨉k∈XA⁡kA⁡k→f∈⨉j∈XA⁡jA⁡j
13 12 ad2antlr ⊢φ∧f∈⨉k∈XA⁡kA⁡k∧j∈X→f∈⨉j∈XA⁡jA⁡j
14 simpr ⊢φ∧f∈⨉k∈XA⁡kA⁡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∈XA⁡jA⁡j∧j∈X→A⁡j∈ℝ
19 18 18 iccssred ⊢φ∧f∈⨉j∈XA⁡jA⁡j∧j∈X→A⁡jA⁡j⊆ℝ
20 fvixp2 ⊢f∈⨉j∈XA⁡jA⁡j∧j∈X→f⁡j∈A⁡jA⁡j
21 20 adantll ⊢φ∧f∈⨉j∈XA⁡jA⁡j∧j∈X→f⁡j∈A⁡jA⁡j
22 19 21 sseldd ⊢φ∧f∈⨉j∈XA⁡jA⁡j∧j∈X→f⁡j∈ℝ
23 22 rexrd ⊢φ∧f∈⨉j∈XA⁡jA⁡j∧j∈X→f⁡j∈ℝ*
24 18 rexrd ⊢φ∧f∈⨉j∈XA⁡jA⁡j∧j∈X→A⁡j∈ℝ*
25 iccleub ⊢A⁡j∈ℝ*∧A⁡j∈ℝ*∧f⁡j∈A⁡jA⁡j→f⁡j≤A⁡j
26 24 24 21 25 syl3anc ⊢φ∧f∈⨉j∈XA⁡jA⁡j∧j∈X→f⁡j≤A⁡j
27 iccgelb ⊢A⁡j∈ℝ*∧A⁡j∈ℝ*∧f⁡j∈A⁡jA⁡j→A⁡j≤f⁡j
28 24 24 21 27 syl3anc ⊢φ∧f∈⨉j∈XA⁡jA⁡j∧j∈X→A⁡j≤f⁡j
29 23 24 26 28 xrletrid ⊢φ∧f∈⨉j∈XA⁡jA⁡j∧j∈X→f⁡j=A⁡j
30 7 13 14 29 syl21anc ⊢φ∧f∈⨉k∈XA⁡kA⁡k∧j∈X→f⁡j=A⁡j
31 3 6 30 eqfnfvd ⊢φ∧f∈⨉k∈XA⁡kA⁡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∈XA⁡kA⁡k→f∈A
36 35 ssd ⊢φ→⨉k∈XA⁡kA⁡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⁡kA⁡k
41 40 ralrimiva ⊢φ→∀k∈XA⁡k∈A⁡kA⁡k
42 37 5 41 3jca ⊢φ→A∈V∧AFnX∧∀k∈XA⁡k∈A⁡kA⁡k
43 elixp2 ⊢A∈⨉k∈XA⁡kA⁡k↔A∈V∧AFnX∧∀k∈XA⁡k∈A⁡kA⁡k
44 42 43 sylibr ⊢φ→A∈⨉k∈XA⁡kA⁡k
45 snssg ⊢A∈ℝX→A∈⨉k∈XA⁡kA⁡k↔A⊆⨉k∈XA⁡kA⁡k
46 1 45 syl ⊢φ→A∈⨉k∈XA⁡kA⁡k↔A⊆⨉k∈XA⁡kA⁡k
47 44 46 mpbid ⊢φ→A⊆⨉k∈XA⁡kA⁡k
48 36 47 eqssd ⊢φ→⨉k∈XA⁡kA⁡k=A