Theorem metcnss2 7896

Description: Subset relationship for continuity of metric spaces.

Hypotheses

Ref	Expression
metcnss2.1	|- X = dom dom B
metcnss2.2	|- J = (Open` B)
metcnss2.3	|- K = (Open` C)
metcnss2.4	|- L = (Open` D)

Assertion

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

Proof of Theorem metcnss2

Step	Hyp	Ref	Expression
1		fssres 3649	. . . . . . . . 9 |- ((F:dom dom C-->dom dom D /\ X (_ dom dom C) -> (F |` X):X-->dom dom D)
2		metcnss2.1	. . . . . . . . . 10 |- X = dom dom B
3		eqid 1478	. . . . . . . . . 10 |- dom dom C = dom dom C
4	2, 3	metss 7821	. . . . . . . . 9 |- (B (_ C -> X (_ dom dom C)
5	1, 4	sylan2 453	. . . . . . . 8 |- ((F:dom dom C-->dom dom D /\ B (_ C) -> (F |` X):X-->dom dom D)
6	5	expcom 374	. . . . . . 7 |- (B (_ C -> (F:dom dom C-->dom dom D -> (F |` X):X-->dom dom D))
7	6	adantl 390	. . . . . 6 |- (((B e. Met /\ C e. Met) /\ B (_ C) -> (F:dom dom C-->dom dom D -> (F |` X):X-->dom dom D))
8		ssralv 2117	. . . . . . . . 9 |- (X (_ dom dom C -> (A.x e. dom dom CA.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. dom dom C((xCw) < z -> ((F` x)D(F` w)) < y))) -> A.x e. X A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. dom dom C((xCw) < z -> ((F` x)D(F` w)) < y)))))
9	4, 8	syl 10	. . . . . . . 8 |- (B (_ C -> (A.x e. dom dom CA.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. dom dom C((xCw) < z -> ((F` x)D(F` w)) < y))) -> A.x e. X A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. dom dom C((xCw) < z -> ((F` x)D(F` w)) < y)))))
10	9	adantl 390	. . . . . . 7 |- (((B e. Met /\ C e. Met) /\ B (_ C) -> (A.x e. dom dom CA.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. dom dom C((xCw) < z -> ((F` x)D(F` w)) < y))) -> A.x e. X A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. dom dom C((xCw) < z -> ((F` x)D(F` w)) < y)))))
11		ssralv 2117	. . . . . . . . . . . . . . 15 |- (X (_ dom dom C -> (A.w e. dom dom C((xCw) < z -> ((F` x)D(F` w)) < y) -> A.w e. X ((xCw) < z -> ((F` x)D(F` w)) < y)))
12	4, 11	syl 10	. . . . . . . . . . . . . 14 |- (B (_ C -> (A.w e. dom dom C((xCw) < z -> ((F` x)D(F` w)) < y) -> A.w e. X ((xCw) < z -> ((F` x)D(F` w)) < y)))
13	12	ad2antlr 407	. . . . . . . . . . . . 13 |- ((((B e. Met /\ C e. Met) /\ B (_ C) /\ x e. X) -> (A.w e. dom dom C((xCw) < z -> ((F` x)D(F` w)) < y) -> A.w e. X ((xCw) < z -> ((F` x)D(F` w)) < y)))
14	2	metf 7804	. . . . . . . . . . . . . . . . . . . . . . 23 |- (B e. Met -> B:(X X. X)-->RR)
15		fdm 3637	. . . . . . . . . . . . . . . . . . . . . . 23 |- (B:(X X. X)-->RR -> dom B = (X X. X))
16		reseq2 3375	. . . . . . . . . . . . . . . . . . . . . . 23 |- (dom B = (X X. X) -> (C |` dom B) = (C |` (X X. X)))
17	14, 15, 16	3syl 20	. . . . . . . . . . . . . . . . . . . . . 22 |- (B e. Met -> (C |` dom B) = (C |` (X X. X)))
18	17	ad2antrr 406	. . . . . . . . . . . . . . . . . . . . 21 |- (((B e. Met /\ C e. Met) /\ B (_ C) -> (C |` dom B) = (C |` (X X. X)))
19		funssres 3558	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((Fun C /\ B (_ C) -> (C |` dom B) = B)
20	3	metf 7804	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (C e. Met -> C:(dom dom C X. dom dom C)-->RR)
21		ffun 3635	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (C:(dom dom C X. dom dom C)-->RR -> Fun C)
22	20, 21	syl 10	. . . . . . . . . . . . . . . . . . . . . . 23 |- (C e. Met -> Fun C)
23	19, 22	sylan 450	. . . . . . . . . . . . . . . . . . . . . 22 |- ((C e. Met /\ B (_ C) -> (C |` dom B) = B)
24	23	adantll 394	. . . . . . . . . . . . . . . . . . . . 21 |- (((B e. Met /\ C e. Met) /\ B (_ C) -> (C |` dom B) = B)
25	18, 24	eqtr3d 1512	. . . . . . . . . . . . . . . . . . . 20 |- (((B e. Met /\ C e. Met) /\ B (_ C) -> (C |` (X X. X)) = B)
26	25	opreqd 3983	. . . . . . . . . . . . . . . . . . 19 |- (((B e. Met /\ C e. Met) /\ B (_ C) -> (x(C |` (X X. X))w) = (xBw))
27	26	ad2antrr 406	. . . . . . . . . . . . . . . . . 18 |- (((((B e. Met /\ C e. Met) /\ B (_ C) /\ x e. X) /\ w e. X) -> (x(C |` (X X. X))w) = (xBw))
28		oprvalres 4039	. . . . . . . . . . . . . . . . . . 19 |- ((x e. X /\ w e. X) -> (x(C |` (X X. X))w) = (xCw))
29	28	adantll 394	. . . . . . . . . . . . . . . . . 18 |- (((((B e. Met /\ C e. Met) /\ B (_ C) /\ x e. X) /\ w e. X) -> (x(C |` (X X. X))w) = (xCw))
30	27, 29	eqtr3d 1512	. . . . . . . . . . . . . . . . 17 |- (((((B e. Met /\ C e. Met) /\ B (_ C) /\ x e. X) /\ w e. X) -> (xBw) = (xCw))
31	30	breq1d 2634	. . . . . . . . . . . . . . . 16 |- (((((B e. Met /\ C e. Met) /\ B (_ C) /\ x e. X) /\ w e. X) -> ((xBw) < z <-> (xCw) < z))
32		fvres 3740	. . . . . . . . . . . . . . . . . . 19 |- (x e. X -> ((F |` X)` x) = (F` x))
33		fvres 3740	. . . . . . . . . . . . . . . . . . 19 |- (w e. X -> ((F |` X)` w) = (F` w))
34	32, 33	opreqan12d 3985	. . . . . . . . . . . . . . . . . 18 |- ((x e. X /\ w e. X) -> (((F |` X)` x)D((F |` X)` w)) = ((F` x)D(F` w)))
35	34	breq1d 2634	. . . . . . . . . . . . . . . . 17 |- ((x e. X /\ w e. X) -> ((((F |` X)` x)D((F |` X)` w)) < y <-> ((F` x)D(F` w)) < y))
36	35	adantll 394	. . . . . . . . . . . . . . . 16 |- (((((B e. Met /\ C e. Met) /\ B (_ C) /\ x e. X) /\ w e. X) -> ((((F |` X)` x)D((F |` X)` w)) < y <-> ((F` x)D(F` w)) < y))
37	31, 36	imbi12d 628	. . . . . . . . . . . . . . 15 |- (((((B e. Met /\ C e. Met) /\ B (_ C) /\ x e. X) /\ w e. X) -> (((xBw) < z -> (((F |` X)` x)D((F |` X)` w)) < y) <-> ((xCw) < z -> ((F` x)D(F` w)) < y)))
38	37	biimprd 154	. . . . . . . . . . . . . 14 |- (((((B e. Met /\ C e. Met) /\ B (_ C) /\ x e. X) /\ w e. X) -> (((xCw) < z -> ((F` x)D(F` w)) < y) -> ((xBw) < z -> (((F |` X)` x)D((F |` X)` w)) < y)))
39	38	r19.20dva 1712	. . . . . . . . . . . . 13 |- ((((B e. Met /\ C e. Met) /\ B (_ C) /\ x e. X) -> (A.w e. X ((xCw) < z -> ((F` x)D(F` w)) < y) -> A.w e. X ((xBw) < z -> (((F |` X)` x)D((F |` X)` w)) < y)))
40	13, 39	syld 27	. . . . . . . . . . . 12 |- ((((B e. Met /\ C e. Met) /\ B (_ C) /\ x e. X) -> (A.w e. dom dom C((xCw) < z -> ((F` x)D(F` w)) < y) -> A.w e. X ((xBw) < z -> (((F |` X)` x)D((F |` X)` w)) < y)))
41	40	anim2d 563	. . . . . . . . . . 11 |- ((((B e. Met /\ C e. Met) /\ B (_ C) /\ x e. X) -> ((0 < z /\ A.w e. dom dom C((xCw) < z -> ((F` x)D(F` w)) < y)) -> (0 < z /\ A.w e. X ((xBw) < z -> (((F |` X)` x)D((F |` X)` w)) < y))))
42	41	r19.22sdv 1741	. . . . . . . . . 10 |- ((((B e. Met /\ C e. Met) /\ B (_ C) /\ x e. X) -> (E.z e. RR (0 < z /\ A.w e. dom dom C(