# Metamath Proof Explorer

## Theorem bnd2lem

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

Ref Expression
Hypothesis bnd2lem.1 ${⊢}{D}={{M}↾}_{\left({Y}×{Y}\right)}$
Assertion bnd2lem ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {D}\in \mathrm{Bnd}\left({Y}\right)\right)\to {Y}\subseteq {X}$

### Proof

Step Hyp Ref Expression
1 bnd2lem.1 ${⊢}{D}={{M}↾}_{\left({Y}×{Y}\right)}$
2 resss ${⊢}{{M}↾}_{\left({Y}×{Y}\right)}\subseteq {M}$
3 1 2 eqsstri ${⊢}{D}\subseteq {M}$
4 dmss ${⊢}{D}\subseteq {M}\to \mathrm{dom}{D}\subseteq \mathrm{dom}{M}$
5 3 4 mp1i ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {D}\in \mathrm{Bnd}\left({Y}\right)\right)\to \mathrm{dom}{D}\subseteq \mathrm{dom}{M}$
6 bndmet ${⊢}{D}\in \mathrm{Bnd}\left({Y}\right)\to {D}\in \mathrm{Met}\left({Y}\right)$
7 metf ${⊢}{D}\in \mathrm{Met}\left({Y}\right)\to {D}:{Y}×{Y}⟶ℝ$
8 fdm ${⊢}{D}:{Y}×{Y}⟶ℝ\to \mathrm{dom}{D}={Y}×{Y}$
9 6 7 8 3syl ${⊢}{D}\in \mathrm{Bnd}\left({Y}\right)\to \mathrm{dom}{D}={Y}×{Y}$
10 9 adantl ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {D}\in \mathrm{Bnd}\left({Y}\right)\right)\to \mathrm{dom}{D}={Y}×{Y}$
11 metf ${⊢}{M}\in \mathrm{Met}\left({X}\right)\to {M}:{X}×{X}⟶ℝ$
12 11 fdmd ${⊢}{M}\in \mathrm{Met}\left({X}\right)\to \mathrm{dom}{M}={X}×{X}$
13 12 adantr ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {D}\in \mathrm{Bnd}\left({Y}\right)\right)\to \mathrm{dom}{M}={X}×{X}$
14 5 10 13 3sstr3d ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {D}\in \mathrm{Bnd}\left({Y}\right)\right)\to {Y}×{Y}\subseteq {X}×{X}$
15 dmss ${⊢}{Y}×{Y}\subseteq {X}×{X}\to \mathrm{dom}\left({Y}×{Y}\right)\subseteq \mathrm{dom}\left({X}×{X}\right)$
16 14 15 syl ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {D}\in \mathrm{Bnd}\left({Y}\right)\right)\to \mathrm{dom}\left({Y}×{Y}\right)\subseteq \mathrm{dom}\left({X}×{X}\right)$
17 dmxpid ${⊢}\mathrm{dom}\left({Y}×{Y}\right)={Y}$
18 dmxpid ${⊢}\mathrm{dom}\left({X}×{X}\right)={X}$
19 16 17 18 3sstr3g ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {D}\in \mathrm{Bnd}\left({Y}\right)\right)\to {Y}\subseteq {X}$