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 
|- ( ph -> A e. ( RR ^m X ) )
Assertion rrxsnicc 
|- ( ph -> X_ k e. X ( ( A ` k ) [,] ( A ` k ) ) = { A } )

Proof

Step Hyp Ref Expression
1 rrxsnicc.1 
 |-  ( ph -> A e. ( RR ^m X ) )
2 ixpfn 
 |-  ( f e. X_ k e. X ( ( A ` k ) [,] ( A ` k ) ) -> f Fn X )
3 2 adantl 
 |-  ( ( ph /\ f e. X_ k e. X ( ( A ` k ) [,] ( A ` k ) ) ) -> f Fn X )
4 elmapfn 
 |-  ( A e. ( RR ^m X ) -> A Fn X )
5 1 4 syl 
 |-  ( ph -> A Fn X )
6 5 adantr 
 |-  ( ( ph /\ f e. X_ k e. X ( ( A ` k ) [,] ( A ` k ) ) ) -> A Fn X )
7 simpll 
 |-  ( ( ( ph /\ f e. X_ k e. X ( ( A ` k ) [,] ( A ` k ) ) ) /\ j e. X ) -> ph )
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 
 |-  X_ k e. X ( ( A ` k ) [,] ( A ` k ) ) = X_ j e. X ( ( A ` j ) [,] ( A ` j ) )
11 10 eleq2i 
 |-  ( f e. X_ k e. X ( ( A ` k ) [,] ( A ` k ) ) <-> f e. X_ j e. X ( ( A ` j ) [,] ( A ` j ) ) )
12 11 biimpi 
 |-  ( f e. X_ k e. X ( ( A ` k ) [,] ( A ` k ) ) -> f e. X_ j e. X ( ( A ` j ) [,] ( A ` j ) ) )
13 12 ad2antlr 
 |-  ( ( ( ph /\ f e. X_ k e. X ( ( A ` k ) [,] ( A ` k ) ) ) /\ j e. X ) -> f e. X_ j e. X ( ( A ` j ) [,] ( A ` j ) ) )
14 simpr 
 |-  ( ( ( ph /\ f e. X_ k e. X ( ( A ` k ) [,] ( A ` k ) ) ) /\ j e. X ) -> j e. X )
15 elmapi 
 |-  ( A e. ( RR ^m X ) -> A : X --> RR )
16 1 15 syl 
 |-  ( ph -> A : X --> RR )
17 16 ffvelrnda 
 |-  ( ( ph /\ j e. X ) -> ( A ` j ) e. RR )
18 17 adantlr 
 |-  ( ( ( ph /\ f e. X_ j e. X ( ( A ` j ) [,] ( A ` j ) ) ) /\ j e. X ) -> ( A ` j ) e. RR )
19 18 18 iccssred 
 |-  ( ( ( ph /\ f e. X_ j e. X ( ( A ` j ) [,] ( A ` j ) ) ) /\ j e. X ) -> ( ( A ` j ) [,] ( A ` j ) ) C_ RR )
20 fvixp2 
 |-  ( ( f e. X_ j e. X ( ( A ` j ) [,] ( A ` j ) ) /\ j e. X ) -> ( f ` j ) e. ( ( A ` j ) [,] ( A ` j ) ) )
21 20 adantll 
 |-  ( ( ( ph /\ f e. X_ j e. X ( ( A ` j ) [,] ( A ` j ) ) ) /\ j e. X ) -> ( f ` j ) e. ( ( A ` j ) [,] ( A ` j ) ) )
22 19 21 sseldd 
 |-  ( ( ( ph /\ f e. X_ j e. X ( ( A ` j ) [,] ( A ` j ) ) ) /\ j e. X ) -> ( f ` j ) e. RR )
23 22 rexrd 
 |-  ( ( ( ph /\ f e. X_ j e. X ( ( A ` j ) [,] ( A ` j ) ) ) /\ j e. X ) -> ( f ` j ) e. RR* )
24 18 rexrd 
 |-  ( ( ( ph /\ f e. X_ j e. X ( ( A ` j ) [,] ( A ` j ) ) ) /\ j e. X ) -> ( A ` j ) e. RR* )
25 iccleub 
 |-  ( ( ( A ` j ) e. RR* /\ ( A ` j ) e. RR* /\ ( f ` j ) e. ( ( A ` j ) [,] ( A ` j ) ) ) -> ( f ` j ) <_ ( A ` j ) )
