Theorem ubthlem1 27726

Description: Lemma for ubth 27729. The function A exhibits a countable collection of sets that are closed, being the inverse image under t of the closed ball of radius k, and by assumption they cover X. Thus, by the Baire Category theorem bcth2 23127, for some n the set A ` n has an interior, meaning that there is a closed ball { z e. X | ( y D z ) <_ r } in the set. (Contributed by Mario Carneiro, 11-Jan-2014.) (New usage is discouraged.)

Hypotheses

Ref	Expression
ubth.1	|- X = ( BaseSet ` U )
ubth.2	|- N = ( normCV ` W )
ubthlem.3	|- D = ( IndMet ` U )
ubthlem.4	|- J = ( MetOpen ` D )
ubthlem.5	|- U e. CBan
ubthlem.6	|- W e. NrmCVec
ubthlem.7	|- ( ph -> T C_ ( U BLnOp W ) )
ubthlem.8	|- ( ph -> A. x e. X E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c )
ubthlem.9	|- A = ( k e. NN |-> { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } )

Assertion

Ref	Expression
ubthlem1	|- ( ph -> E. n e. NN E. y e. X E. r e. RR+ { z e. X | ( y D z ) <_ r } C_ ( A ` n ) )

Distinct variable groups:   k, c, n, r, x, y, z, A   t, c, D, k, n, r, x, z   k, J, n   y, t, J, x   N, c, k, n, r, t, x, y, z   ph, c, k, n, r, t, x, y   T, c, k, n, r, t, x, y, z   U, c, n, r, t, x, y, z   W, c, n, r, t, x, y   X, c, k, n, r, t, x, y, z

Allowed substitution hints:   ph( z)   A( t)   D( y)   U( k)   J( z, r, c)   W( z, k)

Proof of Theorem ubthlem1

