Metamath Proof Explorer

Theorem metres2

Description: Lemma for metres . (Contributed by FL, 12-Oct-2006) (Proof shortened by Mario Carneiro, 14-Aug-2015)

Ref Expression
Assertion metres2 ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝑅 βŠ† 𝑋 ) β†’ ( 𝐷 β†Ύ ( 𝑅 Γ— 𝑅 ) ) ∈ ( Met β€˜ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 metxmet ⊒ ( 𝐷 ∈ ( Met β€˜ 𝑋 ) β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
2 xmetres2 ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑅 βŠ† 𝑋 ) β†’ ( 𝐷 β†Ύ ( 𝑅 Γ— 𝑅 ) ) ∈ ( ∞Met β€˜ 𝑅 ) )
3 1 2 sylan ⊒ ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝑅 βŠ† 𝑋 ) β†’ ( 𝐷 β†Ύ ( 𝑅 Γ— 𝑅 ) ) ∈ ( ∞Met β€˜ 𝑅 ) )
4 metf ⊒ ( 𝐷 ∈ ( Met β€˜ 𝑋 ) β†’ 𝐷 : ( 𝑋 Γ— 𝑋 ) ⟢ ℝ )
5 4 adantr ⊒ ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝑅 βŠ† 𝑋 ) β†’ 𝐷 : ( 𝑋 Γ— 𝑋 ) ⟢ ℝ )
6 simpr ⊒ ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝑅 βŠ† 𝑋 ) β†’ 𝑅 βŠ† 𝑋 )
7 xpss12 ⊒ ( ( 𝑅 βŠ† 𝑋 ∧ 𝑅 βŠ† 𝑋 ) β†’ ( 𝑅 Γ— 𝑅 ) βŠ† ( 𝑋 Γ— 𝑋 ) )
8 6 7 sylancom ⊒ ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝑅 βŠ† 𝑋 ) β†’ ( 𝑅 Γ— 𝑅 ) βŠ† ( 𝑋 Γ— 𝑋 ) )
9 5 8 fssresd ⊒ ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝑅 βŠ† 𝑋 ) β†’ ( 𝐷 β†Ύ ( 𝑅 Γ— 𝑅 ) ) : ( 𝑅 Γ— 𝑅 ) ⟢ ℝ )
10 ismet2 ⊒ ( ( 𝐷 β†Ύ ( 𝑅 Γ— 𝑅 ) ) ∈ ( Met β€˜ 𝑅 ) ↔ ( ( 𝐷 β†Ύ ( 𝑅 Γ— 𝑅 ) ) ∈ ( ∞Met β€˜ 𝑅 ) ∧ ( 𝐷 β†Ύ ( 𝑅 Γ— 𝑅 ) ) : ( 𝑅 Γ— 𝑅 ) ⟢ ℝ ) )
11 3 9 10 sylanbrc ⊒ ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝑅 βŠ† 𝑋 ) β†’ ( 𝐷 β†Ύ ( 𝑅 Γ— 𝑅 ) ) ∈ ( Met β€˜ 𝑅 ) )