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 imbitrrid ⊒ ( ( 𝑀 ∈ ( ∞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β†’ π‘Œ ∧ βˆ€ π‘₯ ∈ 𝑋 βˆ€ 𝑦 ∈ 𝑋 ( π‘₯ 𝑀 𝑦 ) = ( ( 𝑓 β€˜ π‘₯ ) 𝑁 ( 𝑓 β€˜ 𝑦 ) ) ) } )