Theorem metcnss 7907

Description: Subset relationship for continuity of metric spaces.

Hypotheses

Ref	Expression
metcnco.1	|- J = (Open` B)
metcnco.2	|- K = (Open` C)
metcnco.3	|- L = (Open` D)

Assertion

Ref	Expression
metcnss	|- (((B e. Met /\ C e. Met /\ D e. Met) /\ C (_ D) -> (J Cn K) (_ (J Cn L))

Proof of Theorem metcnss

Step	Hyp	Ref	Expression
1		fss 3649	. . . . . . . . 9 |- ((f:dom dom B-->dom dom C /\ dom dom C (_ dom dom D) -> f:dom dom B-->dom dom D)
2		eqid 1482	. . . . . . . . . 10 |- dom dom C = dom dom C
3		eqid 1482	. . . . . . . . . 10 |- dom dom D = dom dom D
4	2, 3	metss 7833	. . . . . . . . 9 |- (C (_ D -> dom dom C (_ dom dom D)
5	1, 4	sylan2 454	. . . . . . . 8 |- ((f:dom dom B-->dom dom C /\ C (_ D) -> f:dom dom B-->dom dom D)
6	5	expcom 374	. . . . . . 7 |- (C (_ D -> (f:dom dom B-->dom dom C -> f:dom dom B-->dom dom D))
7	6	adantl 390	. . . . . 6 |- (((C e. Met /\ D e. Met) /\ C (_ D) -> (f:dom dom B-->dom dom C -> f:dom dom B-->dom dom D))
8	7	adantrd 393	. . . . 5 |- (((C e. Met /\ D e. Met) /\ C (_ D) -> ((f:dom dom B-->dom dom C /\ A.x e. dom dom BA.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. dom dom B((xBw) < z -> ((f` x)C(f` w)) < y)))) -> f:dom dom B-->dom dom D))
9		oprvalres 4047	. . . . . . . . . . . . . . . . . 18 |- (((f` x) e. dom dom C /\ (f` w) e. dom dom C) -> ((f` x)(D |` (dom dom C X. dom dom C))(f` w)) = ((f` x)D(f` w)))
10		ffvelrn 3828	. . . . . . . . . . . . . . . . . . 19 |- ((f:dom dom B-->dom dom C /\ x e. dom dom B) -> (f` x) e. dom dom C)
11	10	adantr 391	. . . . . . . . . . . . . . . . . 18 |- (((f:dom dom B-->dom dom C /\ x e. dom dom B) /\ w e. dom dom B) -> (f` x) e. dom dom C)
12		ffvelrn 3828	. . . . . . . . . . . . . . . . . . 19 |- ((f:dom dom B-->dom dom C /\ w e. dom dom B) -> (f` w) e. dom dom C)
13	12	adantlr 395	. . . . . . . . . . . . . . . . . 18 |- (((f:dom dom B-->dom dom C /\ x e. dom dom B) /\ w e. dom dom B) -> (f` w) e. dom dom C)
14	9, 11, 13	sylanc 474	. . . . . . . . . . . . . . . . 17 |- (((f:dom dom B-->dom dom C /\ x e. dom dom B) /\ w e. dom dom B) -> ((f` x)(D |` (dom dom C X. dom dom C))(f` w)) = ((f` x)D(f` w)))
15	14	adantlll 398	. . . . . . . . . . . . . . . 16 |- ((((((C e. Met /\ D e. Met) /\ C (_ D) /\ f:dom dom B-->dom dom C) /\ x e. dom dom B) /\ w e. dom dom B) -> ((f` x)(D |` (dom dom C X. dom dom C))(f` w)) = ((f` x)D(f` w)))
16	2	metf 7816	. . . . . . . . . . . . . . . . . . . . . 22 |- (C e. Met -> C:(dom dom C X. dom dom C)-->RR)
17		fdm 3645	. . . . . . . . . . . . . . . . . . . . . 22 |- (C:(dom dom C X. dom dom C)-->RR -> dom C = (dom dom C X. dom dom C))
18		reseq2 3383	. . . . . . . . . . . . . . . . . . . . . 22 |- (dom C = (dom dom C X. dom dom C) -> (D |` dom C) = (D |` (dom dom C X. dom dom C)))
19	16, 17, 18	3syl 20	. . . . . . . . . . . . . . . . . . . . 21 |- (C e. Met -> (D |` dom C) = (D |` (dom dom C X. dom dom C)))
20	19	ad2antrr 406	. . . . . . . . . . . . . . . . . . . 20 |- (((C e. Met /\ D e. Met) /\ C (_ D) -> (D |` dom C) = (D |` (dom dom C X. dom dom C)))
21		funssres 3566	. . . . . . . . . . . . . . . . . . . . . 22 |- ((Fun D /\ C (_ D) -> (D |` dom C) = C)
22	3	metf 7816	. . . . . . . . . . . . . . . . . . . . . . 23 |- (D e. Met -> D:(dom dom D X. dom dom D)-->RR)
23		ffun 3643	. . . . . . . . . . . . . . . . . . . . . . 23 |- (D:(dom dom D X. dom dom D)-->RR -> Fun D)
24	22, 23	syl 10	. . . . . . . . . . . . . . . . . . . . . 22 |- (D e. Met -> Fun D)
25	21, 24	sylan 451	. . . . . . . . . . . . . . . . . . . . 21 |- ((D e. Met /\ C (_ D) -> (D |` dom C) = C)
26	25	adantll 394	. . . . . . . . . . . . . . . . . . . 20 |- (((C e. Met /\ D e. Met) /\ C (_ D) -> (D |` dom C) = C)
27	20, 26	eqtr3d 1516	. . . . . . . . . . . . . . . . . . 19 |- (((C e. Met /\ D e. Met) /\ C (_ D) -> (D |` (dom dom C X. dom dom C)) = C)
28	27	adantr 391	. . . . . . . . . . . . . . . . . 18 |- ((((C e. Met /\ D e. Met) /\ C (_ D) /\ f:dom dom B-->dom dom C) -> (D |` (dom dom C X. dom dom C)) = C)
29	28	ad2antrr 406	. . . . . . . . . . . . . . . . 17 |- ((((((C e. Met /\ D e. Met) /\ C (_ D) /\ f:dom dom B-->dom dom C) /\ x e. dom dom B) /\ w e. dom dom B) -> (D |` (dom dom C X. dom dom C)) = C)
30	29	opreqd 3991	. . . . . . . . . . . . . . . 16 |- ((((((C e. Met /\ D e. Met) /\ C (_ D) /\ f:dom dom B-->dom dom C) /\ x e. dom dom B) /\ w e. dom dom B) -> ((f` x)(D |` (dom dom C X. dom dom C))(f` w)) = ((f` x)C(f` w)))
31	15, 30	eqtr3d 1516	. . . . . . . . . . . . . . 15 |- ((((((C e. Met /\ D e. Met) /\ C (_ D) /\ f:dom dom B-->dom dom C) /\ x e. dom dom B) /\ w e. dom dom B) -> ((f` x)D(f` w)) = ((f` x)C(f` w)))
32	31	breq1d 2642	. . . . . . . . . . . . . 14 |- ((((((C e. Met /\ D e. Met) /\ C (_ D) /\ f:dom dom B-->dom dom C) /\ x e. dom dom B) /\ w e. dom dom B) -> (((f` x)D(f` w)) < y <-> ((f` x)C(f` w)) < y))
33	32	imbi2d 615	. . . . . . . . . . . . 13 |- ((((((C e. Met /\ D e. Met) /\ C (_ D) /\ f:dom dom B-->dom dom C) /\ x e. dom dom B) /\ w e. dom dom B) -> (((xBw) < z -> ((f` x)D(f` w)) < y) <-> ((xBw) < z -> ((f` x)C(f` w)) < y)))
34	33	ralbidva 1666	. . . . . . . . . . . 12 |- (((((C e. Met /\ D e. Met) /\ C (_ D) /\ f:dom dom B-->dom dom C) /\ x e. dom dom B) -> (A.w e. dom dom B((xBw) < z -> ((f` x)D(f` w)) < y) <-> A.w e. dom dom B((xBw) < z -> ((f` x)C(f` w)) < y)))
35	34	anbi2d 619	. . . . . . . . . . 11 |- (((((C e. Met /\ D e. Met) /\ C (_ D) /\ f:dom dom B-->dom dom C) /\ x e. dom dom B) -> ((0 < z /\ A.w e. dom dom B((xBw) < z -> ((f` x)D(f` w)) < y)) <-> (0 < z /\ A.w e. dom dom B((xBw) < z -> ((f` x)C(f` w)) < y))))
36	35	rexbidv 1671	. . . . . . . . . 10 |- (((((C e. Met /\ D e. Met) /\ C (_ D) /\ f:dom dom B-->dom dom C) /\ x e. dom dom B) -> (E.z e. RR (0 < z /\ A.w e. dom dom B((xBw) < z -> ((f` x)D(f` w)) < y)) <-> E.z e. RR (0 < z /\ A.w e. dom dom B((xBw) < z -> ((f` x)C(f` w)) < y))))
37	36	imbi2d 615	. . . . . . . . 9 |- (((((C e. Met /\ D e. Met) /\ C (_ D) /\ f:dom dom B-->dom dom C) /\ x e. dom dom B) -> ((0 < y -> E.z e. RR (0 < z /\ A.w e. dom dom B((xBw) < z -> ((f` x)D(f` w)) < y))) <-> (0 < y -> E.z e. RR (0 < z /\ A.w e. dom dom B((xBw) < z -> ((f` x)C(f` w)) < y)))))
38	37	ralbidv 1670	. . . . . . . 8 |- (((((C e. Met /\ D e. Met) /\ C (_ D) /\ f:dom dom B-->dom dom C) /\ x e. dom dom B) -> (A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. dom dom B((xBw) < z -> ((f` x)D(f` w)) < y))) <-> A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. dom dom B((xBw) < z -> ((f` x)C(f` w)) < y)))))
39	38	ralbidva 1666	. . . . . . 7 |- ((((C e. Met /\ D e. Met) /\ C (_ D) /\ f:dom dom B-->dom dom C) -> (A.x e. dom dom BA.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. dom dom B((xBw) < z