Step	Hyp	Ref	Expression
1		rzal 4073	. . . . . . . . 9 |- ( T = (/) -> A. t e. T ( N ` ( t ` z ) ) <_ k )
2	1	ralrimivw 2967	. . . . . . . 8 |- ( T = (/) -> A. z e. X A. t e. T ( N ` ( t ` z ) ) <_ k )
3		rabid2 3118	. . . . . . . 8 |- ( X = { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } <-> A. z e. X A. t e. T ( N ` ( t ` z ) ) <_ k )
4	2, 3	sylibr 224	. . . . . . 7 |- ( T = (/) -> X = { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } )
5	4	eqcomd 2628	. . . . . 6 |- ( T = (/) -> { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } = X )
6	5	eleq1d 2686	. . . . 5 |- ( T = (/) -> ( { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } e. ( Clsd ` J ) <-> X e. ( Clsd ` J ) ) )
7		iinrab 4582	. . . . . . 7 |- ( T =/= (/) -> |^|_ t e. T { z e. X | ( N ` ( t ` z ) ) <_ k } = { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } )
8	7	adantl 482	. . . . . 6 |- ( ( ( ph /\ k e. NN ) /\ T =/= (/) ) -> |^|_ t e. T { z e. X | ( N ` ( t ` z ) ) <_ k } = { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } )
9		id 22	. . . . . . 7 |- ( T =/= (/) -> T =/= (/) )
10		ubthlem.7	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> T C_ ( U BLnOp W ) )
11	10	sselda 3603	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ t e. T ) -> t e. ( U BLnOp W ) )
12		ubthlem.3	. . . . . . . . . . . . . . . . . . . 20 |- D = ( IndMet ` U )
13		eqid 2622	. . . . . . . . . . . . . . . . . . . 20 |- ( IndMet ` W ) = ( IndMet ` W )
14		ubthlem.4	. . . . . . . . . . . . . . . . . . . 20 |- J = ( MetOpen ` D )
15		eqid 2622	. . . . . . . . . . . . . . . . . . . 20 |- ( MetOpen ` ( IndMet ` W ) ) = ( MetOpen ` ( IndMet ` W ) )
16		eqid 2622	. . . . . . . . . . . . . . . . . . . 20 |- ( U BLnOp W ) = ( U BLnOp W )
17		ubthlem.5	. . . . . . . . . . . . . . . . . . . . 21 |- U e. CBan
18		bnnv 27722	. . . . . . . . . . . . . . . . . . . . 21 |- ( U e. CBan -> U e. NrmCVec )
19	17, 18	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 |- U e. NrmCVec
20		ubthlem.6	. . . . . . . . . . . . . . . . . . . 20 |- W e. NrmCVec
21	12, 13, 14, 15, 16, 19, 20	blocn2 27663	. . . . . . . . . . . . . . . . . . 19 |- ( t e. ( U BLnOp W ) -> t e. ( J Cn ( MetOpen ` ( IndMet ` W ) ) ) )
22		ubth.1	. . . . . . . . . . . . . . . . . . . . . . . 24 |- X = ( BaseSet ` U )
23	22, 12	cbncms 27721	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( U e. CBan -> D e. ( CMet ` X ) )
24	17, 23	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 |- D e. ( CMet ` X )
25		cmetmet 23084	. . . . . . . . . . . . . . . . . . . . . 22 |- ( D e. ( CMet ` X ) -> D e. ( Met ` X ) )
26		metxmet 22139	. . . . . . . . . . . . . . . . . . . . . 22 |- ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
27	24, 25, 26	mp2b 10	. . . . . . . . . . . . . . . . . . . . 21 |- D e. ( *Met ` X )
28	14	mopntopon 22244	. . . . . . . . . . . . . . . . . . . . 21 |- ( D e. ( *Met ` X ) -> J e. (TopOn ` X ) )
29	27, 28	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 |- J e. (TopOn ` X )
30		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( BaseSet ` W ) = ( BaseSet ` W )
31	30, 13	imsxmet 27547	. . . . . . . . . . . . . . . . . . . . . 22 |- ( W e. NrmCVec -> ( IndMet ` W ) e. ( *Met ` ( BaseSet ` W ) ) )
32	20, 31	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 |- ( IndMet ` W ) e. ( *Met ` ( BaseSet ` W ) )
33	15	mopntopon 22244	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( IndMet ` W ) e. ( *Met ` ( BaseSet ` W ) ) -> ( MetOpen ` ( IndMet ` W ) ) e. (TopOn ` ( BaseSet ` W ) ) )
34	32, 33	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 |- ( MetOpen ` ( IndMet ` W ) ) e. (TopOn ` ( BaseSet ` W ) )
35		iscncl 21073	. . . . . . . . . . . . . . . . . . . 20 |- ( ( J e. (TopOn ` X ) /\ ( MetOpen ` ( IndMet ` W ) ) e. (TopOn ` ( BaseSet ` W ) ) ) -> ( t e. ( J Cn ( MetOpen ` ( IndMet ` W ) ) ) <-> ( t : X --> ( BaseSet ` W ) /\ A. x e. ( Clsd ` ( MetOpen ` ( IndMet ` W ) ) ) ( `' t " x ) e. ( Clsd ` J ) ) ) )
36	29, 34, 35	mp2an 708	. . . . . . . . . . . . . . . . . . 19 |- ( t e. ( J Cn ( MetOpen ` ( IndMet ` W ) ) ) <-> ( t : X --> ( BaseSet ` W ) /\ A. x e. ( Clsd ` ( MetOpen ` ( IndMet ` W ) ) ) ( `' t " x ) e. ( Clsd ` J ) ) )
37	21, 36	sylib 208	. . . . . . . . . . . . . . . . . 18 |- ( t e. ( U BLnOp W ) -> ( t : X --> ( BaseSet ` W ) /\ A. x e. ( Clsd ` ( MetOpen ` ( IndMet ` W ) ) ) ( `' t " x ) e. ( Clsd ` J ) ) )
38	11, 37	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ t e. T ) -> ( t : X --> ( BaseSet ` W ) /\ A. x e. ( Clsd ` ( MetOpen ` ( IndMet ` W ) ) ) ( `' t " x ) e. ( Clsd ` J ) ) )
39	38	simpld 475	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ t e. T ) -> t : X --> ( BaseSet ` W ) )
40	39	adantlr 751	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ k e. NN ) /\ t e. T ) -> t : X --> ( BaseSet ` W ) )
41	40	ffvelrnda 6359	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ k e. NN ) /\ t e. T ) /\ x e. X ) -> ( t ` x ) e. ( BaseSet ` W ) )
42	41	biantrurd 529	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ k e. NN ) /\ t e. T ) /\ x e. X ) -> ( ( N ` ( t ` x ) ) <_ k <-> ( ( t ` x ) e. ( BaseSet ` W ) /\ ( N ` ( t ` x ) ) <_ k ) ) )
43		fveq2 6191	. . . . . . . . . . . . . . 15 |- ( y = ( t ` x ) -> ( N ` y ) = ( N ` ( t ` x ) ) )
44	43	breq1d 4663	. . . . . . . . . . . . . 14 |- ( y = ( t ` x ) -> ( ( N ` y ) <_ k <-> ( N ` ( t ` x ) ) <_ k ) )
45	44	elrab 3363	. . . . . . . . . . . . 13 |- ( ( t ` x ) e. { y e. ( BaseSet ` W ) | ( N ` y ) <_ k } <-> ( ( t ` x ) e. ( BaseSet ` W ) /\ ( N ` ( t ` x ) ) <_ k ) )
46	42, 45	syl6bbr 278	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ k e. NN ) /\ t e. T ) /\ x e. X ) -> ( ( N ` ( t ` x ) ) <_ k <-> ( t ` x ) e. { y e. ( BaseSet ` W ) | ( N ` y ) <_ k } ) )
47	46	pm5.32da 673	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. NN ) /\ t e. T ) -> ( ( x e. X /\ ( N ` ( t ` x ) ) <_ k ) <-> ( x e. X /\ ( t ` x ) e. { y e. ( BaseSet ` W ) | ( N ` y ) <_ k } ) ) )
48		fveq2 6191	. . . . . . . . . . . . . . 15 |- ( z = x -> ( t ` z ) = ( t ` x ) )
49	48	fveq2d 6195	. . . . . . . . . . . . . 14 |- ( z = x -> ( N ` ( t ` z ) ) = ( N ` ( t ` x ) ) )
50	49	breq1d 4663	. . . . . . . . . . . . 13 |- ( z = x -> ( ( N ` ( t ` z ) ) <_ k <-> ( N ` ( t ` x ) ) <_ k ) )
51	50	elrab 3363	. . . . . . . . . . . 12 |- ( x e. { z e. X | ( N ` ( t ` z ) ) <_ k } <-> ( x e. X /\ ( N ` ( t ` x ) ) <_ k ) )
52	51	a1i 11	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. NN ) /\ t e. T ) -> ( x e. { z e. X | ( N ` ( t ` z ) ) <_ k } <-> ( x e. X /\ ( N ` ( t ` x ) ) <_ k ) ) )
53		ffn 6045	. . . . . . . . . . . 12 |- ( t : X --> ( BaseSet ` W ) -> t Fn X )
54		elpreima 6337	. . . . . . . . . . . 12 |- ( t Fn X -> ( x e. ( `' t " { y e. ( BaseSet ` W ) | ( N ` y ) <_ k } ) <-> ( x e. X /\ ( t ` x ) e. { y e. ( BaseSet ` W ) | ( N ` y ) <_ k } ) ) )
55	40, 53, 54	3syl 18	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. NN ) /\ t e. T ) -> ( x e. ( `' t " { y e. ( BaseSet ` W ) | ( N ` y ) <_ k } ) <-> ( x e. X /\ ( t ` x ) e. { y e. ( BaseSet ` W ) | ( N ` y ) <_ k } ) ) )
56	47, 52, 55	3bitr4d 300	. . . . . . . . . 10 |- ( ( ( ph /\ k e. NN ) /\ t e. T ) -> ( x e. { z e. X | ( N ` ( t ` z ) ) <_ k } <-> x e. ( `' t " { y e. ( BaseSet ` W ) | ( N ` y ) <_ k } ) ) )
57	56	eqrdv 2620	. . . . . . . . 9 |- ( ( ( ph /\ k e. NN ) /\ t e. T ) -> { z e. X | ( N ` ( t ` z ) ) <_ k } = ( `' t " { y e. ( BaseSet ` W ) | ( N ` y ) <_ k } ) )
58		nnre 11027	. . . . . . . . . . . . 13 |- ( k e. NN -> k e. RR )
59	58	ad2antlr 763	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. NN ) /\ t e. T ) -> k e. RR )
60	59	rexrd 10089	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. NN ) /\ t e. T ) -> k e. RR* )
61		eqid 2622	. . . . . . . . . . . . . 14 |- ( 0vec ` W ) = ( 0vec ` W )
62	30, 61	nvzcl 27489	. . . . . . . . . . . . 13 |- ( W e. NrmCVec -> ( 0vec ` W ) e. ( BaseSet ` W ) )
63	20, 62	ax-mp 5	. . . . . . . . . . . 12 |- ( 0vec ` W ) e. ( BaseSet ` W )
64		ubth.2	. . . . . . . . . . . . . . . . . 18 |- N = ( normCV ` W )
65	30, 61, 64, 13	nvnd 27543	. . . . . . . . . . . . . . . . 17 |- ( ( W e. NrmCVec /\ y e. ( BaseSet ` W ) ) -> ( N ` y ) = ( y ( IndMet ` W ) ( 0vec ` W ) ) )
66	20, 65	mpan 706	. . . . . . . . . . . . . . . 16 |- ( y e. ( BaseSet ` W ) -> ( N ` y ) = ( y ( IndMet ` W ) ( 0vec ` W ) ) )
67		xmetsym 22152	. . . . . . . . . . . . . . . . 17 |- ( ( ( IndMet ` W ) e. ( *Met ` ( BaseSet ` W ) ) /\ ( 0vec ` W ) e. ( BaseSet ` W ) /\ y e. ( BaseSet ` W ) ) -> ( ( 0vec ` W ) ( IndMet ` W ) y ) = ( y ( IndMet ` W ) ( 0vec ` W ) ) )
68	32, 63, 67	mp3an12 1414	. . . . . . . . . . . . . . . 16 |- ( y e. ( BaseSet ` W ) -> ( ( 0vec ` W ) ( IndMet ` W ) y ) = ( y ( IndMet ` W ) ( 0vec ` W ) ) )
69	66, 68	eqtr4d 2659	. . . . . . . . . . . . . . 15 |- ( y e. ( BaseSet ` W ) -> ( N ` y ) = ( ( 0vec ` W ) ( IndMet ` W ) y ) )
70	69	breq1d 4663	. . . . . . . . . . . . . 14 |- ( y e. ( BaseSet ` W ) -> ( ( N ` y ) <_ k <-> ( ( 0vec ` W ) ( IndMet ` W ) y ) <_ k ) )
71	70	rabbiia 3185	. . . . . . . . . . . . 13 |- { y e. ( BaseSet ` W ) | ( N ` y ) <_ k } = { y e. ( BaseSet ` W ) | ( ( 0vec ` W ) ( IndMet ` W ) y ) <_ k }
72	15, 71	blcld 22310	. . . . . . . . . . . 12 |- ( ( ( IndMet ` W ) e. ( *Met ` ( BaseSet ` W ) ) /\ ( 0vec ` W ) e. ( BaseSet ` W ) /\ k e. RR* ) -> { y e. ( BaseSet ` W ) | ( N ` y ) <_ k } e. ( Clsd ` ( MetOpen ` ( IndMet ` W ) ) ) )
73	32, 63, 72	mp3an12 1414	. . . . . . . . . . 11 |- ( k e. RR* -> { y e. ( BaseSet ` W ) | ( N ` y ) <_ k } e. ( Clsd ` ( MetOpen ` ( IndMet ` W ) ) ) )
74	60, 73	syl 17	. . . . . . . . . 10 |- ( ( ( ph /\ k e. NN ) /\ t e. T ) -> { y e. ( BaseSet ` W ) | ( N ` y ) <_ k } e. ( Clsd ` ( MetOpen ` ( IndMet ` W ) ) ) )
75	38	simprd 479	. . . . . . . . . . 11 |- ( ( ph /\ t e. T ) -> A. x e. ( Clsd ` ( MetOpen ` ( IndMet ` W ) ) ) ( `' t " x ) e. ( Clsd ` J ) )
76	75	adantlr 751	. . . . . . . . . 10 |- ( ( ( ph /\ k e. NN ) /\ t e. T ) -> A. x e. ( Clsd ` ( MetOpen ` ( IndMet ` W ) ) ) ( `' t " x ) e. ( Clsd ` J ) )
77		imaeq2 5462	. . . . . . . . . . . 12 |- ( x = { y e. ( BaseSet ` W ) | ( N ` y ) <_ k } -> ( `' t " x ) = ( `' t " { y e. ( BaseSet ` W ) | ( N ` y ) <_ k } ) )
78	77	eleq1d 2686	. . . . . . . . . . 11 |- ( x = { y e. ( BaseSet ` W ) | ( N ` y ) <_ k } -> ( ( `' t " x ) e. ( Clsd ` J ) <-> ( `' t " { y e. ( BaseSet ` W ) | ( N ` y ) <_ k } ) e. ( Clsd ` J ) ) )
79	78	rspcv 3305	. . . . . . . . . 10 |- ( { y e. ( BaseSet ` W ) | ( N ` y ) <_ k } e. ( Clsd ` ( MetOpen ` ( IndMet ` W ) ) ) -> ( A. x e. ( Clsd ` ( MetOpen ` ( IndMet ` W ) ) ) ( `' t " x ) e. ( Clsd ` J ) -> ( `' t " { y e. ( BaseSet ` W ) | ( N ` y ) <_ k } ) e. ( Clsd ` J ) ) )
80	74, 76, 79	sylc 65	. . . . . . . . 9 |- ( ( ( ph /\ k e. NN ) /\ t e. T ) -> ( `' t " { y e. ( BaseSet ` W ) | ( N ` y ) <_ k } ) e. ( Clsd ` J ) )
81	57, 80	eqeltrd 2701	. . . . . . . 8 |- ( ( ( ph /\ k e. NN ) /\ t e. T ) -> { z e. X | ( N ` ( t ` z ) ) <_ k } e. ( Clsd ` J ) )
82	81	ralrimiva 2966	. . . . . . 7 |- ( ( ph /\ k e. NN ) -> A. t e. T { z e. X | ( N ` ( t ` z ) ) <_ k } e. ( Clsd ` J ) )
83		iincld 20843	. . . . . . 7 |- ( ( T =/= (/) /\ A. t e. T { z e. X | ( N ` ( t ` z ) ) <_ k } e. ( Clsd ` J ) ) -> |^|_ t e. T { z e. X | ( N ` ( t ` z ) ) <_ k } e. ( Clsd ` J ) )
84	9, 82, 83	syl2anr 495	. . . . . 6 |- ( ( ( ph /\ k e. NN ) /\ T =/= (/) ) -> |^|_ t e. T { z e. X | ( N ` ( t ` z ) ) <_ k } e. ( Clsd ` J ) )
85	8, 84	eqeltrrd 2702	. . . . 5 |- ( ( ( ph /\ k e. NN ) /\ T =/= (/) ) -> { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } e. ( Clsd ` J ) )
86	14	mopntop 22245	. . . . . . . 8 |- ( D e. ( *Met ` X ) -> J e. Top )
87	27, 86	ax-mp 5	. . . . . . 7 |- J e. Top
88	29	toponunii 20721	. . . . . . . 8 |- X = U. J
89	88	topcld 20839	. . . . . . 7 |- ( J e. Top -> X e. ( Clsd ` J ) )
90	87, 89	ax-mp 5	. . . . . 6 |- X e. ( Clsd ` J )
91	90	a1i 11	. . . . 5 |- ( ( ph /\ k e. NN ) -> X e. ( Clsd ` J ) )
92	6, 85, 91	pm2.61ne 2879	. . . 4 |- ( ( ph /\ k e. NN ) -> { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } e. ( Clsd ` J ) )
93		ubthlem.9	. . . 4 |- A = ( k e. NN |-> { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } )
94	92, 93	fmptd 6385	. . 3 |- ( ph -> A : NN --> ( Clsd ` J ) )
95		frn 6053	. . . . . . 7 |- ( A : NN --> ( Clsd ` J ) -> ran A C_ ( Clsd ` J ) )
96	94, 95	syl 17	. . . . . 6 |- ( ph -> ran A C_ ( Clsd ` J ) )
97	88	cldss2 20834	. . . . . 6 |- ( Clsd ` J ) C_ ~P X
98	96, 97	syl6ss 3615	. . . . 5 |- ( ph -> ran A C_ ~P X )
99		sspwuni 4611	. . . . 5 |- ( ran A C_ ~P X <-> U. ran A C_ X )
100	98, 99	sylib 208	. . . 4 |- ( ph -> U. ran A C_ X )
101		ubthlem.8	. . . . . 6 |- ( ph -> A. x e. X E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c )
102		arch 11289	. . . . . . . . . 10 |- ( c e. RR -> E. k e. NN c < k )
103	102	adantl 482	. . . . . . . . 9 |- ( ( ( ph /\ x e. X ) /\ c e. RR ) -> E. k e. NN c < k )
104		simpr 477	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. X ) /\ c e. RR ) -> c e. RR )
105		ltle 10126	. . . . . . . . . . . . . . . . 17 |- ( ( c e. RR /\ k e. RR ) -> ( c < k -> c <_ k ) )
106	104, 58, 105	syl2an 494	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ x e. X ) /\ c e. RR ) /\ k e. NN ) -> ( c < k -> c <_ k ) )
107	106	impr 649	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ x e. X ) /\ c e. RR ) /\ ( k e. NN /\ c < k ) ) -> c <_ k )
108	107	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ x e. X ) /\ c e. RR ) /\ ( k e. NN /\ c < k ) ) /\ t e. T ) -> c <_ k )
109	39	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( t ` x ) e. ( BaseSet ` W ) )
110	109	an32s 846	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. X ) /\ t e. T ) -> ( t ` x ) e. ( BaseSet ` W ) )
111	30, 64	nvcl 27516	. . . . . . . . . . . . . . . . . 18 |- ( ( W e. NrmCVec /\ ( t ` x ) e. ( BaseSet ` W ) ) -> ( N ` ( t ` x ) ) e. RR )
112	20, 110, 111	sylancr 695	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. X ) /\ t e. T ) -> ( N ` ( t ` x ) ) e. RR )
113	112	adantlr 751	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ x e. X ) /\ c e. RR ) /\ t e. T ) -> ( N ` ( t ` x ) ) e. RR )
114	113	adantlr 751	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ x e. X ) /\ c e. RR ) /\ ( k e. NN /\ c < k ) ) /\ t e. T ) -> ( N ` ( t ` x ) ) e. RR )
115		simpllr 799	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ x e. X ) /\ c e. RR ) /\ ( k e. NN /\ c < k ) ) /\ t e. T ) -> c e. RR )
116		simplrl 800	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ x e. X ) /\ c e. RR ) /\ ( k e. NN /\ c < k ) ) /\ t e. T ) -> k e. NN )
117	116, 58	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ x e. X ) /\ c e. RR ) /\ ( k e. NN /\ c < k ) ) /\ t e. T ) -> k e. RR )
118		letr 10131	. . . . . . . . . . . . . . 15 |- ( ( ( N ` ( t ` x ) ) e. RR /\ c e. RR /\ k e. RR ) -> ( ( ( N ` ( t ` x ) ) <_ c /\ c <_ k ) -> ( N ` ( t ` x ) ) <_ k ) )
119	114, 115, 117, 118	syl3anc 1326	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ x e. X ) /\ c e. RR ) /\ ( k e. NN /\ c < k ) ) /\ t e. T ) -> ( ( ( N ` ( t ` x ) ) <_ c /\ c <_ k ) -> ( N ` ( t ` x ) ) <_ k ) )
120	108, 119	mpan2d 710	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ x e. X ) /\ c e. RR ) /\ ( k e. NN /\ c < k ) ) /\ t e. T ) -> ( ( N ` ( t ` x ) ) <_ c -> ( N ` ( t ` x ) ) <_ k ) )
121	120	ralimdva 2962	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. X ) /\ c e. RR ) /\ ( k e. NN /\ c < k ) ) -> ( A. t e. T ( N ` ( t ` x ) ) <_ c -> A. t e. T ( N ` ( t ` x ) ) <_ k ) )
122	121	expr 643	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. X ) /\ c e. RR ) /\ k e. NN ) -> ( c < k -> ( A. t e. T ( N ` ( t ` x ) ) <_ c -> A. t e. T ( N ` ( t ` x ) ) <_ k ) ) )
123		fvex 6201	. . . . . . . . . . . . . . . . . . 19 |- ( BaseSet ` U ) e. _V
124	22, 123	eqeltri 2697	. . . . . . . . . . . . . . . . . 18 |- X e. _V
125	124	rabex 4813	. . . . . . . . . . . . . . . . 17 |- { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } e. _V
126	93	fvmpt2 6291	. . . . . . . . . . . . . . . . 17 |- ( ( k e. NN /\ { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } e. _V ) -> ( A ` k ) = { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } )
127	125, 126	mpan2 707	. . . . . . . . . . . . . . . 16 |- ( k e. NN -> ( A ` k ) = { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } )
128	127	eleq2d 2687	. . . . . . . . . . . . . . 15 |- ( k e. NN -> ( x e. ( A ` k ) <-> x e. { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } ) )
129	50	ralbidv 2986	. . . . . . . . . . . . . . . 16 |- ( z = x -> ( A. t e. T ( N ` ( t ` z ) ) <_ k <-> A. t e. T ( N ` ( t ` x ) ) <_ k ) )
130	129	elrab 3363	. . . . . . . . . . . . . . 15 |- ( x e. { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } <-> ( x e. X /\ A. t e. T ( N ` ( t ` x ) ) <_ k ) )
131	128, 130	syl6bb 276	. . . . . . . . . . . . . 14 |- ( k e. NN -> ( x e. ( A ` k ) <-> ( x e. X /\ A. t e. T ( N ` ( t ` x ) ) <_ k ) ) )
132		simpr 477	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. X ) -> x e. X )
133	132	biantrurd 529	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. X ) -> ( A. t e. T ( N ` ( t ` x ) ) <_ k <-> ( x e. X /\ A. t e. T ( N ` ( t ` x ) ) <_ k ) ) )
134	133	bicomd 213	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. X ) -> ( ( x e. X /\ A. t e. T ( N ` ( t ` x ) ) <_ k ) <-> A. t e. T ( N ` ( t ` x ) ) <_ k ) )
135	131, 134	sylan9bbr 737	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. X ) /\ k e. NN ) -> ( x e. ( A ` k ) <-> A. t e. T ( N ` ( t ` x ) ) <_ k ) )
136		ffn 6045	. . . . . . . . . . . . . . . 16 |- ( A : NN --> ( Clsd ` J ) -> A Fn NN )
137	94, 136	syl 17	. . . . . . . . . . . . . . 15 |- ( ph -> A Fn NN )
138	137	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. X ) -> A Fn NN )
139		fnfvelrn 6356	. . . . . . . . . . . . . . . 16 |- ( ( A Fn NN /\ k e. NN ) -> ( A ` k ) e. ran A )
140		elssuni 4467	. . . . . . . . . . . . . . . 16 |- ( ( A ` k ) e. ran A -> ( A ` k ) C_ U. ran A )
141	139, 140	syl 17	. . . . . . . . . . . . . . 15 |- ( ( A Fn NN /\ k e. NN ) -> ( A ` k ) C_ U. ran A )
142	141	sseld 3602	. . . . . . . . . . . . . 14 |- ( ( A Fn NN /\ k e. NN ) -> ( x e. ( A ` k ) -> x e. U. ran A ) )
143	138, 142	sylan 488	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. X ) /\ k e. NN ) -> ( x e. ( A ` k ) -> x e. U. ran A ) )
144	135, 143	sylbird 250	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. X ) /\ k e. NN ) -> ( A. t e. T ( N ` ( t ` x ) ) <_ k -> x e. U. ran A ) )
145	144	adantlr 751	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. X ) /\ c e. RR ) /\ k e. NN ) -> ( A. t e. T ( N ` ( t ` x ) ) <_ k -> x e. U. ran A ) )
146	122, 145	syl6d 75	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. X ) /\ c e. RR ) /\ k e. NN ) -> ( c < k -> ( A. t e. T ( N ` ( t ` x ) ) <_ c -> x e. U. ran A ) ) )
147	146	rexlimdva 3031	. . . . . . . . 9 |- ( ( ( ph /\ x e. X ) /\ c e. RR ) -> ( E. k e. NN c < k -> ( A. t e. T ( N ` ( t ` x ) ) <_ c -> x e. U. ran A ) ) )
148	103, 147	mpd 15	. . . . . . . 8 |- ( ( ( ph /\ x e. X ) /\ c e. RR ) -> ( A. t e. T ( N ` ( t ` x ) ) <_ c -> x e. U. ran A ) )
149	148	rexlimdva 3031	. . . . . . 7 |- ( ( ph /\ x e. X ) -> ( E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c -> x e. U. ran A ) )
150	149	ralimdva 2962	. . . . . 6 |- ( ph -> ( A. x e. X E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c -> A. x e. X x e. U. ran A ) )
151	101, 150	mpd 15	. . . . 5 |- ( ph -> A. x e. X x e. U. ran A )
152		dfss3 3592	. . . . 5 |- ( X C_ U. ran A <-> A. x e. X x e. U. ran A )
153	151, 152	sylibr 224	. . . 4 |- ( ph -> X C_ U. ran A )
154	100, 153	eqssd 3620	. . 3 |- ( ph -> U. ran A = X )
155		eqid 2622	. . . . . 6 |- ( 0vec ` U ) = ( 0vec ` U )
156	22, 155	nvzcl 27489	. . . . 5 |- ( U e. NrmCVec -> ( 0vec ` U ) e. X )
157		ne0i 3921	. . . . 5 |- ( ( 0vec ` U ) e. X -> X =/= (/) )
158	19, 156, 157	mp2b 10	. . . 4 |- X =/= (/)
159	14	bcth2 23127	. . . 4 |- ( ( ( D e. ( CMet ` X ) /\ X =/= (/) ) /\ ( A : NN --> ( Clsd ` J ) /\ U. ran A = X ) ) -> E. n e. NN ( ( int ` J ) ` ( A ` n ) ) =/= (/) )
160	24, 158, 159	mpanl12 718	. . 3 |- ( ( A : NN --> ( Clsd ` J ) /\ U. ran A = X ) -> E. n e. NN ( ( int ` J ) ` ( A ` n ) ) =/= (/) )
161	94, 154, 160	syl2anc 693	. 2 |- ( ph -> E. n e. NN ( ( int ` J ) ` ( A ` n ) ) =/= (/) )
162		ffvelrn 6357	. . . . . . . . . . 11 |- ( ( A : NN --> ( Clsd ` J ) /\ n e. NN ) -> ( A ` n ) e. ( Clsd ` J ) )
163	97, 162	sseldi 3601	. . . . . . . . . 10 |- ( ( A : NN --> ( Clsd ` J ) /\ n e. NN ) -> ( A ` n ) e. ~P X )
164	163	elpwid 4170	. . . . . . . . 9 |- ( ( A : NN --> ( Clsd ` J ) /\ n e. NN ) -> ( A ` n ) C_ X )
165	94, 164	sylan 488	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> ( A ` n ) C_ X )
166	88	ntrss3 20864	. . . . . . . 8 |- ( ( J e. Top /\ ( A ` n ) C_ X ) -> ( ( int ` J ) ` ( A ` n ) ) C_ X )
167	87, 165, 166	sylancr 695	. . . . . . 7 |- ( ( ph /\ n e. NN ) -> ( ( int ` J ) ` ( A ` n ) ) C_ X )
168	167	sseld 3602	. . . . . 6 |- ( ( ph /\ n e. NN ) -> ( y e. ( ( int ` J ) ` ( A ` n ) ) -> y e. X ) )
169	88	ntropn 20853	. . . . . . . . . 10 |- ( ( J e. Top /\ ( A ` n ) C_ X ) -> ( ( int ` J ) ` ( A ` n ) ) e. J )
170	87, 165, 169	sylancr 695	. . . . . . . . 9 |- ( ( ph /\ n e. NN ) -> ( ( int ` J ) ` ( A ` n ) ) e. J )
171	14	mopni2 22298	. . . . . . . . . 10 |- ( ( D e. ( *Met ` X ) /\ ( ( int ` J ) ` ( A ` n ) ) e. J /\ y e. ( ( int ` J ) ` ( A ` n ) ) ) -> E. x e. RR+ ( y ( ball ` D ) x ) C_ ( ( int ` J ) ` ( A ` n ) ) )
172	27, 171	mp3an1 1411	. . . . . . . . 9 |- ( ( ( ( int ` J ) ` ( A ` n ) ) e. J /\ y e. ( ( int ` J ) ` ( A ` n ) ) ) -> E. x e. RR+ ( y ( ball ` D ) x ) C_ ( ( int ` J ) ` ( A ` n ) ) )
173	170, 172	sylan 488	. . . . . . . 8 |- ( ( ( ph /\ n e. NN ) /\ y e. ( ( int ` J ) ` ( A ` n ) ) ) -> E. x e. RR+ ( y ( ball ` D ) x ) C_ ( ( int ` J ) ` ( A ` n ) ) )
174		elssuni 4467	. . . . . . . . . . . 12 |- ( ( ( int ` J ) ` ( A ` n ) ) e. J -> ( ( int ` J ) ` ( A ` n ) ) C_ U. J )
175	174, 88	syl6sseqr 3652	. . . . . . . . . . 11 |- ( ( ( int ` J ) ` ( A ` n ) ) e. J -> ( ( int ` J ) ` ( A ` n ) ) C_ X )
176	170, 175	syl 17	. . . . . . . . . 10 |- ( ( ph /\ n e. NN ) -> ( ( int ` J ) ` ( A ` n ) ) C_ X )
177	176	sselda 3603	. . . . . . . . 9 |- ( ( ( ph /\ n e. NN ) /\ y e. ( ( int ` J ) ` ( A ` n ) ) ) -> y e. X )
178	88	ntrss2 20861	. . . . . . . . . . . . . 14 |- ( ( J e. Top /\ ( A ` n ) C_ X ) -> ( ( int ` J ) ` ( A ` n ) ) C_ ( A ` n ) )
179	87, 165, 178	sylancr 695	. . . . . . . . . . . . 13 |- ( ( ph /\ n e. NN ) -> ( ( int ` J ) ` ( A ` n ) ) C_ ( A ` n ) )
180		sstr2 3610	. . . . . . . . . . . . 13 |- ( ( y ( ball ` D ) x ) C_ ( ( int ` J ) ` ( A ` n ) ) -> ( ( ( int ` J ) ` ( A ` n ) ) C_ ( A ` n ) -> ( y ( ball ` D ) x ) C_ ( A ` n ) ) )
181	179, 180	syl5com 31	. . . . . . . . . . . 12 |- ( ( ph /\ n e. NN ) -> ( ( y ( ball ` D ) x ) C_ ( ( int ` J ) ` ( A ` n ) ) -> ( y ( ball ` D ) x ) C_ ( A ` n ) ) )
182	181	ad2antrr 762	. . . . . . . . . . 11 |- ( ( ( ( ph /\ n e. NN ) /\ y e. X ) /\ x e. RR+ ) -> ( ( y ( ball ` D ) x ) C_ ( ( int ` J ) ` ( A ` n ) ) -> ( y ( ball ` D ) x ) C_ ( A ` n ) ) )
183		simpr 477	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ n e. NN ) /\ y e. X ) -> y e. X )
184	183, 27	jctil 560	. . . . . . . . . . . . 13 |- ( ( ( ph /\ n e. NN ) /\ y e. X ) -> ( D e. ( *Met ` X ) /\ y e. X ) )
185		rphalfcl 11858	. . . . . . . . . . . . . . 15 |- ( x e. RR+ -> ( x / 2 ) e. RR+ )
186	185	rpxrd 11873	. . . . . . . . . . . . . 14 |- ( x e. RR+ -> ( x / 2 ) e. RR* )
187		rpxr 11840	. . . . . . . . . . . . . 14 |- ( x e. RR+ -> x e. RR* )
188		rphalflt 11860	. . . . . . . . . . . . . 14 |- ( x e. RR+ -> ( x / 2 ) < x )
189	186, 187, 188	3jca 1242	. . . . . . . . . . . . 13 |- ( x e. RR+ -> ( ( x / 2 ) e. RR* /\ x e. RR* /\ ( x / 2 ) < x ) )
190		eqid 2622	. . . . . . . . . . . . . 14 |- { z e. X | ( y D z ) <_ ( x / 2 ) } = { z e. X | ( y D z ) <_ ( x / 2 ) }
191	14, 190	blsscls2 22309	. . . . . . . . . . . . 13 |- ( ( ( D e. ( *Met ` X ) /\ y e. X ) /\ ( ( x / 2 ) e. RR* /\ x e. RR* /\ ( x / 2 ) < x ) ) -> { z e. X | ( y D z ) <_ ( x / 2 ) } C_ ( y ( ball ` D ) x ) )
192	184, 189, 191	syl2an 494	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ n e. NN ) /\ y e. X ) /\ x e. RR+ ) -> { z e. X | ( y D z ) <_ ( x / 2 ) } C_ ( y ( ball ` D ) x ) )
193		sstr2 3610	. . . . . . . . . . . 12 |- ( { z e. X | ( y D z ) <_ ( x / 2 ) } C_ ( y ( ball ` D ) x ) -> ( ( y ( ball ` D ) x ) C_ ( A ` n ) -> { z e. X | ( y D z ) <_ ( x / 2 ) } C_ ( A ` n ) ) )
194	192, 193	syl 17	. . . . . . . . . . 11 |- ( ( ( ( ph /\ n e. NN ) /\ y e. X ) /\ x e. RR+ ) -> ( ( y ( ball ` D ) x ) C_ ( A ` n ) -> { z e. X | ( y D z ) <_ ( x / 2 ) } C_ ( A ` n ) ) )
195	185	adantl 482	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ n e. NN ) /\ y e. X ) /\ x e. RR+ ) -> ( x / 2 ) e. RR+ )
196		breq2 4657	. . . . . . . . . . . . . . . 16 |- ( r = ( x / 2 ) -> ( ( y D z ) <_ r <-> ( y D z ) <_ ( x / 2 ) ) )
197	196	rabbidv 3189	. . . . . . . . . . . . . . 15 |- ( r = ( x / 2 ) -> { z e. X | ( y D z ) <_ r } = { z e. X | ( y D z ) <_ ( x / 2 ) } )
198	197	sseq1d 3632	. . . . . . . . . . . . . 14 |- ( r = ( x / 2 ) -> ( { z e. X | ( y D z ) <_ r } C_ ( A ` n ) <-> { z e. X | ( y D z ) <_ ( x / 2 ) } C_ ( A ` n ) ) )
199	198	rspcev 3309	. . . . . . . . . . . . 13 |- ( ( ( x / 2 ) e. RR+ /\ { z e. X | ( y D z ) <_ ( x / 2 ) } C_ ( A ` n ) ) -> E. r e. RR+ { z e. X | ( y D z ) <_ r } C_ ( A ` n ) )
200	199	ex 450	. . . . . . . . . . . 12 |- ( ( x / 2 ) e. RR+ -> ( { z e. X | ( y D z ) <_ ( x / 2 ) } C_ ( A ` n ) -> E. r e. RR+ { z e. X | ( y D z ) <_ r } C_ ( A ` n ) ) )
201	195, 200	syl 17	. . . . . . . . . . 11 |- ( ( ( ( ph /\ n e. NN ) /\ y e. X ) /\ x e. RR+ ) -> ( { z e. X | ( y D z ) <_ ( x / 2 ) } C_ ( A ` n ) -> E. r e. RR+ { z e. X | ( y D z ) <_ r } C_ ( A ` n ) ) )
202	182, 194, 201	3syld 60	. . . . . . . . . 10 |- ( ( ( ( ph /\ n e. NN ) /\ y e. X ) /\ x e. RR+ ) -> ( ( y ( ball ` D ) x ) C_ ( ( int ` J ) ` ( A ` n ) ) -> E. r e. RR+ { z e. X | ( y D z ) <_ r } C_ ( A ` n ) ) )
203	202	rexlimdva 3031	. . . . . . . . 9 |- ( ( ( ph /\ n e. NN ) /\ y e. X ) -> ( E. x e. RR+ ( y ( ball ` D ) x ) C_ ( ( int ` J ) ` ( A ` n ) ) -> E. r e. RR+ { z e. X | ( y D z ) <_ r } C_ ( A ` n ) ) )
204	177, 203	syldan 487	. . . . . . . 8 |- ( ( ( ph /\ n e. NN ) /\ y e. ( ( int ` J ) ` ( A ` n ) ) ) -> ( E. x e. RR+ ( y ( ball ` D ) x ) C_ ( ( int ` J ) ` ( A ` n ) ) -> E. r e. RR+ { z e. X | ( y D z ) <_ r } C_ ( A ` n ) ) )
205	173, 204	mpd 15	. . . . . . 7 |- ( ( ( ph /\ n e. NN ) /\ y e. ( ( int ` J ) ` ( A ` n ) ) ) -> E. r e. RR+ { z e. X | ( y D z ) <_ r } C_ ( A ` n ) )
206	205	ex 450	. . . . . 6 |- ( ( ph /\ n e. NN ) -> ( y e. ( ( int ` J ) ` ( A ` n ) ) -> E. r e. RR+ { z e. X | ( y D z ) <_ r } C_ ( A ` n ) ) )
207	168, 206	jcad 555	. . . . 5 |- ( ( ph /\ n e. NN ) -> ( y e. ( ( int ` J ) ` ( A ` n ) ) -> ( y e. X /\ E. r e. RR+ { z e. X | ( y D z ) <_ r } C_ ( A ` n ) ) ) )
208	207	eximdv 1846	. . . 4 |- ( ( ph /\ n e. NN ) -> ( E. y y e. ( ( int ` J ) ` ( A ` n ) ) -> E. y ( y e. X /\ E. r e. RR+ { z e. X | ( y D z ) <_ r } C_ ( A ` n ) ) ) )
209		n0 3931	. . . 4 |- ( ( ( int ` J ) ` ( A ` n ) ) =/= (/) <-> E. y y e. ( ( int ` J ) ` ( A ` n ) ) )
210		df-rex 2918	. . . 4 |- ( E. y e. X E. r e. RR+ { z e. X | ( y D z ) <_ r } C_ ( A ` n ) <-> E. y ( y e. X /\ E. r e. RR+ { z e. X | ( y D z ) <_ r } C_ ( A ` n ) ) )
211	208, 209, 210	3imtr4g 285	. . 3 |- ( ( ph /\ n e. NN ) -> ( ( ( int ` J ) ` ( A ` n ) ) =/= (/) -> E. y e. X E. r e. RR+ { z e. X | ( y D z ) <_ r } C_ ( A ` n ) ) )
212	211	reximdva 3017	. 2 |- ( ph -> ( E. n e. NN ( ( int ` J ) ` ( A ` n ) ) =/= (/) -> E. n e. NN E. y e. X E. r e. RR+ { z e. X | ( y D z ) <_ r } C_ ( A ` n ) ) )
213	161, 212	mpd 15	1 |- ( ph -> E. n e. NN E. y e. X E. r e. RR+ { z e. X | ( y D z ) <_ r } C_ ( A ` n ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   E.wex 1704   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   C_ wss 3574   (/)c0 3915   ~Pcpw 4158   U.cuni 4436   |^|_ciin 4521   class class class wbr 4653   |-> cmpt 4729   `'ccnv 5113   ran crn 5115   "cima 5117   Fn wfn 5883   -->wf 5884   ` cfv 5888  (class class class)co 6650   RRcr 9935   RR*cxr 10073   < clt 10074   <_ cle 10075   / cdiv 10684   NNcn 11020   2c2 11070   RR+crp 11832   *Metcxmt 19731   Metcme 19732   ballcbl 19733   MetOpencmopn 19736   Topctop 20698  TopOnctopon 20715   Clsdccld 20820   intcnt 20821   Cn ccn 21028   CMetcms 23052   NrmCVeccnv 27439   BaseSetcba 27441   0veccn0v 27443   norm_CVcnmcv 27445   IndMetcims 27446   BLnOp cblo 27597   CBanccbn 27718

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-dc 9268  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014  ax-addf 10015  ax-mulf 10016

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-er 7742  df-map 7859  df-pm 7860  df-en 7956  df-dom 7957  df-sdom 7958  df-sup 8348  df-inf 8349  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-n0 11293  df-z 11378  df-uz 11688  df-q 11789  df-rp 11833  df-xneg 11946  df-xadd 11947  df-xmul 11948  df-ico 12181  df-seq 12802  df-exp 12861  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-rest 16083  df-topgen 16104  df-psmet 19738  df-xmet 19739  df-met 19740  df-bl 19741  df-mopn 19742  df-fbas 19743  df-fg 19744  df-top 20699  df-topon 20716  df-bases 20750  df-cld 20823  df-ntr 20824  df-cls 20825  df-nei 20902  df-cn 21031  df-cnp 21032  df-lm 21033  df-fil 21650  df-fm 21742  df-flim 21743  df-flf 21744  df-cfil 23053  df-cau 23054  df-cmet 23055  df-grpo 27347  df-gid 27348  df-ginv 27349  df-gdiv 27350  df-ablo 27399  df-vc 27414  df-nv 27447  df-va 27450  df-ba 27451  df-sm 27452  df-0v 27453  df-vs 27454  df-nmcv 27455  df-ims 27456  df-lno 27599  df-nmoo 27600  df-blo 27601  df-0o 27602  df-cbn 27719

This theorem is referenced by:  ubthlem3  27728