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 𝑚 ( 𝑥 𝑚 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑛 ( 𝑓 ‘ 𝑦 ) ) ) } )