Metamath Proof Explorer

Theorem ismrer1

Description: An isometry between RR and RR ^ 1 . (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 22-Sep-2015)

Ref Expression
Hypotheses ismrer1.1 ⊢ 𝑅 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
ismrer1.2 ⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( { 𝐴 } × { 𝑥 } ) )
Assertion ismrer1 ( 𝐴 ∈ 𝑉 → 𝐹 ∈ ( 𝑅 Ismty ( ℝn ‘ { 𝐴 } ) ) )

Proof

Step Hyp Ref Expression
1 ismrer1.1 ⊢ 𝑅 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
2 ismrer1.2 ⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( { 𝐴 } × { 𝑥 } ) )
3 sneq ⊢ ( 𝑦 = 𝐴 → { 𝑦 } = { 𝐴 } )
4 3 xpeq1d ⊢ ( 𝑦 = 𝐴 → ( { 𝑦 } × { 𝑥 } ) = ( { 𝐴 } × { 𝑥 } ) )
5 4 mpteq2dv ⊢ ( 𝑦 = 𝐴 → ( 𝑥 ∈ ℝ ↦ ( { 𝑦 } × { 𝑥 } ) ) = ( 𝑥 ∈ ℝ ↦ ( { 𝐴 } × { 𝑥 } ) ) )
6 5 2 eqtr4di ⊢ ( 𝑦 = 𝐴 → ( 𝑥 ∈ ℝ ↦ ( { 𝑦 } × { 𝑥 } ) ) = 𝐹 )
7 f1oeq1 ⊢ ( ( 𝑥 ∈ ℝ ↦ ( { 𝑦 } × { 𝑥 } ) ) = 𝐹 → ( ( 𝑥 ∈ ℝ ↦ ( { 𝑦 } × { 𝑥 } ) ) : ℝ –1-1-onto→ ( ℝ ↑m { 𝑦 } ) ↔ 𝐹 : ℝ –1-1-onto→ ( ℝ ↑m { 𝑦 } ) ) )
8 6 7 syl ⊢ ( 𝑦 = 𝐴 → ( ( 𝑥 ∈ ℝ ↦ ( { 𝑦 } × { 𝑥 } ) ) : ℝ –1-1-onto→ ( ℝ ↑m { 𝑦 } ) ↔ 𝐹 : ℝ –1-1-onto→ ( ℝ ↑m { 𝑦 } ) ) )
9 3 oveq2d ⊢ ( 𝑦 = 𝐴 → ( ℝ ↑m { 𝑦 } ) = ( ℝ ↑m { 𝐴 } ) )
10 f1oeq3 ⊢ ( ( ℝ ↑m { 𝑦 } ) = ( ℝ ↑m { 𝐴 } ) → ( 𝐹 : ℝ –1-1-onto→ ( ℝ ↑m { 𝑦 } ) ↔ 𝐹 : ℝ –1-1-onto→ ( ℝ ↑m { 𝐴 } ) ) )
11 9 10 syl ⊢ ( 𝑦 = 𝐴 → ( 𝐹 : ℝ –1-1-onto→ ( ℝ ↑m { 𝑦 } ) ↔ 𝐹 : ℝ –1-1-onto→ ( ℝ ↑m { 𝐴 } ) ) )
12 8 11 bitrd ⊢ ( 𝑦 = 𝐴 → ( ( 𝑥 ∈ ℝ ↦ ( { 𝑦 } × { 𝑥 } ) ) : ℝ –1-1-onto→ ( ℝ ↑m { 𝑦 } ) ↔ 𝐹 : ℝ –1-1-onto→ ( ℝ ↑m { 𝐴 } ) ) )
13 eqid ⊢ { 𝑦 } = { 𝑦 }
14 reex ⊢ ℝ ∈ V
15 vex ⊢ 𝑦 ∈ V
16 eqid ⊢ ( 𝑥 ∈ ℝ ↦ ( { 𝑦 } × { 𝑥 } ) ) = ( 𝑥 ∈ ℝ ↦ ( { 𝑦 } × { 𝑥 } ) )
17 13 14 15 16 mapsnf1o3 ⊢ ( 𝑥 ∈ ℝ ↦ ( { 𝑦 } × { 𝑥 } ) ) : ℝ –1-1-onto→ ( ℝ ↑m { 𝑦 } )
18 12 17 vtoclg ⊢ ( 𝐴 ∈ 𝑉 → 𝐹 : ℝ –1-1-onto→ ( ℝ ↑m { 𝐴 } ) )
19 sneq ⊢ ( 𝑥 = 𝑦 → { 𝑥 } = { 𝑦 } )
20 19 xpeq2d ⊢ ( 𝑥 = 𝑦 → ( { 𝐴 } × { 𝑥 } ) = ( { 𝐴 } × { 𝑦 } ) )
21 snex ⊢ { 𝐴 } ∈ V
22 snex ⊢ { 𝑥 } ∈ V
23 21 22 xpex ⊢ ( { 𝐴 } × { 𝑥 } ) ∈ V
24 20 2 23 fvmpt3i ⊢ ( 𝑦 ∈ ℝ → ( 𝐹 ‘ 𝑦 ) = ( { 𝐴 } × { 𝑦 } ) )
25 24 fveq1d ⊢ ( 𝑦 ∈ ℝ → ( ( 𝐹 ‘ 𝑦 ) ‘ 𝐴 ) = ( ( { 𝐴 } × { 𝑦 } ) ‘ 𝐴 ) )
26 25 adantr ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑦 ) ‘ 𝐴 ) = ( ( { 𝐴 } × { 𝑦 } ) ‘ 𝐴 ) )
27 snidg ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 } )
28 fvconst2g ⊢ ( ( 𝑦 ∈ V ∧ 𝐴 ∈ { 𝐴 } ) → ( ( { 𝐴 } × { 𝑦 } ) ‘ 𝐴 ) = 𝑦 )
29 15 27 28 sylancr ⊢ ( 𝐴 ∈ 𝑉 → ( ( { 𝐴 } × { 𝑦 } ) ‘ 𝐴 ) = 𝑦 )
30 26 29 sylan9eqr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( ( 𝐹 ‘ 𝑦 ) ‘ 𝐴 ) = 𝑦 )
31 sneq ⊢ ( 𝑥 = 𝑧 → { 𝑥 } = { 𝑧 } )
32 31 xpeq2d ⊢ ( 𝑥 = 𝑧 → ( { 𝐴 } × { 𝑥 } ) = ( { 𝐴 } × { 𝑧 } ) )
33 32 2 23 fvmpt3i ⊢ ( 𝑧 ∈ ℝ → ( 𝐹 ‘ 𝑧 ) = ( { 𝐴 } × { 𝑧 } ) )
34 33 fveq1d ⊢ ( 𝑧 ∈ ℝ → ( ( 𝐹 ‘ 𝑧 ) ‘ 𝐴 ) = ( ( { 𝐴 } × { 𝑧 } ) ‘ 𝐴 ) )
35 34 adantl ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑧 ) ‘ 𝐴 ) = ( ( { 𝐴 } × { 𝑧 } ) ‘ 𝐴 ) )
36 vex ⊢ 𝑧 ∈ V
37 fvconst2g ⊢ ( ( 𝑧 ∈ V ∧ 𝐴 ∈ { 𝐴 } ) → ( ( { 𝐴 } × { 𝑧 } ) ‘ 𝐴 ) = 𝑧 )
38 36 27 37 sylancr ⊢ ( 𝐴 ∈ 𝑉 → ( ( { 𝐴 } × { 𝑧 } ) ‘ 𝐴 ) = 𝑧 )
39 35 38 sylan9eqr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( ( 𝐹 ‘ 𝑧 ) ‘ 𝐴 ) = 𝑧 )
40 30 39 oveq12d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( ( ( 𝐹 ‘ 𝑦 ) ‘ 𝐴 ) − ( ( 𝐹 ‘ 𝑧 ) ‘ 𝐴 ) ) = ( 𝑦 − 𝑧 ) )
41 40 oveq1d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( ( ( ( 𝐹 ‘ 𝑦 ) ‘ 𝐴 ) − ( ( 𝐹 ‘ 𝑧 ) ‘ 𝐴 ) ) ↑ 2 ) = ( ( 𝑦 − 𝑧 ) ↑ 2 ) )
42 resubcl ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( 𝑦 − 𝑧 ) ∈ ℝ )
43 42 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( 𝑦 − 𝑧 ) ∈ ℝ )
44 absresq ⊢ ( ( 𝑦 − 𝑧 ) ∈ ℝ → ( ( abs ‘ ( 𝑦 − 𝑧 ) ) ↑ 2 ) = ( ( 𝑦 − 𝑧 ) ↑ 2 ) )
45 43 44 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( ( abs ‘ ( 𝑦 − 𝑧 ) ) ↑ 2 ) = ( ( 𝑦 − 𝑧 ) ↑ 2 ) )
46 41 45 eqtr4d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( ( ( ( 𝐹 ‘ 𝑦 ) ‘ 𝐴 ) − ( ( 𝐹 ‘ 𝑧 ) ‘ 𝐴 ) ) ↑ 2 ) = ( ( abs ‘ ( 𝑦 − 𝑧 ) ) ↑ 2 ) )
47 43 recnd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( 𝑦 − 𝑧 ) ∈ ℂ )
48 47 abscld ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( abs ‘ ( 𝑦 − 𝑧 ) ) ∈ ℝ )
49 48 recnd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( abs ‘ ( 𝑦 − 𝑧 ) ) ∈ ℂ )
50 49 sqcld ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( ( abs ‘ ( 𝑦 − 𝑧 ) ) ↑ 2 ) ∈ ℂ )
51 46 50 eqeltrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( ( ( ( 𝐹 ‘ 𝑦 ) ‘ 𝐴 ) − ( ( 𝐹 ‘ 𝑧 ) ‘ 𝐴 ) ) ↑ 2 ) ∈ ℂ )
52 fveq2 ⊢ ( 𝑘 = 𝐴 → ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑦 ) ‘ 𝐴 ) )
53 fveq2 ⊢ ( 𝑘 = 𝐴 → ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑧 ) ‘ 𝐴 ) )
54 52 53 oveq12d ⊢ ( 𝑘 = 𝐴 → ( ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) − ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑘 ) ) = ( ( ( 𝐹 ‘ 𝑦 ) ‘ 𝐴 ) − ( ( 𝐹 ‘ 𝑧 ) ‘ 𝐴 ) ) )
55 54 oveq1d ⊢ ( 𝑘 = 𝐴 → ( ( ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) − ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑘 ) ) ↑ 2 ) = ( ( ( ( 𝐹 ‘ 𝑦 ) ‘ 𝐴 ) − ( ( 𝐹 ‘ 𝑧 ) ‘ 𝐴 ) ) ↑ 2 ) )
56 55 sumsn ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ( ( ( 𝐹 ‘ 𝑦 ) ‘ 𝐴 ) − ( ( 𝐹 ‘ 𝑧 ) ‘ 𝐴 ) ) ↑ 2 ) ∈ ℂ ) → Σ 𝑘 ∈ { 𝐴 } ( ( ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) − ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑘 ) ) ↑ 2 ) = ( ( ( ( 𝐹 ‘ 𝑦 ) ‘ 𝐴 ) − ( ( 𝐹 ‘ 𝑧 ) ‘ 𝐴 ) ) ↑ 2 ) )
57 51 56 syldan ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → Σ 𝑘 ∈ { 𝐴 } ( ( ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) − ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑘 ) ) ↑ 2 ) = ( ( ( ( 𝐹 ‘ 𝑦 ) ‘ 𝐴 ) − ( ( 𝐹 ‘ 𝑧 ) ‘ 𝐴 ) ) ↑ 2 ) )
58 57 46 eqtrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → Σ 𝑘 ∈ { 𝐴 } ( ( ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) − ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑘 ) ) ↑ 2 ) = ( ( abs ‘ ( 𝑦 − 𝑧 ) ) ↑ 2 ) )
59 58 fveq2d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( √ ‘ Σ 𝑘 ∈ { 𝐴 } ( ( ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) − ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑘 ) ) ↑ 2 ) ) = ( √ ‘ ( ( abs ‘ ( 𝑦 − 𝑧 ) ) ↑ 2 ) ) )
60 47 absge0d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → 0 ≤ ( abs ‘ ( 𝑦 − 𝑧 ) ) )
61 48 60 sqrtsqd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( √ ‘ ( ( abs ‘ ( 𝑦 − 𝑧 ) ) ↑ 2 ) ) = ( abs ‘ ( 𝑦 − 𝑧 ) ) )
62 59 61 eqtrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( √ ‘ Σ 𝑘 ∈ { 𝐴 } ( ( ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) − ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑘 ) ) ↑ 2 ) ) = ( abs ‘ ( 𝑦 − 𝑧 ) ) )
63 f1of ⊢ ( 𝐹 : ℝ –1-1-onto→ ( ℝ ↑m { 𝐴 } ) → 𝐹 : ℝ ⟶ ( ℝ ↑m { 𝐴 } ) )
64 18 63 syl ⊢ ( 𝐴 ∈ 𝑉 → 𝐹 : ℝ ⟶ ( ℝ ↑m { 𝐴 } ) )
65 64 ffvelrnda ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ 𝑦 ) ∈ ( ℝ ↑m { 𝐴 } ) )
66 64 ffvelrnda ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑧 ∈ ℝ ) → ( 𝐹 ‘ 𝑧 ) ∈ ( ℝ ↑m { 𝐴 } ) )
67 65 66 anim12dan ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( ( 𝐹 ‘ 𝑦 ) ∈ ( ℝ ↑m { 𝐴 } ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ℝ ↑m { 𝐴 } ) ) )
68 snfi ⊢ { 𝐴 } ∈ Fin
69 eqid ⊢ ( ℝ ↑m { 𝐴 } ) = ( ℝ ↑m { 𝐴 } )
70 69 rrnmval ⊢ ( ( { 𝐴 } ∈ Fin ∧ ( 𝐹 ‘ 𝑦 ) ∈ ( ℝ ↑m { 𝐴 } ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ℝ ↑m { 𝐴 } ) ) → ( ( 𝐹 ‘ 𝑦 ) ( ℝn ‘ { 𝐴 } ) ( 𝐹 ‘ 𝑧 ) ) = ( √ ‘ Σ 𝑘 ∈ { 𝐴 } ( ( ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) − ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑘 ) ) ↑ 2 ) ) )
71 68 70 mp3an1 ⊢ ( ( ( 𝐹 ‘ 𝑦 ) ∈ ( ℝ ↑m { 𝐴 } ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ℝ ↑m { 𝐴 } ) ) → ( ( 𝐹 ‘ 𝑦 ) ( ℝn ‘ { 𝐴 } ) ( 𝐹 ‘ 𝑧 ) ) = ( √ ‘ Σ 𝑘 ∈ { 𝐴 } ( ( ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) − ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑘 ) ) ↑ 2 ) ) )
72 67 71 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( ( 𝐹 ‘ 𝑦 ) ( ℝn ‘ { 𝐴 } ) ( 𝐹 ‘ 𝑧 ) ) = ( √ ‘ Σ 𝑘 ∈ { 𝐴 } ( ( ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) − ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑘 ) ) ↑ 2 ) ) )
73 1 remetdval ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( 𝑦 𝑅 𝑧 ) = ( abs ‘ ( 𝑦 − 𝑧 ) ) )
74 73 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( 𝑦 𝑅 𝑧 ) = ( abs ‘ ( 𝑦 − 𝑧 ) ) )
75 62 72 74 3eqtr4rd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( 𝑦 𝑅 𝑧 ) = ( ( 𝐹 ‘ 𝑦 ) ( ℝn ‘ { 𝐴 } ) ( 𝐹 ‘ 𝑧 ) ) )
76 75 ralrimivva ⊢ ( 𝐴 ∈ 𝑉 → ∀ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ℝ ( 𝑦 𝑅 𝑧 ) = ( ( 𝐹 ‘ 𝑦 ) ( ℝn ‘ { 𝐴 } ) ( 𝐹 ‘ 𝑧 ) ) )
77 1 rexmet ⊢ 𝑅 ∈ ( ∞Met ‘ ℝ )
78 69 rrnmet ⊢ ( { 𝐴 } ∈ Fin → ( ℝn ‘ { 𝐴 } ) ∈ ( Met ‘ ( ℝ ↑m { 𝐴 } ) ) )
79 metxmet ⊢ ( ( ℝn ‘ { 𝐴 } ) ∈ ( Met ‘ ( ℝ ↑m { 𝐴 } ) ) → ( ℝn ‘ { 𝐴 } ) ∈ ( ∞Met ‘ ( ℝ ↑m { 𝐴 } ) ) )
80 68 78 79 mp2b ⊢ ( ℝn ‘ { 𝐴 } ) ∈ ( ∞Met ‘ ( ℝ ↑m { 𝐴 } ) )
81 isismty ⊢ ( ( 𝑅 ∈ ( ∞Met ‘ ℝ ) ∧ ( ℝn ‘ { 𝐴 } ) ∈ ( ∞Met ‘ ( ℝ ↑m { 𝐴 } ) ) ) → ( 𝐹 ∈ ( 𝑅 Ismty ( ℝn ‘ { 𝐴 } ) ) ↔ ( 𝐹 : ℝ –1-1-onto→ ( ℝ ↑m { 𝐴 } ) ∧ ∀ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ℝ ( 𝑦 𝑅 𝑧 ) = ( ( 𝐹 ‘ 𝑦 ) ( ℝn ‘ { 𝐴 } ) ( 𝐹 ‘ 𝑧 ) ) ) ) )
82 77 80 81 mp2an ⊢ ( 𝐹 ∈ ( 𝑅 Ismty ( ℝn ‘ { 𝐴 } ) ) ↔ ( 𝐹 : ℝ –1-1-onto→ ( ℝ ↑m { 𝐴 } ) ∧ ∀ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ℝ ( 𝑦 𝑅 𝑧 ) = ( ( 𝐹 ‘ 𝑦 ) ( ℝn ‘ { 𝐴 } ) ( 𝐹 ‘ 𝑧 ) ) ) )
83 18 76 82 sylanbrc ⊢ ( 𝐴 ∈ 𝑉 → 𝐹 ∈ ( 𝑅 Ismty ( ℝn ‘ { 𝐴 } ) ) )