bnd2lem

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

		Ref	Expression
	Hypothesis	bnd2lem.1	$⊢ D = {M ↾}_{(Y \times Y)}$
	Assertion	bnd2lem	$⊢ (M \in Met (X) \land D \in Bnd (Y)) \to Y \subseteq X$

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

Metamath Proof Explorer