Theorem metss 22526

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

Hypotheses

Ref	Expression
metequiv.3	⊢ 𝐽 = (MetOpen‘𝐶)
metequiv.4	⊢ 𝐾 = (MetOpen‘𝐷)

Assertion

Ref	Expression
metss	⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) → (𝐽 ⊆ 𝐾 ↔ ∀𝑥 ∈ 𝑋 ∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟)))

Distinct variable groups:   𝑠,𝑟,𝑥,𝐶   𝐽,𝑟,𝑠,𝑥   𝐾,𝑟,𝑠,𝑥   𝐷,𝑟,𝑠,𝑥   𝑋,𝑟,𝑠,𝑥

Proof of Theorem metss

Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		metequiv.3	. . . . 5 ⊢ 𝐽 = (MetOpen‘𝐶)
2	1	mopnval 22456	. . . 4 ⊢ (𝐶 ∈ (∞Met‘𝑋) → 𝐽 = (topGen‘ran (ball‘𝐶)))
3	2	adantr 466	. . 3 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) → 𝐽 = (topGen‘ran (ball‘𝐶)))
4		metequiv.4	. . . . 5 ⊢ 𝐾 = (MetOpen‘𝐷)
5	4	mopnval 22456	. . . 4 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐾 = (topGen‘ran (ball‘𝐷)))
6	5	adantl 467	. . 3 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) → 𝐾 = (topGen‘ran (ball‘𝐷)))
7	3, 6	sseq12d 3783	. 2 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) → (𝐽 ⊆ 𝐾 ↔ (topGen‘ran (ball‘𝐶)) ⊆ (topGen‘ran (ball‘𝐷))))
8		blbas 22448	. . . 4 ⊢ (𝐶 ∈ (∞Met‘𝑋) → ran (ball‘𝐶) ∈ TopBases)
9	8	adantr 466	. . 3 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) → ran (ball‘𝐶) ∈ TopBases)
10		unirnbl 22438	. . . . 5 ⊢ (𝐶 ∈ (∞Met‘𝑋) → ∪ ran (ball‘𝐶) = 𝑋)
11	10	adantr 466	. . . 4 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) → ∪ ran (ball‘𝐶) = 𝑋)
12		unirnbl 22438	. . . . 5 ⊢ (𝐷 ∈ (∞Met‘𝑋) → ∪ ran (ball‘𝐷) = 𝑋)
13	12	adantl 467	. . . 4 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) → ∪ ran (ball‘𝐷) = 𝑋)
14	11, 13	eqtr4d 2808	. . 3 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) → ∪ ran (ball‘𝐶) = ∪ ran (ball‘𝐷))
15		tgss2 21005	. . 3 ⊢ ((ran (ball‘𝐶) ∈ TopBases ∧ ∪ ran (ball‘𝐶) = ∪ ran (ball‘𝐷)) → ((topGen‘ran (ball‘𝐶)) ⊆ (topGen‘ran (ball‘𝐷)) ↔ ∀𝑥 ∈ ∪ ran (ball‘𝐶)∀𝑦 ∈ ran (ball‘𝐶)(𝑥 ∈ 𝑦 → ∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))))
16	9, 14, 15	syl2anc 573	. 2 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) → ((topGen‘ran (ball‘𝐶)) ⊆ (topGen‘ran (ball‘𝐷)) ↔ ∀𝑥 ∈ ∪ ran (ball‘𝐶)∀𝑦 ∈ ran (ball‘𝐶)(𝑥 ∈ 𝑦 → ∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))))
17	11	raleqdv 3293	. . 3 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) → (∀𝑥 ∈ ∪ ran (ball‘𝐶)∀𝑦 ∈ ran (ball‘𝐶)(𝑥 ∈ 𝑦 → ∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦)) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ ran (ball‘𝐶)(𝑥 ∈ 𝑦 → ∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))))
18		blssex 22445	. . . . . . . 8 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) → (∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦) ↔ ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ 𝑦))
19	18	adantll 693	. . . . . . 7 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) ∧ 𝑥 ∈ 𝑋) → (∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦) ↔ ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ 𝑦))
20	19	imbi2d 329	. . . . . 6 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) ∧ 𝑥 ∈ 𝑋) → ((𝑥 ∈ 𝑦 → ∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦)) ↔ (𝑥 ∈ 𝑦 → ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ 𝑦)))
21	20	ralbidv 3135	. . . . 5 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) ∧ 𝑥 ∈ 𝑋) → (∀𝑦 ∈ ran (ball‘𝐶)(𝑥 ∈ 𝑦 → ∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦)) ↔ ∀𝑦 ∈ ran (ball‘𝐶)(𝑥 ∈ 𝑦 → ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ 𝑦)))
22		rpxr 12036	. . . . . . . . . . 11 ⊢ (𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ*)
23		blelrn 22435	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ*) → (𝑥(ball‘𝐶)𝑟) ∈ ran (ball‘𝐶))
24	22, 23	syl3an3 1169	. . . . . . . . . 10 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) → (𝑥(ball‘𝐶)𝑟) ∈ ran (ball‘𝐶))
25		blcntr 22431	. . . . . . . . . 10 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) → 𝑥 ∈ (𝑥(ball‘𝐶)𝑟))
26		eleq2 2839	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑥(ball‘𝐶)𝑟) → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ (𝑥(ball‘𝐶)𝑟)))
27		sseq2 3776	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑥(ball‘𝐶)𝑟) → ((𝑥(ball‘𝐷)𝑠) ⊆ 𝑦 ↔ (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟)))
28	27	rexbidv 3200	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑥(ball‘𝐶)𝑟) → (∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ 𝑦 ↔ ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟)))
29	26, 28	imbi12d 333	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑥(ball‘𝐶)𝑟) → ((𝑥 ∈ 𝑦 → ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ 𝑦) ↔ (𝑥 ∈ (𝑥(ball‘𝐶)𝑟) → ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟))))
30	29	rspcv 3456	. . . . . . . . . . 11 ⊢ ((𝑥(ball‘𝐶)𝑟) ∈ ran (ball‘𝐶) → (∀𝑦 ∈ ran (ball‘𝐶)(𝑥 ∈ 𝑦 → ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ 𝑦) → (𝑥 ∈ (𝑥(ball‘𝐶)𝑟) → ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟))))
31	30	com23 86	. . . . . . . . . 10 ⊢ ((𝑥(ball‘𝐶)𝑟) ∈ ran (ball‘𝐶) → (𝑥 ∈ (𝑥(ball‘𝐶)𝑟) → (∀𝑦 ∈ ran (ball‘𝐶)(𝑥 ∈ 𝑦 → ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ 𝑦) → ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟))))
32	24, 25, 31	sylc 65	. . . . . . . . 9 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) → (∀𝑦 ∈ ran (ball‘𝐶)(𝑥 ∈ 𝑦 → ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ 𝑦) → ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟)))
33	32	3expa 1111	. . . . . . . 8 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ 𝑟 ∈ ℝ+) → (∀𝑦 ∈ ran (ball‘𝐶)(𝑥 ∈ 𝑦 → ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ 𝑦) → ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟)))
34	33	adantllr 698	. . . . . . 7 ⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑟 ∈ ℝ+) → (∀𝑦 ∈ ran (ball‘𝐶)(𝑥 ∈ 𝑦 → ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ 𝑦) → ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟)))
35	34	ralrimdva 3118	. . . . . 6 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) ∧ 𝑥 ∈ 𝑋) → (∀𝑦 ∈ ran (ball‘𝐶)(𝑥 ∈ 𝑦 → ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ 𝑦) → ∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟)))
36		blss 22443	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ ran (ball‘𝐶) ∧ 𝑥 ∈ 𝑦) → ∃𝑟 ∈ ℝ+ (𝑥(ball‘𝐶)𝑟) ⊆ 𝑦)
37	36	3expb 1113	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ (𝑦 ∈ ran (ball‘𝐶) ∧ 𝑥 ∈ 𝑦)) → ∃𝑟 ∈ ℝ+ (𝑥(ball‘𝐶)𝑟) ⊆ 𝑦)
38	37	adantlr 694	. . . . . . . . . . 11 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) ∧ (𝑦 ∈ ran (ball‘𝐶) ∧ 𝑥 ∈ 𝑦)) → ∃𝑟 ∈ ℝ+ (𝑥(ball‘𝐶)𝑟) ⊆ 𝑦)
39	38	adantlr 694	. . . . . . . . . 10 ⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ ran (ball‘𝐶) ∧ 𝑥 ∈ 𝑦)) → ∃𝑟 ∈ ℝ+ (𝑥(ball‘𝐶)𝑟) ⊆ 𝑦)
40		r19.29 3220	. . . . . . . . . . . 12 ⊢ ((∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟) ∧ ∃𝑟 ∈ ℝ+ (𝑥(ball‘𝐶)𝑟) ⊆ 𝑦) → ∃𝑟 ∈ ℝ+ (∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟) ∧ (𝑥(ball‘𝐶)𝑟) ⊆ 𝑦))
41		sstr 3760	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟) ∧ (𝑥(ball‘𝐶)𝑟) ⊆ 𝑦) → (𝑥(ball‘𝐷)𝑠) ⊆ 𝑦)
42	41	expcom 398	. . . . . . . . . . . . . . 15 ⊢ ((𝑥(ball‘𝐶)𝑟) ⊆ 𝑦 → ((𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟) → (𝑥(ball‘𝐷)𝑠) ⊆ 𝑦))
43	42	reximdv 3164	. . . . . . . . . . . . . 14 ⊢ ((𝑥(ball‘𝐶)𝑟) ⊆ 𝑦 → (∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟) → ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ 𝑦))
44	43	impcom 394	. . . . . . . . . . . . 13 ⊢ ((∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟) ∧ (𝑥(ball‘𝐶)𝑟) ⊆ 𝑦) → ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ 𝑦)
45	44	rexlimivw 3177	. . . . . . . . . . . 12 ⊢ (∃𝑟 ∈ ℝ+ (∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟) ∧ (𝑥(ball‘𝐶)𝑟) ⊆ 𝑦) → ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ 𝑦)
46	40, 45	syl 17	. . . . . . . . . . 11 ⊢ ((∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟) ∧ ∃𝑟 ∈ ℝ+ (𝑥(ball‘𝐶)𝑟) ⊆ 𝑦) → ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ 𝑦)
47	46	ex 397	. . . . . . . . . 10 ⊢ (∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟) → (∃𝑟 ∈ ℝ+ (𝑥(ball‘𝐶)𝑟) ⊆ 𝑦 → ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ 𝑦))
48	39, 47	syl5com 31	. . . . . . . . 9 ⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ ran (ball‘𝐶) ∧ 𝑥 ∈ 𝑦)) → (∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟) → ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ 𝑦))
49	48	expr 444	. . . . . . . 8 ⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ ran (ball‘𝐶)) → (𝑥 ∈ 𝑦 → (∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟) → ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ 𝑦)))
50	49	com23 86	. . . . . . 7 ⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ ran (ball‘𝐶)) → (∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟) → (𝑥 ∈ 𝑦 → ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ 𝑦)))
51	50	ralrimdva 3118	. . . . . 6 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) ∧ 𝑥 ∈ 𝑋) → (∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟) → ∀𝑦 ∈ ran (ball‘𝐶)(𝑥 ∈ 𝑦 → ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ 𝑦)))
52	35, 51	impbid 202	. . . . 5 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) ∧ 𝑥 ∈ 𝑋) → (∀𝑦 ∈ ran (ball‘𝐶)(𝑥 ∈ 𝑦 → ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ 𝑦) ↔ ∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟)))
53	21, 52	bitrd 268	. . . 4 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) ∧ 𝑥 ∈ 𝑋) → (∀𝑦 ∈ ran (ball‘𝐶)(𝑥 ∈ 𝑦 → ∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦)) ↔ ∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟)))
54	53	ralbidva 3134	. . 3 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ ran (ball‘𝐶)(𝑥 ∈ 𝑦 → ∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦)) ↔ ∀𝑥 ∈ 𝑋 ∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟)))
55	17, 54	bitrd 268	. 2 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) → (∀𝑥 ∈ ∪ ran (ball‘𝐶)∀𝑦 ∈ ran (ball‘𝐶)(𝑥 ∈ 𝑦 → ∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦)) ↔ ∀𝑥 ∈ 𝑋 ∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟)))
56	7, 16, 55	3bitrd 294	1 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) → (𝐽 ⊆ 𝐾 ↔ ∀𝑥 ∈ 𝑋 ∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟)))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 382   ∧ w3a 1071   = wceq 1631   ∈ wcel 2145  ∀wral 3061  ∃wrex 3062   ⊆ wss 3723  ∪ cuni 4574  ran crn 5250  ‘cfv 6029  (class class class)co 6791  ℝ^*cxr 10273  ℝ⁺crp 12028  topGenctg 16299  ∞Metcxmt 19939  ballcbl 19941  MetOpencmopn 19944  TopBasesctb 20963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7094  ax-cnex 10192  ax-resscn 10193  ax-1cn 10194  ax-icn 10195  ax-addcl 10196  ax-addrcl 10197  ax-mulcl 10198  ax-mulrcl 10199  ax-mulcom 10200  ax-addass 10201  ax-mulass 10202  ax-distr 10203  ax-i2m1 10204  ax-1ne0 10205  ax-1rid 10206  ax-rnegex 10207  ax-rrecex 10208  ax-cnre 10209  ax-pre-lttri 10210  ax-pre-lttrn 10211  ax-pre-ltadd 10212  ax-pre-mulgt0 10213  ax-pre-sup 10214

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5821  df-ord 5867  df-on 5868  df-lim 5869  df-suc 5870  df-iota 5992  df-fun 6031  df-fn 6032  df-f 6033  df-f1 6034  df-fo 6035  df-f1o 6036  df-fv 6037  df-riota 6752  df-ov 6794  df-oprab 6795  df-mpt2 6796  df-om 7211  df-1st 7313  df-2nd 7314  df-wrecs 7557  df-recs 7619  df-rdg 7657  df-er 7894  df-map 8009  df-en 8108  df-dom 8109  df-sdom 8110  df-sup 8502  df-inf 8503  df-pnf 10276  df-mnf 10277  df-xr 10278  df-ltxr 10279  df-le 10280  df-sub 10468  df-neg 10469  df-div 10885  df-nn 11221  df-2 11279  df-n0 11493  df-z 11578  df-uz 11887  df-q 11990  df-rp 12029  df-xneg 12144  df-xadd 12145  df-xmul 12146  df-topgen 16305  df-psmet 19946  df-xmet 19947  df-bl 19949  df-mopn 19950  df-bases 20964

This theorem is referenced by:  metequiv  22527  metss2  22530