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 π‘š ( π‘₯ π‘š 𝑦 ) = ( ( 𝑓 β€˜ π‘₯ ) 𝑛 ( 𝑓 β€˜ 𝑦 ) ) ) } )