Metamath Proof Explorer


Definition df-ismty

Description: Define a function which takes two metric spaces and returns the set of isometries between the spaces. An isometry is a bijection which preserves distance. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion df-ismty Ismty = ( 𝑚 ran ∞Met , 𝑛 ran ∞Met ↦ { 𝑓 ∣ ( 𝑓 : dom dom 𝑚1-1-onto→ dom dom 𝑛 ∧ ∀ 𝑥 ∈ dom dom 𝑚𝑦 ∈ dom dom 𝑚 ( 𝑥 𝑚 𝑦 ) = ( ( 𝑓𝑥 ) 𝑛 ( 𝑓𝑦 ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cismty Ismty
1 vm 𝑚
2 cxmet ∞Met
3 2 crn ran ∞Met
4 3 cuni ran ∞Met
5 vn 𝑛
6 vf 𝑓
7 6 cv 𝑓
8 1 cv 𝑚
9 8 cdm dom 𝑚
10 9 cdm dom dom 𝑚
11 5 cv 𝑛
12 11 cdm dom 𝑛
13 12 cdm dom dom 𝑛
14 10 13 7 wf1o 𝑓 : dom dom 𝑚1-1-onto→ dom dom 𝑛
15 vx 𝑥
16 vy 𝑦
17 15 cv 𝑥
18 16 cv 𝑦
19 17 18 8 co ( 𝑥 𝑚 𝑦 )
20 17 7 cfv ( 𝑓𝑥 )
21 18 7 cfv ( 𝑓𝑦 )
22 20 21 11 co ( ( 𝑓𝑥 ) 𝑛 ( 𝑓𝑦 ) )
23 19 22 wceq ( 𝑥 𝑚 𝑦 ) = ( ( 𝑓𝑥 ) 𝑛 ( 𝑓𝑦 ) )
24 23 16 10 wral 𝑦 ∈ dom dom 𝑚 ( 𝑥 𝑚 𝑦 ) = ( ( 𝑓𝑥 ) 𝑛 ( 𝑓𝑦 ) )
25 24 15 10 wral 𝑥 ∈ dom dom 𝑚𝑦 ∈ dom dom 𝑚 ( 𝑥 𝑚 𝑦 ) = ( ( 𝑓𝑥 ) 𝑛 ( 𝑓𝑦 ) )
26 14 25 wa ( 𝑓 : dom dom 𝑚1-1-onto→ dom dom 𝑛 ∧ ∀ 𝑥 ∈ dom dom 𝑚𝑦 ∈ dom dom 𝑚 ( 𝑥 𝑚 𝑦 ) = ( ( 𝑓𝑥 ) 𝑛 ( 𝑓𝑦 ) ) )
27 26 6 cab { 𝑓 ∣ ( 𝑓 : dom dom 𝑚1-1-onto→ dom dom 𝑛 ∧ ∀ 𝑥 ∈ dom dom 𝑚𝑦 ∈ dom dom 𝑚 ( 𝑥 𝑚 𝑦 ) = ( ( 𝑓𝑥 ) 𝑛 ( 𝑓𝑦 ) ) ) }
28 1 5 4 4 27 cmpo ( 𝑚 ran ∞Met , 𝑛 ran ∞Met ↦ { 𝑓 ∣ ( 𝑓 : dom dom 𝑚1-1-onto→ dom dom 𝑛 ∧ ∀ 𝑥 ∈ dom dom 𝑚𝑦 ∈ dom dom 𝑚 ( 𝑥 𝑚 𝑦 ) = ( ( 𝑓𝑥 ) 𝑛 ( 𝑓𝑦 ) ) ) } )
29 0 28 wceq Ismty = ( 𝑚 ran ∞Met , 𝑛 ran ∞Met ↦ { 𝑓 ∣ ( 𝑓 : dom dom 𝑚1-1-onto→ dom dom 𝑛 ∧ ∀ 𝑥 ∈ dom dom 𝑚𝑦 ∈ dom dom 𝑚 ( 𝑥 𝑚 𝑦 ) = ( ( 𝑓𝑥 ) 𝑛 ( 𝑓𝑦 ) ) ) } )