Metamath Proof Explorer

Theorem ismtyval

Description: The set of isometries between two metric spaces. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion ismtyval ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) → ( 𝑀 Ismty 𝑁 ) = { 𝑓 ∣ ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑁 ( 𝑓 ‘ 𝑦 ) ) ) } )

Proof

Step Hyp Ref Expression
1 df-ismty ⊢ Ismty = ( 𝑚 ∈ ∪ ran ∞Met , 𝑛 ∈ ∪ ran ∞Met ↦ { 𝑓 ∣ ( 𝑓 : dom dom 𝑚 –1-1-onto→ dom dom 𝑛 ∧ ∀ 𝑥 ∈ dom dom 𝑚 ∀ 𝑦 ∈ dom dom 𝑚 ( 𝑥 𝑚 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑛 ( 𝑓 ‘ 𝑦 ) ) ) } )
2 1 a1i ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) → Ismty = ( 𝑚 ∈ ∪ ran ∞Met , 𝑛 ∈ ∪ ran ∞Met ↦ { 𝑓 ∣ ( 𝑓 : dom dom 𝑚 –1-1-onto→ dom dom 𝑛 ∧ ∀ 𝑥 ∈ dom dom 𝑚 ∀ 𝑦 ∈ dom dom 𝑚 ( 𝑥 𝑚 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑛 ( 𝑓 ‘ 𝑦 ) ) ) } ) )
3 dmeq ⊢ ( 𝑚 = 𝑀 → dom 𝑚 = dom 𝑀 )
4 xmetf ⊢ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) → 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
5 4 fdmd ⊢ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) → dom 𝑀 = ( 𝑋 × 𝑋 ) )
6 3 5 sylan9eqr ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑚 = 𝑀 ) → dom 𝑚 = ( 𝑋 × 𝑋 ) )
7 6 ad2ant2r ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑚 = 𝑀 ∧ 𝑛 = 𝑁 ) ) → dom 𝑚 = ( 𝑋 × 𝑋 ) )
8 7 dmeqd ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑚 = 𝑀 ∧ 𝑛 = 𝑁 ) ) → dom dom 𝑚 = dom ( 𝑋 × 𝑋 ) )
9 dmxpid ⊢ dom ( 𝑋 × 𝑋 ) = 𝑋
10 8 9 eqtrdi ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑚 = 𝑀 ∧ 𝑛 = 𝑁 ) ) → dom dom 𝑚 = 𝑋 )
11 10 f1oeq2d ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑚 = 𝑀 ∧ 𝑛 = 𝑁 ) ) → ( 𝑓 : dom dom 𝑚 –1-1-onto→ dom dom 𝑛 ↔ 𝑓 : 𝑋 –1-1-onto→ dom dom 𝑛 ) )
12 dmeq ⊢ ( 𝑛 = 𝑁 → dom 𝑛 = dom 𝑁 )
13 xmetf ⊢ ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) → 𝑁 : ( 𝑌 × 𝑌 ) ⟶ ℝ* )
14 13 fdmd ⊢ ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) → dom 𝑁 = ( 𝑌 × 𝑌 ) )
15 12 14 sylan9eqr ⊢ ( ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑛 = 𝑁 ) → dom 𝑛 = ( 𝑌 × 𝑌 ) )
16 15 ad2ant2l ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑚 = 𝑀 ∧ 𝑛 = 𝑁 ) ) → dom 𝑛 = ( 𝑌 × 𝑌 ) )
17 16 dmeqd ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑚 = 𝑀 ∧ 𝑛 = 𝑁 ) ) → dom dom 𝑛 = dom ( 𝑌 × 𝑌 ) )
18 dmxpid ⊢ dom ( 𝑌 × 𝑌 ) = 𝑌
19 17 18 eqtrdi ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑚 = 𝑀 ∧ 𝑛 = 𝑁 ) ) → dom dom 𝑛 = 𝑌 )
20 f1oeq3 ⊢ ( dom dom 𝑛 = 𝑌 → ( 𝑓 : 𝑋 –1-1-onto→ dom dom 𝑛 ↔ 𝑓 : 𝑋 –1-1-onto→ 𝑌 ) )
21 19 20 syl ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑚 = 𝑀 ∧ 𝑛 = 𝑁 ) ) → ( 𝑓 : 𝑋 –1-1-onto→ dom dom 𝑛 ↔ 𝑓 : 𝑋 –1-1-onto→ 𝑌 ) )
22 11 21 bitrd ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑚 = 𝑀 ∧ 𝑛 = 𝑁 ) ) → ( 𝑓 : dom dom 𝑚 –1-1-onto→ dom dom 𝑛 ↔ 𝑓 : 𝑋 –1-1-onto→ 𝑌 ) )
23 oveq ⊢ ( 𝑚 = 𝑀 → ( 𝑥 𝑚 𝑦 ) = ( 𝑥 𝑀 𝑦 ) )
24 oveq ⊢ ( 𝑛 = 𝑁 → ( ( 𝑓 ‘ 𝑥 ) 𝑛 ( 𝑓 ‘ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝑁 ( 𝑓 ‘ 𝑦 ) ) )
25 23 24 eqeqan12d ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑛 = 𝑁 ) → ( ( 𝑥 𝑚 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑛 ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝑥 𝑀 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑁 ( 𝑓 ‘ 𝑦 ) ) ) )
26 25 adantl ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑚 = 𝑀 ∧ 𝑛 = 𝑁 ) ) → ( ( 𝑥 𝑚 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑛 ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝑥 𝑀 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑁 ( 𝑓 ‘ 𝑦 ) ) ) )
27 10 26 raleqbidv ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑚 = 𝑀 ∧ 𝑛 = 𝑁 ) ) → ( ∀ 𝑦 ∈ dom dom 𝑚 ( 𝑥 𝑚 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑛 ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑁 ( 𝑓 ‘ 𝑦 ) ) ) )
28 10 27 raleqbidv ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑚 = 𝑀 ∧ 𝑛 = 𝑁 ) ) → ( ∀ 𝑥 ∈ dom dom 𝑚 ∀ 𝑦 ∈ dom dom 𝑚 ( 𝑥 𝑚 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑛 ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑁 ( 𝑓 ‘ 𝑦 ) ) ) )
29 22 28 anbi12d ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑚 = 𝑀 ∧ 𝑛 = 𝑁 ) ) → ( ( 𝑓 : dom dom 𝑚 –1-1-onto→ dom dom 𝑛 ∧ ∀ 𝑥 ∈ dom dom 𝑚 ∀ 𝑦 ∈ dom dom 𝑚 ( 𝑥 𝑚 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑛 ( 𝑓 ‘ 𝑦 ) ) ) ↔ ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑁 ( 𝑓 ‘ 𝑦 ) ) ) ) )
30 29 abbidv ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝑚 = 𝑀 ∧ 𝑛 = 𝑁 ) ) → { 𝑓 ∣ ( 𝑓 : dom dom 𝑚 –1-1-onto→ dom dom 𝑛 ∧ ∀ 𝑥 ∈ dom dom 𝑚 ∀ 𝑦 ∈ dom dom 𝑚 ( 𝑥 𝑚 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑛 ( 𝑓 ‘ 𝑦 ) ) ) } = { 𝑓 ∣ ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑁 ( 𝑓 ‘ 𝑦 ) ) ) } )
31 fvssunirn ⊢ ( ∞Met ‘ 𝑋 ) ⊆ ∪ ran ∞Met
32 simpl ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
33 31 32 sselid ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) → 𝑀 ∈ ∪ ran ∞Met )
34 fvssunirn ⊢ ( ∞Met ‘ 𝑌 ) ⊆ ∪ ran ∞Met
35 simpr ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) → 𝑁 ∈ ( ∞Met ‘ 𝑌 ) )
36 34 35 sselid ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) → 𝑁 ∈ ∪ ran ∞Met )
37 f1of ⊢ ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 → 𝑓 : 𝑋 ⟶ 𝑌 )
38 37 adantr ⊢ ( ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑁 ( 𝑓 ‘ 𝑦 ) ) ) → 𝑓 : 𝑋 ⟶ 𝑌 )
39 elfvdm ⊢ ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) → 𝑌 ∈ dom ∞Met )
40 elfvdm ⊢ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 ∈ dom ∞Met )
41 elmapg ⊢ ( ( 𝑌 ∈ dom ∞Met ∧ 𝑋 ∈ dom ∞Met ) → ( 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ↔ 𝑓 : 𝑋 ⟶ 𝑌 ) )
42 39 40 41 syl2anr ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) → ( 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ↔ 𝑓 : 𝑋 ⟶ 𝑌 ) )
43 38 42 syl5ibr ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) → ( ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑁 ( 𝑓 ‘ 𝑦 ) ) ) → 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ) )
44 43 abssdv ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) → { 𝑓 ∣ ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑁 ( 𝑓 ‘ 𝑦 ) ) ) } ⊆ ( 𝑌 ↑m 𝑋 ) )
45 ovex ⊢ ( 𝑌 ↑m 𝑋 ) ∈ V
46 45 ssex ⊢ ( { 𝑓 ∣ ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑁 ( 𝑓 ‘ 𝑦 ) ) ) } ⊆ ( 𝑌 ↑m 𝑋 ) → { 𝑓 ∣ ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑁 ( 𝑓 ‘ 𝑦 ) ) ) } ∈ V )
47 44 46 syl ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) → { 𝑓 ∣ ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑁 ( 𝑓 ‘ 𝑦 ) ) ) } ∈ V )
48 2 30 33 36 47 ovmpod ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) → ( 𝑀 Ismty 𝑁 ) = { 𝑓 ∣ ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑁 ( 𝑓 ‘ 𝑦 ) ) ) } )