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 = m ∈ ⋃ ran ⁡ ∞Met , n ∈ ⋃ ran ⁡ ∞Met ⟼ f | f : dom ⁡ dom ⁡ m ⟶ 1-1 onto dom ⁡ dom ⁡ n ∧ ∀ x ∈ dom ⁡ dom ⁡ m ∀ y ∈ dom ⁡ dom ⁡ m x m y = f ⁡ x n f ⁡ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cismty class Ismty
1 vm setvar m
2 cxmet class ∞Met
3 2 crn class ran ⁡ ∞Met
4 3 cuni class ⋃ ran ⁡ ∞Met
5 vn setvar n
6 vf setvar f
7 6 cv setvar f
8 1 cv setvar m
9 8 cdm class dom ⁡ m
10 9 cdm class dom ⁡ dom ⁡ m
11 5 cv setvar n
12 11 cdm class dom ⁡ n
13 12 cdm class dom ⁡ dom ⁡ n
14 10 13 7 wf1o wff f : dom ⁡ dom ⁡ m ⟶ 1-1 onto dom ⁡ dom ⁡ n
15 vx setvar x
16 vy setvar y
17 15 cv setvar x
18 16 cv setvar y
19 17 18 8 co class x m y
20 17 7 cfv class f ⁡ x
21 18 7 cfv class f ⁡ y
22 20 21 11 co class f ⁡ x n f ⁡ y
23 19 22 wceq wff x m y = f ⁡ x n f ⁡ y
24 23 16 10 wral wff ∀ y ∈ dom ⁡ dom ⁡ m x m y = f ⁡ x n f ⁡ y
25 24 15 10 wral wff ∀ x ∈ dom ⁡ dom ⁡ m ∀ y ∈ dom ⁡ dom ⁡ m x m y = f ⁡ x n f ⁡ y
26 14 25 wa wff f : dom ⁡ dom ⁡ m ⟶ 1-1 onto dom ⁡ dom ⁡ n ∧ ∀ x ∈ dom ⁡ dom ⁡ m ∀ y ∈ dom ⁡ dom ⁡ m x m y = f ⁡ x n f ⁡ y
27 26 6 cab class f | f : dom ⁡ dom ⁡ m ⟶ 1-1 onto dom ⁡ dom ⁡ n ∧ ∀ x ∈ dom ⁡ dom ⁡ m ∀ y ∈ dom ⁡ dom ⁡ m x m y = f ⁡ x n f ⁡ y
28 1 5 4 4 27 cmpo class m ∈ ⋃ ran ⁡ ∞Met , n ∈ ⋃ ran ⁡ ∞Met ⟼ f | f : dom ⁡ dom ⁡ m ⟶ 1-1 onto dom ⁡ dom ⁡ n ∧ ∀ x ∈ dom ⁡ dom ⁡ m ∀ y ∈ dom ⁡ dom ⁡ m x m y = f ⁡ x n f ⁡ y
29 0 28 wceq wff Ismty = m ∈ ⋃ ran ⁡ ∞Met , n ∈ ⋃ ran ⁡ ∞Met ⟼ f | f : dom ⁡ dom ⁡ m ⟶ 1-1 onto dom ⁡ dom ⁡ n ∧ ∀ x ∈ dom ⁡ dom ⁡ m ∀ y ∈ dom ⁡ dom ⁡ m x m y = f ⁡ x n f ⁡ y