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 ⊢ ( 𝜑 → 𝐴 ∈ ( ℝ ↑m 𝑋 ) )
Assertion rrxsnicc ( 𝜑 → X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,] ( 𝐴 ‘ 𝑘 ) ) = { 𝐴 } )

Proof

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