This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bnd2lem

Description: Lemma for equivbnd2 and similar theorems. (Contributed by Jeff Madsen, 16-Sep-2015)

Ref Expression
Hypothesis bnd2lem.1 ⊢ 𝐷 = ( 𝑀 ↾ ( 𝑌 × 𝑌 ) )
Assertion bnd2lem ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( Bnd ‘ 𝑌 ) ) → 𝑌 ⊆ 𝑋 )

Proof

Step Hyp Ref Expression
1 bnd2lem.1 ⊢ 𝐷 = ( 𝑀 ↾ ( 𝑌 × 𝑌 ) )
2 resss ⊢ ( 𝑀 ↾ ( 𝑌 × 𝑌 ) ) ⊆ 𝑀
3 1 2 eqsstri ⊢ 𝐷 ⊆ 𝑀
4 dmss ⊢ ( 𝐷 ⊆ 𝑀 → dom 𝐷 ⊆ dom 𝑀 )
5 3 4 mp1i ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( Bnd ‘ 𝑌 ) ) → dom 𝐷 ⊆ dom 𝑀 )
6 bndmet ⊢ ( 𝐷 ∈ ( Bnd ‘ 𝑌 ) → 𝐷 ∈ ( Met ‘ 𝑌 ) )
7 metf ⊢ ( 𝐷 ∈ ( Met ‘ 𝑌 ) → 𝐷 : ( 𝑌 × 𝑌 ) ⟶ ℝ )
8 fdm ⊢ ( 𝐷 : ( 𝑌 × 𝑌 ) ⟶ ℝ → dom 𝐷 = ( 𝑌 × 𝑌 ) )
9 6 7 8 3syl ⊢ ( 𝐷 ∈ ( Bnd ‘ 𝑌 ) → dom 𝐷 = ( 𝑌 × 𝑌 ) )
10 9 adantl ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( Bnd ‘ 𝑌 ) ) → dom 𝐷 = ( 𝑌 × 𝑌 ) )
11 metf ⊢ ( 𝑀 ∈ ( Met ‘ 𝑋 ) → 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ℝ )
12 11 fdmd ⊢ ( 𝑀 ∈ ( Met ‘ 𝑋 ) → dom 𝑀 = ( 𝑋 × 𝑋 ) )
13 12 adantr ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( Bnd ‘ 𝑌 ) ) → dom 𝑀 = ( 𝑋 × 𝑋 ) )
14 5 10 13 3sstr3d ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( Bnd ‘ 𝑌 ) ) → ( 𝑌 × 𝑌 ) ⊆ ( 𝑋 × 𝑋 ) )
15 dmss ⊢ ( ( 𝑌 × 𝑌 ) ⊆ ( 𝑋 × 𝑋 ) → dom ( 𝑌 × 𝑌 ) ⊆ dom ( 𝑋 × 𝑋 ) )
16 14 15 syl ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( Bnd ‘ 𝑌 ) ) → dom ( 𝑌 × 𝑌 ) ⊆ dom ( 𝑋 × 𝑋 ) )
17 dmxpid ⊢ dom ( 𝑌 × 𝑌 ) = 𝑌
18 dmxpid ⊢ dom ( 𝑋 × 𝑋 ) = 𝑋
19 16 17 18 3sstr3g ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( Bnd ‘ 𝑌 ) ) → 𝑌 ⊆ 𝑋 )