26 24 24 21 25 syl3anc 
 |-  ( ( ( ph /\ f e. X_ j e. X ( ( A ` j ) [,] ( A ` j ) ) ) /\ j e. X ) -> ( f ` j ) <_ ( A ` j ) )
27 iccgelb 
 |-  ( ( ( A ` j ) e. RR* /\ ( A ` j ) e. RR* /\ ( f ` j ) e. ( ( A ` j ) [,] ( A ` j ) ) ) -> ( A ` j ) <_ ( f ` j ) )
28 24 24 21 27 syl3anc 
 |-  ( ( ( ph /\ f e. X_ j e. X ( ( A ` j ) [,] ( A ` j ) ) ) /\ j e. X ) -> ( A ` j ) <_ ( f ` j ) )
29 23 24 26 28 xrletrid 
 |-  ( ( ( ph /\ f e. X_ j e. X ( ( A ` j ) [,] ( A ` j ) ) ) /\ j e. X ) -> ( f ` j ) = ( A ` j ) )
30 7 13 14 29 syl21anc 
 |-  ( ( ( ph /\ f e. X_ k e. X ( ( A ` k ) [,] ( A ` k ) ) ) /\ j e. X ) -> ( f ` j ) = ( A ` j ) )
31 3 6 30 eqfnfvd 
 |-  ( ( ph /\ f e. X_ k e. X ( ( A ` k ) [,] ( A ` k ) ) ) -> f = A )
32 velsn 
 |-  ( f e. { A } <-> f = A )
33 32 bicomi 
 |-  ( f = A <-> f e. { A } )
34 33 biimpi 
 |-  ( f = A -> f e. { A } )
35 31 34 syl 
 |-  ( ( ph /\ f e. X_ k e. X ( ( A ` k ) [,] ( A ` k ) ) ) -> f e. { A } )
36 35 ssd 
 |-  ( ph -> X_ k e. X ( ( A ` k ) [,] ( A ` k ) ) C_ { A } )
37 1 elexd 
 |-  ( ph -> A e. _V )
38 16 ffvelrnda 
 |-  ( ( ph /\ k e. X ) -> ( A ` k ) e. RR )
39 38 leidd 
 |-  ( ( ph /\ k e. X ) -> ( A ` k ) <_ ( A ` k ) )
40 38 38 38 39 39 eliccd 
 |-  ( ( ph /\ k e. X ) -> ( A ` k ) e. ( ( A ` k ) [,] ( A ` k ) ) )
41 40 ralrimiva 
 |-  ( ph -> A. k e. X ( A ` k ) e. ( ( A ` k ) [,] ( A ` k ) ) )
42 37 5 41 3jca 
 |-  ( ph -> ( A e. _V /\ A Fn X /\ A. k e. X ( A ` k ) e. ( ( A ` k ) [,] ( A ` k ) ) ) )
43 elixp2 
 |-  ( A e. X_ k e. X ( ( A ` k ) [,] ( A ` k ) ) <-> ( A e. _V /\ A Fn X /\ A. k e. X ( A ` k ) e. ( ( A ` k ) [,] ( A ` k ) ) ) )
44 42 43 sylibr 
 |-  ( ph -> A e. X_ k e. X ( ( A ` k ) [,] ( A ` k ) ) )
45 snssg 
 |-  ( A e. ( RR ^m X ) -> ( A e. X_ k e. X ( ( A ` k ) [,] ( A ` k ) ) <-> { A } C_ X_ k e. X ( ( A ` k ) [,] ( A ` k ) ) ) )
46 1 45 syl 
 |-  ( ph -> ( A e. X_ k e. X ( ( A ` k ) [,] ( A ` k ) ) <-> { A } C_ X_ k e. X ( ( A ` k ) [,] ( A ` k ) ) ) )
47 44 46 mpbid 
 |-  ( ph -> { A } C_ X_ k e. X ( ( A ` k ) [,] ( A ` k ) ) )
48 36 47 eqssd 
 |-  ( ph -> X_ k e. X ( ( A ` k ) [,] ( A ` k ) ) = { A } )