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 ‘ 𝑌 ) ) → 𝑌 ⊆ 𝑋 )