metss

Description: Two ways of saying that metric D generates a finer topology than metric C . (Contributed by Mario Carneiro, 12-Nov-2013) (Revised by Mario Carneiro, 24-Aug-2015)

	Ref	Expression
Hypotheses	metequiv.3	$⊢ J = MetOpen (C)$
	metequiv.4	$⊢ K = MetOpen (D)$
Assertion	metss	$⊢ (C \in ∞Met (X) \land D \in ∞Met (X)) \to (J \subseteq K \leftrightarrow \forall x \in X \forall r \in ℝ^{+} \exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r)$

Proof

Step	Hyp	Ref	Expression
1		metequiv.3	$⊢ J = MetOpen (C)$
2		metequiv.4	$⊢ K = MetOpen (D)$
3	1	mopnval	$⊢ C \in ∞Met (X) \to J = topGen (ran ball (C))$
4	3	adantr	$⊢ (C \in ∞Met (X) \land D \in ∞Met (X)) \to J = topGen (ran ball (C))$
5	2	mopnval	$⊢ D \in ∞Met (X) \to K = topGen (ran ball (D))$
6	5	adantl	$⊢ (C \in ∞Met (X) \land D \in ∞Met (X)) \to K = topGen (ran ball (D))$
7	4 6	sseq12d	$⊢ (C \in ∞Met (X) \land D \in ∞Met (X)) \to (J \subseteq K \leftrightarrow topGen (ran ball (C)) \subseteq topGen (ran ball (D)))$
8		blbas	$⊢ C \in ∞Met (X) \to ran ball (C) \in TopBases$
9		unirnbl	$⊢ C \in ∞Met (X) \to ⋃ ran ball (C) = X$
10	9	adantr	$⊢ (C \in ∞Met (X) \land D \in ∞Met (X)) \to ⋃ ran ball (C) = X$
11		unirnbl	$⊢ D \in ∞Met (X) \to ⋃ ran ball (D) = X$
12	11	adantl	$⊢ (C \in ∞Met (X) \land D \in ∞Met (X)) \to ⋃ ran ball (D) = X$
13	10 12	eqtr4d	$⊢ (C \in ∞Met (X) \land D \in ∞Met (X)) \to ⋃ ran ball (C) = ⋃ ran ball (D)$
14		tgss2	$⊢ (ran ball (C) \in TopBases \land ⋃ ran ball (C) = ⋃ ran ball (D)) \to (topGen (ran ball (C)) \subseteq topGen (ran ball (D)) \leftrightarrow \forall x \in ⋃ ran ball (C) \forall y \in ran ball (C) (x \in y \to \exists z \in ran ball (D) (x \in z \land z \subseteq y)))$
15	8 13 14	syl2an2r	$⊢ (C \in ∞Met (X) \land D \in ∞Met (X)) \to (topGen (ran ball (C)) \subseteq topGen (ran ball (D)) \leftrightarrow \forall x \in ⋃ ran ball (C) \forall y \in ran ball (C) (x \in y \to \exists z \in ran ball (D) (x \in z \land z \subseteq y)))$
16	10	raleqdv	$⊢ (C \in ∞Met (X) \land D \in ∞Met (X)) \to (\forall x \in ⋃ ran ball (C) \forall y \in ran ball (C) (x \in y \to \exists z \in ran ball (D) (x \in z \land z \subseteq y)) \leftrightarrow \forall x \in X \forall y \in ran ball (C) (x \in y \to \exists z \in ran ball (D) (x \in z \land z \subseteq y)))$
17		blssex	$⊢ (D \in ∞Met (X) \land x \in X) \to (\exists z \in ran ball (D) (x \in z \land z \subseteq y) \leftrightarrow \exists s \in ℝ^{+} x ball (D) s \subseteq y)$
18	17	adantll	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (X)) \land x \in X) \to (\exists z \in ran ball (D) (x \in z \land z \subseteq y) \leftrightarrow \exists s \in ℝ^{+} x ball (D) s \subseteq y)$
19	18	imbi2d	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (X)) \land x \in X) \to ((x \in y \to \exists z \in ran ball (D) (x \in z \land z \subseteq y)) \leftrightarrow (x \in y \to \exists s \in ℝ^{+} x ball (D) s \subseteq y))$
20	19	ralbidv	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (X)) \land x \in X) \to (\forall y \in ran ball (C) (x \in y \to \exists z \in ran ball (D) (x \in z \land z \subseteq y)) \leftrightarrow \forall y \in ran ball (C) (x \in y \to \exists s \in ℝ^{+} x ball (D) s \subseteq y))$
21		rpxr	$⊢ r \in ℝ^{+} \to r \in ℝ^{*}$
22		blelrn	$⊢ (C \in ∞Met (X) \land x \in X \land r \in ℝ^{*}) \to x ball (C) r \in ran ball (C)$
23	21 22	syl3an3	$⊢ (C \in ∞Met (X) \land x \in X \land r \in ℝ^{+}) \to x ball (C) r \in ran ball (C)$
24		blcntr	$⊢ (C \in ∞Met (X) \land x \in X \land r \in ℝ^{+}) \to x \in (x ball (C) r)$
25		eleq2	$⊢ y = x ball (C) r \to (x \in y \leftrightarrow x \in (x ball (C) r))$
26		sseq2	$⊢ y = x ball (C) r \to (x ball (D) s \subseteq y \leftrightarrow x ball (D) s \subseteq x ball (C) r)$
27	26	rexbidv	$⊢ y = x ball (C) r \to (\exists s \in ℝ^{+} x ball (D) s \subseteq y \leftrightarrow \exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r)$
28	25 27	imbi12d	$⊢ y = x ball (C) r \to ((x \in y \to \exists s \in ℝ^{+} x ball (D) s \subseteq y) \leftrightarrow (x \in (x ball (C) r) \to \exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r))$
29	28	rspcv	$⊢ x ball (C) r \in ran ball (C) \to (\forall y \in ran ball (C) (x \in y \to \exists s \in ℝ^{+} x ball (D) s \subseteq y) \to (x \in (x ball (C) r) \to \exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r))$
30	29	com23	$⊢ x ball (C) r \in ran ball (C) \to (x \in (x ball (C) r) \to (\forall y \in ran ball (C) (x \in y \to \exists s \in ℝ^{+} x ball (D) s \subseteq y) \to \exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r))$
31	23 24 30	sylc	$⊢ (C \in ∞Met (X) \land x \in X \land r \in ℝ^{+}) \to (\forall y \in ran ball (C) (x \in y \to \exists s \in ℝ^{+} x ball (D) s \subseteq y) \to \exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r)$
32	31	ad4ant134	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (X)) \land x \in X) \land r \in ℝ^{+}) \to (\forall y \in ran ball (C) (x \in y \to \exists s \in ℝ^{+} x ball (D) s \subseteq y) \to \exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r)$
33	32	ralrimdva	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (X)) \land x \in X) \to (\forall y \in ran ball (C) (x \in y \to \exists s \in ℝ^{+} x ball (D) s \subseteq y) \to \forall r \in ℝ^{+} \exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r)$
34		blss	$⊢ (C \in ∞Met (X) \land y \in ran ball (C) \land x \in y) \to \exists r \in ℝ^{+} x ball (C) r \subseteq y$
35	34	3expb	$⊢ (C \in ∞Met (X) \land (y \in ran ball (C) \land x \in y)) \to \exists r \in ℝ^{+} x ball (C) r \subseteq y$
36	35	ad4ant14	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (X)) \land x \in X) \land (y \in ran ball (C) \land x \in y)) \to \exists r \in ℝ^{+} x ball (C) r \subseteq y$
37		r19.29	$⊢ (\forall r \in ℝ^{+} \exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r \land \exists r \in ℝ^{+} x ball (C) r \subseteq y) \to \exists r \in ℝ^{+} (\exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r \land x ball (C) r \subseteq y)$
38		sstr	$⊢ (x ball (D) s \subseteq x ball (C) r \land x ball (C) r \subseteq y) \to x ball (D) s \subseteq y$
39	38	expcom	$⊢ x ball (C) r \subseteq y \to (x ball (D) s \subseteq x ball (C) r \to x ball (D) s \subseteq y)$
40	39	reximdv	$⊢ x ball (C) r \subseteq y \to (\exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r \to \exists s \in ℝ^{+} x ball (D) s \subseteq y)$
41	40	impcom	$⊢ (\exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r \land x ball (C) r \subseteq y) \to \exists s \in ℝ^{+} x ball (D) s \subseteq y$
42	41	rexlimivw	$⊢ \exists r \in ℝ^{+} (\exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r \land x ball (C) r \subseteq y) \to \exists s \in ℝ^{+} x ball (D) s \subseteq y$
43	37 42	syl	$⊢ (\forall r \in ℝ^{+} \exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r \land \exists r \in ℝ^{+} x ball (C) r \subseteq y) \to \exists s \in ℝ^{+} x ball (D) s \subseteq y$
44	43	ex	$⊢ \forall r \in ℝ^{+} \exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r \to (\exists r \in ℝ^{+} x ball (C) r \subseteq y \to \exists s \in ℝ^{+} x ball (D) s \subseteq y)$
45	36 44	syl5com	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (X)) \land x \in X) \land (y \in ran ball (C) \land x \in y)) \to (\forall r \in ℝ^{+} \exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r \to \exists s \in ℝ^{+} x ball (D) s \subseteq y)$
46	45	expr	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (X)) \land x \in X) \land y \in ran ball (C)) \to (x \in y \to (\forall r \in ℝ^{+} \exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r \to \exists s \in ℝ^{+} x ball (D) s \subseteq y))$
47	46	com23	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (X)) \land x \in X) \land y \in ran ball (C)) \to (\forall r \in ℝ^{+} \exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r \to (x \in y \to \exists s \in ℝ^{+} x ball (D) s \subseteq y))$
48	47	ralrimdva	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (X)) \land x \in X) \to (\forall r \in ℝ^{+} \exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r \to \forall y \in ran ball (C) (x \in y \to \exists s \in ℝ^{+} x ball (D) s \subseteq y))$
49	33 48	impbid	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (X)) \land x \in X) \to (\forall y \in ran ball (C) (x \in y \to \exists s \in ℝ^{+} x ball (D) s \subseteq y) \leftrightarrow \forall r \in ℝ^{+} \exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r)$
50	20 49	bitrd	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (X)) \land x \in X) \to (\forall y \in ran ball (C) (x \in y \to \exists z \in ran ball (D) (x \in z \land z \subseteq y)) \leftrightarrow \forall r \in ℝ^{+} \exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r)$
51	50	ralbidva	$⊢ (C \in ∞Met (X) \land D \in ∞Met (X)) \to (\forall x \in X \forall y \in ran ball (C) (x \in y \to \exists z \in ran ball (D) (x \in z \land z \subseteq y)) \leftrightarrow \forall x \in X \forall r \in ℝ^{+} \exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r)$
52	16 51	bitrd	$⊢ (C \in ∞Met (X) \land D \in ∞Met (X)) \to (\forall x \in ⋃ ran ball (C) \forall y \in ran ball (C) (x \in y \to \exists z \in ran ball (D) (x \in z \land z \subseteq y)) \leftrightarrow \forall x \in X \forall r \in ℝ^{+} \exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r)$
53	7 15 52	3bitrd	$⊢ (C \in ∞Met (X) \land D \in ∞Met (X)) \to (J \subseteq K \leftrightarrow \forall x \in X \forall r \in ℝ^{+} \exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r)$

Metamath Proof Explorer

Theorem metss

Proof