Metamath Proof Explorer

Theorem isismty

Description: The condition "is an isometry". (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion isismty ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ↔ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ismtyval ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) → ( 𝑀 Ismty 𝑁 ) = { 𝑓 ∣ ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑁 ( 𝑓 ‘ 𝑦 ) ) ) } )
2 1 eleq2d ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ↔ 𝐹 ∈ { 𝑓 ∣ ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑁 ( 𝑓 ‘ 𝑦 ) ) ) } ) )
3 f1of ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → 𝐹 : 𝑋 ⟶ 𝑌 )
4 3 adantr ⊢ ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
5 elfvdm ⊢ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 ∈ dom ∞Met )
6 elfvdm ⊢ ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) → 𝑌 ∈ dom ∞Met )
7 fex2 ⊢ ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑋 ∈ dom ∞Met ∧ 𝑌 ∈ dom ∞Met ) → 𝐹 ∈ V )
8 4 5 6 7 syl3an ⊢ ( ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) ∧ 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) → 𝐹 ∈ V )
9 8 3expib ⊢ ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) → ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) → 𝐹 ∈ V ) )
10 9 com12 ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) → ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) → 𝐹 ∈ V ) )
11 f1oeq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 ↔ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) )
12 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
13 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
14 12 13 oveq12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝑥 ) 𝑁 ( 𝑓 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) )
15 14 eqeq2d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑥 𝑀 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑁 ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) )
16 15 2ralbidv ⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑁 ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) )
17 11 16 anbi12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑁 ( 𝑓 ‘ 𝑦 ) ) ) ↔ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) ) )
18 17 elab3g ⊢ ( ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) → 𝐹 ∈ V ) → ( 𝐹 ∈ { 𝑓 ∣ ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑁 ( 𝑓 ‘ 𝑦 ) ) ) } ↔ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) ) )
19 10 18 syl ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) → ( 𝐹 ∈ { 𝑓 ∣ ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑁 ( 𝑓 ‘ 𝑦 ) ) ) } ↔ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) ) )
20 2 19 bitrd ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ↔ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) ) )