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 ffvelrnda φ 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 ffvelrnda φ 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