Theorem locfincf 15516

Description: A locally finite cover in a coarser topology is locally finite in a finer topology.

Hypotheses

Ref	Expression
locfincf.1	|- X = U.J
locfincf.2	|- Y = U.K

Assertion

Ref	Expression
locfincf	|- (((A e. B /\ <.J, A>. e. LocFin) /\ (K e. Top /\ J C_ K /\ X = Y)) -> <.K, A>. e. LocFin)

Proof of Theorem locfincf

Step	Hyp	Ref	Expression
1		simpr1 882	. . 3 |- (((A e. B /\ <.J, A>. e. LocFin) /\ (K e. Top /\ J C_ K /\ X = Y)) -> K e. Top)
2		simpr3 884	. . . 4 |- (((A e. B /\ <.J, A>. e. LocFin) /\ (K e. Top /\ J C_ K /\ X = Y)) -> X = Y)
3		locfincf.1	. . . . . 6 |- X = U.J
4		eqid 1884	. . . . . 6 |- U.A = U.A
5	3, 4	locfinbas 15511	. . . . 5 |- ((A e. B /\ <.J, A>. e. LocFin) -> X = U.A)
6	5	adantr 425	. . . 4 |- (((A e. B /\ <.J, A>. e. LocFin) /\ (K e. Top /\ J C_ K /\ X = Y)) -> X = U.A)
7	2, 6	eqtr3d 1927	. . 3 |- (((A e. B /\ <.J, A>. e. LocFin) /\ (K e. Top /\ J C_ K /\ X = Y)) -> Y = U.A)
8		simplll 452	. . . . . 6 |- ((((A e. B /\ <.J, A>. e. LocFin) /\ (K e. Top /\ J C_ K /\ X = Y)) /\ x e. Y) -> A e. B)
9		simpllr 453	. . . . . 6 |- ((((A e. B /\ <.J, A>. e. LocFin) /\ (K e. Top /\ J C_ K /\ X = Y)) /\ x e. Y) -> <.J, A>. e. LocFin)
10	2	eleq2d 1964	. . . . . . 7 |- (((A e. B /\ <.J, A>. e. LocFin) /\ (K e. Top /\ J C_ K /\ X = Y)) -> (x e. X <-> x e. Y))
11	10	biimpar 461	. . . . . 6 |- ((((A e. B /\ <.J, A>. e. LocFin) /\ (K e. Top /\ J C_ K /\ X = Y)) /\ x e. Y) -> x e. X)
12	3	locfinnei 15512	. . . . . 6 |- ((A e. B /\ <.J, A>. e. LocFin /\ x e. X) -> E.n e. ((nei` J)` {x}){s e. A | (s i^i n) =/= (/)} e. Fin)
13	8, 9, 11, 12	syl111anc 1100	. . . . 5 |- ((((A e. B /\ <.J, A>. e. LocFin) /\ (K e. Top /\ J C_ K /\ X = Y)) /\ x e. Y) -> E.n e. ((nei` J)` {x}){s e. A | (s i^i n) =/= (/)} e. Fin)
14		simplr1 918	. . . . . . . . . 10 |- ((((A e. B /\ <.J, A>. e. LocFin) /\ (K e. Top /\ J C_ K /\ X = Y)) /\ (x e. Y /\ n e. ((nei` J)` {x}))) -> K e. Top)
15		simprl 450	. . . . . . . . . 10 |- ((((A e. B /\ <.J, A>. e. LocFin) /\ (K e. Top /\ J C_ K /\ X = Y)) /\ (x e. Y /\ n e. ((nei` J)` {x}))) -> x e. Y)
16		locfincf.2	. . . . . . . . . . 11 |- Y = U.K
17	16	isneip 8996	. . . . . . . . . 10 |- ((K e. Top /\ x e. Y) -> (n e. ((nei` K)` {x}) <-> (n C_ Y /\ E.o e. K (x e. o /\ o C_ n))))
18	14, 15, 17	syl11anc 524	. . . . . . . . 9 |- ((((A e. B /\ <.J, A>. e. LocFin) /\ (K e. Top /\ J C_ K /\ X = Y)) /\ (x e. Y /\ n e. ((nei` J)` {x}))) -> (n e. ((nei` K)` {x}) <-> (n C_ Y /\ E.o e. K (x e. o /\ o C_ n))))
19		locfintop 15510	. . . . . . . . . . . . 13 |- ((A e. B /\ <.J, A>. e. LocFin) -> J e. Top)
20	3	neii1 8997	. . . . . . . . . . . . . 14 |- ((J e. Top /\ n e. ((nei` J)` {x})) -> n C_ X)
21	20	ex 402	. . . . . . . . . . . . 13 |- (J e. Top -> (n e. ((nei` J)` {x}) -> n C_ X))
22	19, 21	syl 12	. . . . . . . . . . . 12 |- ((A e. B /\ <.J, A>. e. LocFin) -> (n e. ((nei` J)` {x}) -> n C_ X))
23	22	ad2antrr 440	. . . . . . . . . . 11 |- ((((A e. B /\ <.J, A>. e. LocFin) /\ (K e. Top /\ J C_ K /\ X = Y)) /\ x e. Y) -> (n e. ((nei` J)` {x}) -> n C_ X))
24		simplr3 920	. . . . . . . . . . . 12 |- ((((A e. B /\ <.J, A>. e. LocFin) /\ (K e. Top /\ J C_ K /\ X = Y)) /\ x e. Y) -> X = Y)
25	24	sseq2d 2645	. . . . . . . . . . 11 |- ((((A e. B /\ <.J, A>. e. LocFin) /\ (K e. Top /\ J C_ K /\ X = Y)) /\ x e. Y) -> (n C_ X <-> n C_ Y))
26	23, 25	sylibd 219	. . . . . . . . . 10 |- ((((A e. B /\ <.J, A>. e. LocFin) /\ (K e. Top /\ J C_ K /\ X = Y)) /\ x e. Y) -> (n e. ((nei` J)` {x}) -> n C_ Y))
27	26	impr 422	. . . . . . . . 9 |- ((((A e. B /\ <.J, A>. e. LocFin) /\ (K e. Top /\ J C_ K /\ X = Y)) /\ (x e. Y /\ n e. ((nei` J)` {x}))) -> n C_ Y)
28		neii2 8998	. . . . . . . . . . . . . 14 |- ((J e. Top /\ n e. ((nei` J)` {x})) -> E.o e. J ({x} C_ o /\ o C_ n))
29	28	ex 402	. . . . . . . . . . . . 13 |- (J e. Top -> (n e. ((nei` J)` {x}) -> E.o e. J ({x} C_ o /\ o C_ n)))
30	19, 29	syl 12	. . . . . . . . . . . 12 |- ((A e. B /\ <.J, A>. e. LocFin) -> (n e. ((nei` J)` {x}) -> E.o e. J ({x} C_ o /\ o C_ n)))
31	30	ad2antrr 440	. . . . . . . . . . 11 |- ((((A e. B /\ <.J, A>. e. LocFin) /\ (K e. Top /\ J C_ K /\ X = Y)) /\ x e. Y) -> (n e. ((nei` J)` {x}) -> E.o e. J ({x} C_ o /\ o C_ n)))
32		ssel 2615	. . . . . . . . . . . . . . 15 |- (J C_ K -> (o e. J -> o e. K))
33	32	3ad2ant2 898	. . . . . . . . . . . . . 14 |- ((K e. Top /\ J C_ K /\ X = Y) -> (o e. J -> o e. K))
34	33	ad2antlr 441	. . . . . . . . . . . . 13 |- ((((A e. B /\ <.J, A>. e. LocFin) /\ (K e. Top /\ J C_ K /\ X = Y)) /\ x e. Y) -> (o e. J -> o e. K))
35		visset 2295	. . . . . . . . . . . . . . . . 17 |- x e. _V
36	35	snss 3122	. . . . . . . . . . . . . . . 16 |- (x e. o <-> {x} C_ o)
37	36	biimpri 169	. . . . . . . . . . . . . . 15 |- ({x} C_ o -> x e. o)
38	37	anim1i 361	. . . . . . . . . . . . . 14 |- (({x} C_ o /\ o C_ n) -> (x e. o /\ o C_ n))
39	38	a1i 8	. . . . . . . . . . . . 13 |- ((((A e. B /\ <.J, A>. e. LocFin) /\ (K e. Top /\ J C_ K /\ X = Y)) /\ x e. Y) -> (({x} C_ o /\ o C_ n) -> (x e. o /\ o C_ n)))
40	34, 39	anim12d 617	. . . . . . . . . . . 12 |- ((((A e. B /\ <.J, A>. e. LocFin) /\ (K e. Top /\ J C_ K /\ X = Y)) /\ x e. Y) -> ((o e. J /\ ({x} C_ o /\ o C_ n)) -> (o e. K /\ (x e. o /\ o C_ n))))
41	40	reximdv2 2200	. . . . . . . . . . 11 |- ((((A e. B /\ <.J, A>. e. LocFin) /\ (K e. Top /\ J C_ K /\ X = Y)) /\ x e. Y) -> (E.o e. J ({x} C_ o /\ o C_ n) -> E.o e. K (x e. o /\ o C_ n)))
42	31, 41	syld 30	. . . . . . . . . 10 |- ((((A e. B /\ <.J, A>. e. LocFin) /\ (K e. Top /\ J C_ K /\ X = Y)) /\ x e. Y) -> (n e. ((nei` J)` {x}) -> E.o e. K (x e. o /\ o C_ n)))
43	42	impr 422	. . . . . . . . 9 |- ((((A e. B /\ <.J, A>. e. LocFin) /\ (K e. Top /\ J C_ K /\ X = Y)) /\ (x e. Y /\ n e. ((nei` J)` {x}))) -> E.o e. K (x e. o /\ o C_ n))
44	18, 27, 43	mpbir2and 802	. . . . . . . 8 |- ((((A e. B /\ <.J, A>. e. LocFin) /\ (K e. Top /\ J C_ K /\ X = Y)) /\ (x e. Y /\ n e. ((nei` J)` {x}))) -> n e. ((nei` K)` {x}))
45	44	expr 418	. . . . . . 7 |- ((((A e. B /\ <.J, A>. e. LocFin) /\ (K e. Top /\ J C_ K /\ X = Y)) /\ x e. Y) -> (n e. ((nei` J)` {x}) -> n e. ((nei` K)` {x})))
46	45	anim1d 619	. . . . . 6 |- ((((A e. B /\ <.J, A>. e. LocFin) /\ (K e. Top /\ J C_ K /\ X = Y)) /\ x e. Y) -> ((n e. ((nei` J)` {x}) /\ {s e. A | (s i^i n) =/= (/)} e. Fin) -> (n e. ((nei` K)` {x}) /\ {s e. A | (s i^i n) =/= (/)} e. Fin)))
47	46	reximdv2 2200	. . . . 5 |- ((((A e. B /\ <.J, A>. e. LocFin) /\ (K e. Top /\ J C_ K /\ X = Y)) /\ x e. Y) -> (E.n e. ((nei` J)` {x}){s e. A | (s i^i n) =/= (/)} e. Fin -> E.n e. ((nei` K)` {x}){s e. A | (s i^i n) =/= (/)} e. Fin))
48	13, 47	mpd 29	. . . 4 |- ((((A e. B /\ <.J, A>. e. LocFin) /\ (K e. Top /\ J C_ K /\ X = Y)) /\ x e. Y) -> E.n e. ((nei` K)` {x}){s e. A | (s i^i n) =/= (/)} e. Fin)
49	48	r19.21aiva 2176	. . 3 |- (((A e. B /\ <.J, A>. e. LocFin) /\ (K e. Top /\ J C_ K /\ X = Y)) -> A.x e. Y E.n e. ((nei` K)` {x}){s e. A | (s i^i n) =/= (/)} e. Fin)
50	1, 7, 49	3jca 1050	. 2 |- (((A e. B /\ <.J, A>. e. LocFin) /\ (K e. Top /\ J C_ K /\ X = Y)) -> (K e. Top /\ Y = U.A /\ A.x e. Y E.n e. ((nei` K)` {x}){s e. A | (s i^i n) =/= (/)} e. Fin))
51	16, 4	islocfin 15506	. . 3 |- (A e. B -> (<.K, A>. e. LocFin <-> (K e. Top /\ Y = U.A /\ A.x e. Y E.n e. ((nei` K)` {x}){s e. A | (s i^i n) =/= (/)} e. Fin)))
52	51	ad2antrr 440	. 2 |- (((A e. B /\ <.J, A>. e. LocFin) /\ (K e. Top /\ J C_ K /\ X = Y)) -> (<.K, A>. e. LocFin <-> (K e. Top /\ Y = U.A /\ A.x e. Y E.n e. ((nei` K)` {x}){s e. A | (s i^i n) =/= (/)} e. Fin)))
53	50, 52	mpbird 213	1 |- (((A e. B /\ <.J, A>. e. LocFin) /\ (K e. Top /\ J C_ K /\ X = Y)) -> <.K, A>. e. LocFin)

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300   =/= wne 2017  A.wral 2105  E.wrex 2106  {crab 2108   i^i cin 2592   C_ wss 2593  (/)c0 2875  {csn 3044  <.cop 3046  U.cuni 3177  ` cfv 3998  Fincfn 5426  Topctop 8857  neicnei 8988  LocFinclocfin 15460

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-rab 2112  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-fv 4014  df-nei 8989  df-locfin 15466

Copyright terms: Public domain