Metamath Proof Explorer

Theorem ismtyima

Description: The image of a ball under an isometry is another ball. (Contributed by Jeff Madsen, 31-Jan-2014)

Ref Expression
Assertion ismtyima ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) β†’ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝑀 ) 𝑅 ) ) = ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝑁 ) 𝑅 ) )

Proof

Step Hyp Ref Expression
1 imassrn ⊒ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝑀 ) 𝑅 ) ) βŠ† ran 𝐹
2 isismty ⊒ ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ) β†’ ( 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ↔ ( 𝐹 : 𝑋 –1-1-ontoβ†’ π‘Œ ∧ βˆ€ π‘₯ ∈ 𝑋 βˆ€ 𝑦 ∈ 𝑋 ( π‘₯ 𝑀 𝑦 ) = ( ( 𝐹 β€˜ π‘₯ ) 𝑁 ( 𝐹 β€˜ 𝑦 ) ) ) ) )
3 2 biimp3a ⊒ ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) β†’ ( 𝐹 : 𝑋 –1-1-ontoβ†’ π‘Œ ∧ βˆ€ π‘₯ ∈ 𝑋 βˆ€ 𝑦 ∈ 𝑋 ( π‘₯ 𝑀 𝑦 ) = ( ( 𝐹 β€˜ π‘₯ ) 𝑁 ( 𝐹 β€˜ 𝑦 ) ) ) )
4 3 adantr ⊒ ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) β†’ ( 𝐹 : 𝑋 –1-1-ontoβ†’ π‘Œ ∧ βˆ€ π‘₯ ∈ 𝑋 βˆ€ 𝑦 ∈ 𝑋 ( π‘₯ 𝑀 𝑦 ) = ( ( 𝐹 β€˜ π‘₯ ) 𝑁 ( 𝐹 β€˜ 𝑦 ) ) ) )
5 4 simpld ⊒ ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) β†’ 𝐹 : 𝑋 –1-1-ontoβ†’ π‘Œ )
6 f1of ⊒ ( 𝐹 : 𝑋 –1-1-ontoβ†’ π‘Œ β†’ 𝐹 : 𝑋 ⟢ π‘Œ )
7 5 6 syl ⊒ ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) β†’ 𝐹 : 𝑋 ⟢ π‘Œ )
8 7 frnd ⊒ ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) β†’ ran 𝐹 βŠ† π‘Œ )
9 1 8 sstrid ⊒ ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) β†’ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝑀 ) 𝑅 ) ) βŠ† π‘Œ )
10 9 sseld ⊒ ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) β†’ ( π‘₯ ∈ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝑀 ) 𝑅 ) ) β†’ π‘₯ ∈ π‘Œ ) )
11 simpl2 ⊒ ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) β†’ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) )
12 simprl ⊒ ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) β†’ 𝑃 ∈ 𝑋 )
13 ffvelcdm ⊒ ( ( 𝐹 : 𝑋 ⟢ π‘Œ ∧ 𝑃 ∈ 𝑋 ) β†’ ( 𝐹 β€˜ 𝑃 ) ∈ π‘Œ )
14 7 12 13 syl2anc ⊒ ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) β†’ ( 𝐹 β€˜ 𝑃 ) ∈ π‘Œ )
15 simprr ⊒ ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) β†’ 𝑅 ∈ ℝ* )
16 blssm ⊒ ( ( 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ ( 𝐹 β€˜ 𝑃 ) ∈ π‘Œ ∧ 𝑅 ∈ ℝ* ) β†’ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝑁 ) 𝑅 ) βŠ† π‘Œ )
17 11 14 15 16 syl3anc ⊒ ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) β†’ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝑁 ) 𝑅 ) βŠ† π‘Œ )
18 17 sseld ⊒ ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) β†’ ( π‘₯ ∈ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝑁 ) 𝑅 ) β†’ π‘₯ ∈ π‘Œ ) )
19 simpl1 ⊒ ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) β†’ 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) )
20 19 adantr ⊒ ( ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ π‘₯ ∈ π‘Œ ) β†’ 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) )
21 simplrr ⊒ ( ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ π‘₯ ∈ π‘Œ ) β†’ 𝑅 ∈ ℝ* )
22 simplrl ⊒ ( ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ π‘₯ ∈ π‘Œ ) β†’ 𝑃 ∈ 𝑋 )
23 f1ocnv ⊒ ( 𝐹 : 𝑋 –1-1-ontoβ†’ π‘Œ β†’ β—‘ 𝐹 : π‘Œ –1-1-ontoβ†’ 𝑋 )
24 f1of ⊒ ( β—‘ 𝐹 : π‘Œ –1-1-ontoβ†’ 𝑋 β†’ β—‘ 𝐹 : π‘Œ ⟢ 𝑋 )
25 5 23 24 3syl ⊒ ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) β†’ β—‘ 𝐹 : π‘Œ ⟢ 𝑋 )
26 ffvelcdm ⊒ ( ( β—‘ 𝐹 : π‘Œ ⟢ 𝑋 ∧ π‘₯ ∈ π‘Œ ) β†’ ( β—‘ 𝐹 β€˜ π‘₯ ) ∈ 𝑋 )
27 25 26 sylan ⊒ ( ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ π‘₯ ∈ π‘Œ ) β†’ ( β—‘ 𝐹 β€˜ π‘₯ ) ∈ 𝑋 )
28 elbl2 ⊒ ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑅 ∈ ℝ* ) ∧ ( 𝑃 ∈ 𝑋 ∧ ( β—‘ 𝐹 β€˜ π‘₯ ) ∈ 𝑋 ) ) β†’ ( ( β—‘ 𝐹 β€˜ π‘₯ ) ∈ ( 𝑃 ( ball β€˜ 𝑀 ) 𝑅 ) ↔ ( 𝑃 𝑀 ( β—‘ 𝐹 β€˜ π‘₯ ) ) < 𝑅 ) )
29 20 21 22 27 28 syl22anc ⊒ ( ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ π‘₯ ∈ π‘Œ ) β†’ ( ( β—‘ 𝐹 β€˜ π‘₯ ) ∈ ( 𝑃 ( ball β€˜ 𝑀 ) 𝑅 ) ↔ ( 𝑃 𝑀 ( β—‘ 𝐹 β€˜ π‘₯ ) ) < 𝑅 ) )
30 4 simprd ⊒ ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) β†’ βˆ€ π‘₯ ∈ 𝑋 βˆ€ 𝑦 ∈ 𝑋 ( π‘₯ 𝑀 𝑦 ) = ( ( 𝐹 β€˜ π‘₯ ) 𝑁 ( 𝐹 β€˜ 𝑦 ) ) )
31 oveq1 ⊒ ( π‘₯ = 𝑃 β†’ ( π‘₯ 𝑀 𝑦 ) = ( 𝑃 𝑀 𝑦 ) )
32 fveq2 ⊒ ( π‘₯ = 𝑃 β†’ ( 𝐹 β€˜ π‘₯ ) = ( 𝐹 β€˜ 𝑃 ) )
33 32 oveq1d ⊒ ( π‘₯ = 𝑃 β†’ ( ( 𝐹 β€˜ π‘₯ ) 𝑁 ( 𝐹 β€˜ 𝑦 ) ) = ( ( 𝐹 β€˜ 𝑃 ) 𝑁 ( 𝐹 β€˜ 𝑦 ) ) )
34 31 33 eqeq12d ⊒ ( π‘₯ = 𝑃 β†’ ( ( π‘₯ 𝑀 𝑦 ) = ( ( 𝐹 β€˜ π‘₯ ) 𝑁 ( 𝐹 β€˜ 𝑦 ) ) ↔ ( 𝑃 𝑀 𝑦 ) = ( ( 𝐹 β€˜ 𝑃 ) 𝑁 ( 𝐹 β€˜ 𝑦 ) ) ) )
35 oveq2 ⊒ ( 𝑦 = ( β—‘ 𝐹 β€˜ π‘₯ ) β†’ ( 𝑃 𝑀 𝑦 ) = ( 𝑃 𝑀 ( β—‘ 𝐹 β€˜ π‘₯ ) ) )
36 fveq2 ⊒ ( 𝑦 = ( β—‘ 𝐹 β€˜ π‘₯ ) β†’ ( 𝐹 β€˜ 𝑦 ) = ( 𝐹 β€˜ ( β—‘ 𝐹 β€˜ π‘₯ ) ) )
37 36 oveq2d ⊒ ( 𝑦 = ( β—‘ 𝐹 β€˜ π‘₯ ) β†’ ( ( 𝐹 β€˜ 𝑃 ) 𝑁 ( 𝐹 β€˜ 𝑦 ) ) = ( ( 𝐹 β€˜ 𝑃 ) 𝑁 ( 𝐹 β€˜ ( β—‘ 𝐹 β€˜ π‘₯ ) ) ) )
38 35 37 eqeq12d ⊒ ( 𝑦 = ( β—‘ 𝐹 β€˜ π‘₯ ) β†’ ( ( 𝑃 𝑀 𝑦 ) = ( ( 𝐹 β€˜ 𝑃 ) 𝑁 ( 𝐹 β€˜ 𝑦 ) ) ↔ ( 𝑃 𝑀 ( β—‘ 𝐹 β€˜ π‘₯ ) ) = ( ( 𝐹 β€˜ 𝑃 ) 𝑁 ( 𝐹 β€˜ ( β—‘ 𝐹 β€˜ π‘₯ ) ) ) ) )
39 34 38 rspc2v ⊒ ( ( 𝑃 ∈ 𝑋 ∧ ( β—‘ 𝐹 β€˜ π‘₯ ) ∈ 𝑋 ) β†’ ( βˆ€ π‘₯ ∈ 𝑋 βˆ€ 𝑦 ∈ 𝑋 ( π‘₯ 𝑀 𝑦 ) = ( ( 𝐹 β€˜ π‘₯ ) 𝑁 ( 𝐹 β€˜ 𝑦 ) ) β†’ ( 𝑃 𝑀 ( β—‘ 𝐹 β€˜ π‘₯ ) ) = ( ( 𝐹 β€˜ 𝑃 ) 𝑁 ( 𝐹 β€˜ ( β—‘ 𝐹 β€˜ π‘₯ ) ) ) ) )
40 39 impancom ⊒ ( ( 𝑃 ∈ 𝑋 ∧ βˆ€ π‘₯ ∈ 𝑋 βˆ€ 𝑦 ∈ 𝑋 ( π‘₯ 𝑀 𝑦 ) = ( ( 𝐹 β€˜ π‘₯ ) 𝑁 ( 𝐹 β€˜ 𝑦 ) ) ) β†’ ( ( β—‘ 𝐹 β€˜ π‘₯ ) ∈ 𝑋 β†’ ( 𝑃 𝑀 ( β—‘ 𝐹 β€˜ π‘₯ ) ) = ( ( 𝐹 β€˜ 𝑃 ) 𝑁 ( 𝐹 β€˜ ( β—‘ 𝐹 β€˜ π‘₯ ) ) ) ) )
41 12 30 40 syl2anc ⊒ ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) β†’ ( ( β—‘ 𝐹 β€˜ π‘₯ ) ∈ 𝑋 β†’ ( 𝑃 𝑀 ( β—‘ 𝐹 β€˜ π‘₯ ) ) = ( ( 𝐹 β€˜ 𝑃 ) 𝑁 ( 𝐹 β€˜ ( β—‘ 𝐹 β€˜ π‘₯ ) ) ) ) )
42 41 imp ⊒ ( ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ ( β—‘ 𝐹 β€˜ π‘₯ ) ∈ 𝑋 ) β†’ ( 𝑃 𝑀 ( β—‘ 𝐹 β€˜ π‘₯ ) ) = ( ( 𝐹 β€˜ 𝑃 ) 𝑁 ( 𝐹 β€˜ ( β—‘ 𝐹 β€˜ π‘₯ ) ) ) )
43 27 42 syldan ⊒ ( ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ π‘₯ ∈ π‘Œ ) β†’ ( 𝑃 𝑀 ( β—‘ 𝐹 β€˜ π‘₯ ) ) = ( ( 𝐹 β€˜ 𝑃 ) 𝑁 ( 𝐹 β€˜ ( β—‘ 𝐹 β€˜ π‘₯ ) ) ) )
44 43 breq1d ⊒ ( ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ π‘₯ ∈ π‘Œ ) β†’ ( ( 𝑃 𝑀 ( β—‘ 𝐹 β€˜ π‘₯ ) ) < 𝑅 ↔ ( ( 𝐹 β€˜ 𝑃 ) 𝑁 ( 𝐹 β€˜ ( β—‘ 𝐹 β€˜ π‘₯ ) ) ) < 𝑅 ) )
45 29 44 bitrd ⊒ ( ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ π‘₯ ∈ π‘Œ ) β†’ ( ( β—‘ 𝐹 β€˜ π‘₯ ) ∈ ( 𝑃 ( ball β€˜ 𝑀 ) 𝑅 ) ↔ ( ( 𝐹 β€˜ 𝑃 ) 𝑁 ( 𝐹 β€˜ ( β—‘ 𝐹 β€˜ π‘₯ ) ) ) < 𝑅 ) )
46 f1of1 ⊒ ( 𝐹 : 𝑋 –1-1-ontoβ†’ π‘Œ β†’ 𝐹 : 𝑋 –1-1β†’ π‘Œ )
47 5 46 syl ⊒ ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) β†’ 𝐹 : 𝑋 –1-1β†’ π‘Œ )
48 47 adantr ⊒ ( ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ π‘₯ ∈ π‘Œ ) β†’ 𝐹 : 𝑋 –1-1β†’ π‘Œ )
49 blssm ⊒ ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) β†’ ( 𝑃 ( ball β€˜ 𝑀 ) 𝑅 ) βŠ† 𝑋 )
50 19 12 15 49 syl3anc ⊒ ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) β†’ ( 𝑃 ( ball β€˜ 𝑀 ) 𝑅 ) βŠ† 𝑋 )
51 50 adantr ⊒ ( ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ π‘₯ ∈ π‘Œ ) β†’ ( 𝑃 ( ball β€˜ 𝑀 ) 𝑅 ) βŠ† 𝑋 )
52 f1elima ⊒ ( ( 𝐹 : 𝑋 –1-1β†’ π‘Œ ∧ ( β—‘ 𝐹 β€˜ π‘₯ ) ∈ 𝑋 ∧ ( 𝑃 ( ball β€˜ 𝑀 ) 𝑅 ) βŠ† 𝑋 ) β†’ ( ( 𝐹 β€˜ ( β—‘ 𝐹 β€˜ π‘₯ ) ) ∈ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝑀 ) 𝑅 ) ) ↔ ( β—‘ 𝐹 β€˜ π‘₯ ) ∈ ( 𝑃 ( ball β€˜ 𝑀 ) 𝑅 ) ) )
53 48 27 51 52 syl3anc ⊒ ( ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ π‘₯ ∈ π‘Œ ) β†’ ( ( 𝐹 β€˜ ( β—‘ 𝐹 β€˜ π‘₯ ) ) ∈ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝑀 ) 𝑅 ) ) ↔ ( β—‘ 𝐹 β€˜ π‘₯ ) ∈ ( 𝑃 ( ball β€˜ 𝑀 ) 𝑅 ) ) )
54 11 adantr ⊒ ( ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ π‘₯ ∈ π‘Œ ) β†’ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) )
55 14 adantr ⊒ ( ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ π‘₯ ∈ π‘Œ ) β†’ ( 𝐹 β€˜ 𝑃 ) ∈ π‘Œ )
56 f1ocnvfv2 ⊒ ( ( 𝐹 : 𝑋 –1-1-ontoβ†’ π‘Œ ∧ π‘₯ ∈ π‘Œ ) β†’ ( 𝐹 β€˜ ( β—‘ 𝐹 β€˜ π‘₯ ) ) = π‘₯ )
57 5 56 sylan ⊒ ( ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ π‘₯ ∈ π‘Œ ) β†’ ( 𝐹 β€˜ ( β—‘ 𝐹 β€˜ π‘₯ ) ) = π‘₯ )
58 simpr ⊒ ( ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ π‘₯ ∈ π‘Œ ) β†’ π‘₯ ∈ π‘Œ )
59 57 58 eqeltrd ⊒ ( ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ π‘₯ ∈ π‘Œ ) β†’ ( 𝐹 β€˜ ( β—‘ 𝐹 β€˜ π‘₯ ) ) ∈ π‘Œ )
60 elbl2 ⊒ ( ( ( 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑅 ∈ ℝ* ) ∧ ( ( 𝐹 β€˜ 𝑃 ) ∈ π‘Œ ∧ ( 𝐹 β€˜ ( β—‘ 𝐹 β€˜ π‘₯ ) ) ∈ π‘Œ ) ) β†’ ( ( 𝐹 β€˜ ( β—‘ 𝐹 β€˜ π‘₯ ) ) ∈ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝑁 ) 𝑅 ) ↔ ( ( 𝐹 β€˜ 𝑃 ) 𝑁 ( 𝐹 β€˜ ( β—‘ 𝐹 β€˜ π‘₯ ) ) ) < 𝑅 ) )
61 54 21 55 59 60 syl22anc ⊒ ( ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ π‘₯ ∈ π‘Œ ) β†’ ( ( 𝐹 β€˜ ( β—‘ 𝐹 β€˜ π‘₯ ) ) ∈ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝑁 ) 𝑅 ) ↔ ( ( 𝐹 β€˜ 𝑃 ) 𝑁 ( 𝐹 β€˜ ( β—‘ 𝐹 β€˜ π‘₯ ) ) ) < 𝑅 ) )
62 45 53 61 3bitr4d ⊒ ( ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ π‘₯ ∈ π‘Œ ) β†’ ( ( 𝐹 β€˜ ( β—‘ 𝐹 β€˜ π‘₯ ) ) ∈ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝑀 ) 𝑅 ) ) ↔ ( 𝐹 β€˜ ( β—‘ 𝐹 β€˜ π‘₯ ) ) ∈ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝑁 ) 𝑅 ) ) )
63 57 eleq1d ⊒ ( ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ π‘₯ ∈ π‘Œ ) β†’ ( ( 𝐹 β€˜ ( β—‘ 𝐹 β€˜ π‘₯ ) ) ∈ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝑀 ) 𝑅 ) ) ↔ π‘₯ ∈ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝑀 ) 𝑅 ) ) ) )
64 57 eleq1d ⊒ ( ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ π‘₯ ∈ π‘Œ ) β†’ ( ( 𝐹 β€˜ ( β—‘ 𝐹 β€˜ π‘₯ ) ) ∈ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝑁 ) 𝑅 ) ↔ π‘₯ ∈ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝑁 ) 𝑅 ) ) )
65 62 63 64 3bitr3d ⊒ ( ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ π‘₯ ∈ π‘Œ ) β†’ ( π‘₯ ∈ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝑀 ) 𝑅 ) ) ↔ π‘₯ ∈ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝑁 ) 𝑅 ) ) )
66 65 ex ⊒ ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) β†’ ( π‘₯ ∈ π‘Œ β†’ ( π‘₯ ∈ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝑀 ) 𝑅 ) ) ↔ π‘₯ ∈ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝑁 ) 𝑅 ) ) ) )
67 10 18 66 pm5.21ndd ⊒ ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) β†’ ( π‘₯ ∈ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝑀 ) 𝑅 ) ) ↔ π‘₯ ∈ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝑁 ) 𝑅 ) ) )
68 67 eqrdv ⊒ ( ( ( 𝑀 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) β†’ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝑀 ) 𝑅 ) ) = ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝑁 ) 𝑅 ) )