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 \in ⋃ ran ∞Met, n \in ⋃ ran ∞Met ⟼ \{f \| (f : dom dom m \underset{1-1 onto}{⟶} dom dom n \land \forall x \in dom dom m \forall y \in 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 \underset{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 \forall y \in dom dom m x m y = f (x) n f (y)$
25	24 15 10	wral	$wff \forall x \in dom dom m \forall y \in dom dom m x m y = f (x) n f (y)$
26	14 25	wa	$wff (f : dom dom m \underset{1-1 onto}{⟶} dom dom n \land \forall x \in dom dom m \forall y \in dom dom m x m y = f (x) n f (y))$
27	26 6	cab	$class \{f \| (f : dom dom m \underset{1-1 onto}{⟶} dom dom n \land \forall x \in dom dom m \forall y \in dom dom m x m y = f (x) n f (y))\}$
28	1 5 4 4 27	cmpo	$class (m \in ⋃ ran ∞Met, n \in ⋃ ran ∞Met ⟼ \{f \| (f : dom dom m \underset{1-1 onto}{⟶} dom dom n \land \forall x \in dom dom m \forall y \in dom dom m x m y = f (x) n f (y))\})$
29	0 28	wceq	$wff Ismty = (m \in ⋃ ran ∞Met, n \in ⋃ ran ∞Met ⟼ \{f \| (f : dom dom m \underset{1-1 onto}{⟶} dom dom n \land \forall x \in dom dom m \forall y \in dom dom m x m y = f (x) n f (y))\})$

Metamath Proof Explorer

Definition df-ismty

Detailed syntax breakdown