Theorem subtopmetlem 11093

Description: Lemma for subtopmet 11094. (Contributed by Jeff Hankins, 21-Aug-2009.)

Hypotheses

Ref	Expression
subtopmet.1	|- D = (C |` (Y X. Y))
subtopmet.2	|- X = dom dom C
subtopmet.j	|- J = (MetOpen` C)
subtopmet.k	|- K = (MetOpen` D)
subtopmet.a	|- A e. _V

Assertion

Ref	Expression
subtopmetlem	|- ((C e. Met /\ Y C_ X) -> (A e. (subSp` <.Y, J>.) -> A e. K))

Proof of Theorem subtopmetlem

Step	Hyp	Ref	Expression
1		inss2 3027	. . . . . . . 8 |- (y i^i Y) C_ Y
2		sseq1 2865	. . . . . . . 8 |- (A = (y i^i Y) -> (A C_ Y <-> (y i^i Y) C_ Y))
3	1, 2	mpbiri 321	. . . . . . 7 |- (A = (y i^i Y) -> A C_ Y)
4	3	3ad2ant3 1143	. . . . . 6 |- (((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) -> A C_ Y)
5		subtopmet.1	. . . . . . . 8 |- D = (C |` (Y X. Y))
6		subtopmet.2	. . . . . . . 8 |- X = dom dom C
7	5, 6	basmetres 11018	. . . . . . 7 |- ((C e. Met /\ Y C_ X) -> Y = dom dom D)
8	7	3ad2ant1 1141	. . . . . 6 |- (((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) -> Y = dom dom D)
9	4, 8	sseqtrd 2880	. . . . 5 |- (((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) -> A C_ dom dom D)
10		simpl1l 1171	. . . . . . . 8 |- ((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A) -> C e. Met)
11		simp2 1121	. . . . . . . . 9 |- (((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) -> y e. J)
12	11	adantr 447	. . . . . . . 8 |- ((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A) -> y e. J)
13		inss1 3026	. . . . . . . . . . 11 |- (y i^i Y) C_ y
14		sseq1 2865	. . . . . . . . . . 11 |- (A = (y i^i Y) -> (A C_ y <-> (y i^i Y) C_ y))
15	13, 14	mpbiri 321	. . . . . . . . . 10 |- (A = (y i^i Y) -> A C_ y)
16	15	3ad2ant3 1143	. . . . . . . . 9 |- (((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) -> A C_ y)
17		ssel2 2847	. . . . . . . . 9 |- ((A C_ y /\ x e. A) -> x e. y)
18	16, 17	sylan 597	. . . . . . . 8 |- ((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A) -> x e. y)
19		subtopmet.j	. . . . . . . . 9 |- J = (MetOpen` C)
20	19	opni2 10008	. . . . . . . 8 |- ((C e. Met /\ y e. J /\ x e. y) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ y))
21	10, 12, 18, 20	syl111anc 1349	. . . . . . 7 |- ((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ y))
22		metres 9966	. . . . . . . . . . . . . . . . 17 |- (C e. Met -> (C |` (Y X. Y)) e. Met)
23	5, 22	syl5eqel 2222	. . . . . . . . . . . . . . . 16 |- (C e. Met -> D e. Met)
24	23	adantr 447	. . . . . . . . . . . . . . 15 |- ((C e. Met /\ Y C_ X) -> D e. Met)
25	24	3ad2ant1 1141	. . . . . . . . . . . . . 14 |- (((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) -> D e. Met)
26	25	3ad2ant1 1141	. . . . . . . . . . . . 13 |- ((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) -> D e. Met)
27	26	adantr 447	. . . . . . . . . . . 12 |- (((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) -> D e. Met)
28		ssel2 2847	. . . . . . . . . . . . . . . 16 |- ((A C_ Y /\ x e. A) -> x e. Y)
29	28	3adant3 1140	. . . . . . . . . . . . . . 15 |- ((A C_ Y /\ x e. A /\ r e. RR) -> x e. Y)
30	4, 29	syl3an1 1382	. . . . . . . . . . . . . 14 |- ((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) -> x e. Y)
31	30	adantr 447	. . . . . . . . . . . . 13 |- (((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) -> x e. Y)
32	8	3ad2ant1 1141	. . . . . . . . . . . . . 14 |- ((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) -> Y = dom dom D)
33	32	adantr 447	. . . . . . . . . . . . 13 |- (((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) -> Y = dom dom D)
34	31, 33	eleqtrd 2220	. . . . . . . . . . . 12 |- (((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) -> x e. dom dom D)
35		simp3 1122	. . . . . . . . . . . . 13 |- ((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) -> r e. RR)
36	35	adantr 447	. . . . . . . . . . . 12 |- (((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) -> r e. RR)
37		simprl 812	. . . . . . . . . . . 12 |- (((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) -> 0 < r)
38		eqid 2141	. . . . . . . . . . . . 13 |- dom dom D = dom dom D
39	38	blelrn 9991	. . . . . . . . . . . 12 |- (((D e. Met /\ x e. dom dom D) /\ (r e. RR /\ 0 < r)) -> (x( ball ` D)r) e. ran ( ball ` D))
40	27, 34, 36, 37, 39	syl22anc 1350	. . . . . . . . . . 11 |- (((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) -> (x( ball ` D)r) e. ran ( ball ` D))
41	38	blcntr 9988	. . . . . . . . . . . 12 |- (((D e. Met /\ x e. dom dom D) /\ (r e. RR /\ 0 < r)) -> x e. (x( ball ` D)r))
42	27, 34, 36, 37, 41	syl22anc 1350	. . . . . . . . . . 11 |- (((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) -> x e. (x( ball ` D)r))
43		simplrr 817	. . . . . . . . . . . . . . . . 17 |- ((((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) /\ (z e. dom dom D /\ (xDz) < r)) -> (x( ball ` C)r) C_ y)
44	6	metf 9950	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (C e. Met -> C:(X X. X)-->RR)
45		ffun 4661	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (C:(X X. X)-->RR -> Fun C)
46	44, 45	syl 13	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (C e. Met -> Fun C)
47	46	adantr 447	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((C e. Met /\ Y C_ X) -> Fun C)
48	47	3ad2ant1 1141	. . . . . . . . . . . . . . . . . . . . . 22 |- (((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) -> Fun C)
49	48	3ad2ant1 1141	. . . . . . . . . . . . . . . . . . . . 21 |- ((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) -> Fun C)
50	49	ad2antrr 799	. . . . . . . . . . . . . . . . . . . 20 |- ((((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) /\ (z e. dom dom D /\ (xDz) < r)) -> Fun C)
51		resss 4359	. . . . . . . . . . . . . . . . . . . . . . 23 |- (C |` (Y X. Y)) C_ C
52	5, 51	eqsstri 2874	. . . . . . . . . . . . . . . . . . . . . 22 |- D C_ C
53		funss 4543	. . . . . . . . . . . . . . . . . . . . . 22 |- (D C_ C -> (Fun C -> Fun D))
54	52, 50, 53	mpsyl 112	. . . . . . . . . . . . . . . . . . . . 21 |- ((((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) /\ (z e. dom dom D /\ (xDz) < r)) -> Fun D)
55	5	dmeqi 4284	. . . . . . . . . . . . . . . . . . . . . . 23 |- dom D = dom ( C |` (Y X. Y))
56		dmres 4356	. . . . . . . . . . . . . . . . . . . . . . 23 |- dom ( C |` (Y X. Y)) = ((Y X. Y) i^i dom C)
57	55, 56	eqtri 2161	. . . . . . . . . . . . . . . . . . . . . 22 |- dom D = ((Y X. Y) i^i dom C)
58		simp11r 1232	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) -> Y C_ X)
59	58	ad2antrr 799	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) /\ (z e. dom dom D /\ (xDz) < r)) -> Y C_ X)
60		xpss12 4220	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((Y C_ X /\ Y C_ X) -> (Y X. Y) C_ (X X. X))
61	59, 59, 60	syl11anc 659	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) /\ (z e. dom dom D /\ (xDz) < r)) -> (Y X. Y) C_ (X X. X))
62		fdm 4663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (C:(X X. X)-->RR -> dom C = (X X. X))
63	44, 62	syl 13	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (C e. Met -> dom C = (X X. X))
64	63	adantr 447	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((C e. Met /\ Y C_ X) -> dom C = (X X. X))
65	64	3ad2ant1 1141	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) -> dom C = (X X. X))
66	65	3ad2ant1 1141	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) -> dom C = (X X. X))
67	66	ad2antrr 799	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) /\ (z e. dom dom D /\ (xDz) < r)) -> dom C = (X X. X))
68	61, 67	sseqtr4d 2881	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) /\ (z e. dom dom D /\ (xDz) < r)) -> (Y X. Y) C_ dom C)
69		df-ss 2836	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((Y X. Y) C_ dom C <-> ((Y X. Y) i^i dom C) = (Y X. Y))
70	68, 69	sylib 242	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) /\ (z e. dom dom D /\ (xDz) < r)) -> ((Y X. Y) i^i dom C) = (Y X. Y))
71	57, 70	syl5eq 2185	. . . . . . . . . . . . . . . . . . . . 21 |- ((((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) /\ (z e. dom dom D /\ (xDz) < r)) -> dom D = (Y X. Y))
72		df-fn 4142	. . . . . . . . . . . . . . . . . . . . 21 |- (D Fn (Y X. Y) <-> (Fun D /\ dom D = (Y X. Y)))
73	54, 71, 72	sylanbrc 664	. . . . . . . . . . . . . . . . . . . 20 |- ((((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) /\ (z e. dom dom D /\ (xDz) < r)) -> D Fn (Y X. Y))
74	52	a1i 8	. . . . . . . . . . . . . . . . . . . 20 |- ((((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) /\ (z e. dom dom D /\ (xDz) < r)) -> D C_ C)
75	30	ad2antrr 799	. . . . . . . . . . . . . . . . . . . 20 |- ((((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) /\ (z e. dom dom D /\ (xDz) < r)) -> x e. Y)
76		eqimss2 2895	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (Y = dom dom D -> dom dom D C_ Y)
77	33, 76	syl 13	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) -> dom dom D C_ Y)
78	77	sseld 2850	. . . . . . . . . . . . . . . . . . . . . 22 |- (((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) -> (z e. dom dom D -> z e. Y))
79	78	imp 393	. . . . . . . . . . . . . . . . . . . . 21 |- ((((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) /\ z e. dom dom D) -> z e. Y)
80	79	adantrr 781	. . . . . . . . . . . . . . . . . . . 20 |- ((((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) /\ (z e. dom dom D /\ (xDz) < r)) -> z e. Y)
81		oprssoprv 5058	. . . . . . . . . . . . . . . . . . . 20 |- (((Fun C /\ D Fn (Y X. Y) /\ D C_ C) /\ (x e. Y /\ z e. Y)) -> (xCz) = (xDz))
82	50, 73, 74, 75, 80, 81	syl32anc 1357	. . . . . . . . . . . . . . . . . . 19 |- ((((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) /\ (z e. dom dom D /\ (xDz) < r)) -> (xCz) = (xDz))
83		simprr 813	. . . . . . . . . . . . . . . . . . 19 |- ((((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) /\ (z e. dom dom D /\ (xDz) < r)) -> (xDz) < r)
84	82, 83	eqbrtrd 3527	. . . . . . . . . . . . . . . . . 18 |- ((((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) /\ (z e. dom dom D /\ (xDz) < r)) -> (xCz) < r)
85		simp11l 1231	. . . . . . . . . . . . . . . . . . . 20 |- ((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) -> C e. Met)
86	85	ad2antrr 799	. . . . . . . . . . . . . . . . . . 19 |- ((((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) /\ (z e. dom dom D /\ (xDz) < r)) -> C e. Met)
87	59, 75	sseldd 2851	. . . . . . . . . . . . . . . . . . 19 |- ((((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) /\ (z e. dom dom D /\ (xDz) < r)) -> x e. X)
88		dmss 4282	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (D C_ C -> dom D C_ dom C)
89	52, 88	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . 23 |- dom D C_ dom C
90		dmss 4282	. . . . . . . . . . . . . . . . . . . . . . 23 |- (dom D C_ dom C -> dom dom D C_ dom dom C)
91	89, 90	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . 22 |- dom dom D C_ dom dom C
92	91	sseli 2848	. . . . . . . . . . . . . . . . . . . . 21 |- (z e. dom dom D -> z e. dom dom C)
93	92, 6	syl6eleqr 2233	. . . . . . . . . . . . . . . . . . . 20 |- (z e. dom dom D -> z e. X)
94	93	ad2antrl 804	. . . . . . . . . . . . . . . . . . 19 |- ((((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) /\ (z e. dom dom D /\ (xDz) < r)) -> z e. X)
95		simpll3 1161	. . . . . . . . . . . . . . . . . . 19 |- ((((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) /\ (z e. dom dom D /\ (xDz) < r)) -> r e. RR)
96		simplrl 816	. . . . . . . . . . . . . . . . . . 19 |- ((((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) /\ (z e. dom dom D /\ (xDz) < r)) -> 0 < r)
97	6	elbl2 9982	. . . . . . . . . . . . . . . . . . 19 |- (((C e. Met /\ x e. X /\ z e. X) /\ (r e. RR /\ 0 < r)) -> (z e. (x( ball ` C)r) <-> (xCz) < r))
98	86, 87, 94, 95, 96, 97	syl32anc 1357	. . . . . . . . . . . . . . . . . 18 |- ((((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) /\ (z e. dom dom D /\ (xDz) < r)) -> (z e. (x( ball ` C)r) <-> (xCz) < r))
99	84, 98	mpbird 318	. . . . . . . . . . . . . . . . 17 |- ((((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) /\ (z e. dom dom D /\ (xDz) < r)) -> z e. (x( ball ` C)r))
100	43, 99	sseldd 2851	. . . . . . . . . . . . . . . 16 |- ((((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) /\ (z e. dom dom D /\ (xDz) < r)) -> z e. y)
101	100	ex 398	. . . . . . . . . . . . . . 15 |- (((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) -> ((z e. dom dom D /\ (xDz) < r) -> z e. y))
102	57	dmeqi 4284	. . . . . . . . . . . . . . . . . 18 |- dom dom D = dom ((Y X. Y) i^i dom C)
103		inss1 3026	. . . . . . . . . . . . . . . . . . . . 21 |- ((Y X. Y) i^i dom C) C_ (Y X. Y)
104		dmss 4282	. . . . . . . . . . . . . . . . . . . . 21 |- (((Y X. Y) i^i dom C) C_ (Y X. Y) -> dom ((Y X. Y) i^i dom C) C_ dom ( Y X. Y))
105	103, 104	ax-mp 7	. . . . . . . . . . . . . . . . . . . 20 |- dom ((Y X. Y) i^i dom C) C_ dom ( Y X. Y)
106	105	a1i 8	. . . . . . . . . . . . . . . . . . 19 |- (((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) -> dom ((Y X. Y) i^i dom C) C_ dom ( Y X. Y))
107		dmxpid 4301	. . . . . . . . . . . . . . . . . . 19 |- dom ( Y X. Y) = Y
108	106, 107	syl6sseq 2892	. . . . . . . . . . . . . . . . . 18 |- (((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) -> dom ((Y X. Y) i^i dom C) C_ Y)
109	102, 108	syl5eqss 2888	. . . . . . . . . . . . . . . . 17 |- (((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) -> dom dom D C_ Y)
110	109	sseld 2850	. . . . . . . . . . . . . . . 16 |- (((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) -> (z e. dom dom D -> z e. Y))
111	110	adantrd 452	. . . . . . . . . . . . . . 15 |- (((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) -> ((z e. dom dom D /\ (xDz) < r) -> z e. Y))
112	101, 111	jcad 496	. . . . . . . . . . . . . 14 |- (((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) -> ((z e. dom dom D /\ (xDz) < r) -> (z e. y /\ z e. Y)))
113		elin 2999	. . . . . . . . . . . . . 14 |- (z e. (y i^i Y) <-> (z e. y /\ z e. Y))
114	112, 113	syl6ibr 262	. . . . . . . . . . . . 13 |- (((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) -> ((z e. dom dom D /\ (xDz) < r) -> z e. (y i^i Y)))
115	38	elbl 9981	. . . . . . . . . . . . . 14 |- (((D e. Met /\ x e. dom dom D) /\ (r e. RR /\ 0 < r)) -> (z e. (x( ball ` D)r) <-> (z e. dom dom D /\ (xDz) < r)))
116	27, 34, 36, 37, 115	syl22anc 1350	. . . . . . . . . . . . 13 |- (((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) -> (z e. (x( ball ` D)r) <-> (z e. dom dom D /\ (xDz) < r)))
117		simpl13 1197	. . . . . . . . . . . . . 14 |- (((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) -> A = (y i^i Y))
118	117	eleq2d 2211	. . . . . . . . . . . . 13 |- (((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) -> (z e. A <-> z e. (y i^i Y)))
119	114, 116, 118	3imtr4d 330	. . . . . . . . . . . 12 |- (((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) -> (z e. (x( ball ` D)r) -> z e. A))
120	119	ssrdv 2853	. . . . . . . . . . 11 |- (((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) -> (x( ball ` D)r) C_ A)
121		eleq2 2205	. . . . . . . . . . . . 13 |- (o = (x( ball ` D)r) -> (x e. o <-> x e. (x( ball ` D)r)))
122		sseq1 2865	. . . . . . . . . . . . 13 |- (o = (x( ball ` D)r) -> (o C_ A <-> (x( ball ` D)r) C_ A))
123	121, 122	anbi12d 763	. . . . . . . . . . . 12 |- (o = (x( ball ` D)r) -> ((x e. o /\ o C_ A) <-> (x e. (x( ball ` D)r) /\ (x( ball ` D)r) C_ A)))
124	123	rcla4ev 2620	. . . . . . . . . . 11 |- (((x( ball ` D)r) e. ran ( ball ` D) /\ (x e. (x( ball ` D)r) /\ (x( ball ` D)r) C_ A)) -> E.o e. ran ( ball ` D)(x e. o /\ o C_ A))
125	40, 42, 120, 124	syl12anc 1347	. . . . . . . . . 10 |- (((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) /\ (0 < r /\ (x( ball ` C)r) C_ y)) -> E.o e. ran ( ball ` D)(x e. o /\ o C_ A))
126	125	ex 398	. . . . . . . . 9 |- ((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A /\ r e. RR) -> ((0 < r /\ (x( ball ` C)r) C_ y) -> E.o e. ran ( ball ` D)(x e. o /\ o C_ A)))
127	126	3expia 1319	. . . . . . . 8 |- ((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A) -> (r e. RR -> ((0 < r /\ (x( ball ` C)r) C_ y) -> E.o e. ran ( ball ` D)(x e. o /\ o C_ A))))
128	127	r19.23adv 2463	. . . . . . 7 |- ((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A) -> (E.r e. RR (0 < r /\ (x( ball ` C)r) C_ y) -> E.o e. ran ( ball ` D)(x e. o /\ o C_ A)))
129	21, 128	mpd 11	. . . . . 6 |- ((((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) /\ x e. A) -> E.o e. ran ( ball ` D)(x e. o /\ o C_ A))
130	129	r19.21aiva 2426	. . . . 5 |- (((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) -> A.x e. A E.o e. ran ( ball ` D)(x e. o /\ o C_ A))
131	9, 130	jca 494	. . . 4 |- (((C e. Met /\ Y C_ X) /\ y e. J /\ A = (y i^i Y)) -> (A C_ dom dom D /\ A.x e. A E.o e. ran ( ball ` D)(x e. o /\ o C_ A)))
132	131	3exp 1316	. . 3 |- ((C e. Met /\ Y C_ X) -> (y e. J -> (A = (y i^i Y) -> (A C_ dom dom D /\ A.x e. A E.o e. ran ( ball ` D)(x e. o /\ o C_ A)))))
133	132	r19.23adv 2463	. 2 |- ((C e. Met /\ Y C_ X) -> (E.y e. J A = (y i^i Y) -> (A C_ dom dom D /\ A.x e. A E.o e. ran ( ball ` D)(x e. o /\ o C_ A))))
134	19	opntop 10013	. . . 4 |- (C e. Met -> J e. Top)
135	134	adantr 447	. . 3 |- ((C e. Met /\ Y C_ X) -> J e. Top)
136		subtopmet.a	. . . 4 |- A e. _V
137	136	a1i 8	. . 3 |- ((C e. Met /\ Y C_ X) -> A e. _V)
138	6	sseq2i 2869	. . . . 5 |- (Y C_ X <-> Y C_ dom dom C)
139		dmexg 4328	. . . . . . 7 |- (C e. Met -> dom C e. _V)
140		dmexg 4328	. . . . . . 7 |- (dom C e. _V -> dom dom C e. _V)
141	139, 140	syl 13	. . . . . 6 |- (C e. Met -> dom dom C e. _V)
142		ssexg 3624	. . . . . 6 |- ((Y C_ dom dom C /\ dom dom C e. _V) -> Y e. _V)
143	141, 142	sylan2 600	. . . . 5 |- ((Y C_ dom dom C /\ C e. Met) -> Y e. _V)
144	138, 143	sylanb 598	. . . 4 |- ((Y C_ X /\ C e. Met) -> Y e. _V)
145	144	ancoms 416	. . 3 |- ((C e. Met /\ Y C_ X) -> Y e. _V)
146		issubspt 11083	. . 3 |- ((J e. Top /\ A e. _V /\ Y e. _V) -> (A e. (subSp` <.Y, J>.) <-> E.y e. J A = (y i^i Y)))
147	135, 137, 145, 146	syl111anc 1349	. 2 |- ((C e. Met /\ Y C_ X) -> (A e. (subSp` <.Y, J>.) <-> E.y e. J A = (y i^i Y)))
148	22	adantr 447	. . . 4 |- ((C e. Met /\ Y C_ X) -> (C |` (Y X. Y)) e. Met)
149	5, 148	syl5eqel 2222	. . 3 |- ((C e. Met /\ Y C_ X) -> D e. Met)
150		subtopmet.k	. . . 4 |- K = (MetOpen` D)
151	38, 150	isopn 10002	. . 3 |- (D e. Met -> (A e. K <-> (A C_ dom dom D /\ A.x e. A E.o e. ran ( ball ` D)(x e. o /\ o C_ A))))
152	149, 151	syl 13	. 2 |- ((C e. Met /\ Y C_ X) -> (A e. K <-> (A C_ dom dom D /\ A.x e. A E.o e. ran ( ball ` D)(x e. o /\ o C_ A))))
153	133, 147, 152	3imtr4d 330	1 |- ((C e. Met /\ Y C_ X) -> (A e. (subSp` <.Y, J>.) -> A e. K))

Syntax hints:   -> wi 3   <-> wb 219   /\ wa 337   /\ w3a 1102   = wceq 1586   e. wcel 1588  A.wral 2355  E.wrex 2356  _Vcvv 2538   i^i cin 2826   C_ wss 2827  <.cop 3240   class class class wbr 3507   X. cxp 4117  dom cdm 4119  ran crn 4120   |` cres 4121  Fun wfun 4125   Fn wfn 4126  -->wf 4127  ` cfv 4131  (class class class)co 4981  RRcr 6751  0cc0 6752   < clt 6845  Topctop 9686  Metcme 9932   ball cbl 9934  MetOpencopn 9935  subSpcsubsp 11077

This theorem is referenced by:  subtopmet 11094

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-rep 3596  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929  ax-inf2 5964

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3or 1103  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-nel 2269  df-ral 2359  df-rex 2360  df-reu 2361  df-rab 2362  df-v 2540  df-sbc 2700  df-csb 2774  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-pss 2838  df-nul 3083  df-if 3181  df-pw 3229  df-sn 3242  df-pr 3243  df-tp 3245  df-op 3246  df-uni 3367  df-int 3401  df-iun 3438  df-br 3508  df-opab 3566  df-tr 3580  df-eprel 3744  df-id 3747  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-ord 3814  df-on 3815  df-lim 3816  df-suc 3817  df-om 4086  df-xp 4133  df-rel 4134  df-cnv 4135  df-co 4136  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fun 4141  df-fn 4142  df-f 4143  df-f1 4144  df-fo 4145  df-f1o 4146  df-fv 4147  df-opr 4983  df-oprab 4984  df-mpt 5099  df-1st 5126  df-2nd 5127  df-iota 5219  df-rdg 5304  df-1o 5344  df-oadd 5346  df-omul 5347  df-er 5479  df-ec 5481  df-qs 5484  df-en 5588  df-dom 5589  df-sdom 5590  df-undef 5725  df-riota 5729  df-ni 6518  df-pli 6519  df-mi 6520  df-lti 6521  df-plpq 6553  df-mpq 6554  df-enq 6555  df-nq 6556  df-plq 6557  df-mq 6558  df-rq 6559  df-ltq 6560  df-1q 6561  df-np 6604  df-1p 6605  df-plp 6606  df-mp 6607  df-ltp 6608  df-plpr 6682  df-mpr 6683  df-enr 6684  df-nr 6685  df-plr 6686  df-mr 6687  df-ltr 6688  df-0r 6689  df-1r 6690  df-m1r 6691  df-c 6758  df-0 6759  df-1 6760  df-i 6761  df-r 6762  df-plus 6763  df-mul 6764  df-lt 6765  df-pnf 6846  df-mnf 6847  df-xr 6848  df-ltxr 6849  df-le 6850  df-sub 7009  df-neg 7011  df-top 9692  df-met 9936  df-bl 9938  df-opn 9939  df-subsp 11078

Copyright terms: Public domain