Theorem locfindsc 16339

Description: The locally finite covers of a discrete space are precisely the point-finite covers.

Hypothesis

Ref	Expression
locfindsc.1	|- Y = U.C

Assertion

Ref	Expression
locfindsc	|- (C e. B -> (<.~PX, C>. e. LocFin <-> (C e. PtFin /\ X = Y)))

Proof of Theorem locfindsc

Step	Hyp	Ref	Expression
1		lfinpfin 16337	. . . 4 |- ((C e. B /\ <.~PX, C>. e. LocFin) -> C e. PtFin)
2		unipw 3668	. . . . . 6 |- U.~PX = X
3	2	eqcomi 2145	. . . . 5 |- X = U.~PX
4		locfindsc.1	. . . . 5 |- Y = U.C
5	3, 4	locfinbas 16335	. . . 4 |- ((C e. B /\ <.~PX, C>. e. LocFin) -> X = Y)
6	1, 5	jca 494	. . 3 |- ((C e. B /\ <.~PX, C>. e. LocFin) -> (C e. PtFin /\ X = Y))
7	6	ex 398	. 2 |- (C e. B -> (<.~PX, C>. e. LocFin -> (C e. PtFin /\ X = Y)))
8		uniexg 3934	. . . . . . 7 |- (C e. PtFin -> U.C e. _V)
9	4, 8	syl5eqel 2222	. . . . . 6 |- (C e. PtFin -> Y e. _V)
10		eleq1 2204	. . . . . . 7 |- (X = Y -> (X e. _V <-> Y e. _V))
11	10	biimparc 618	. . . . . 6 |- ((Y e. _V /\ X = Y) -> X e. _V)
12	9, 11	sylan 597	. . . . 5 |- ((C e. PtFin /\ X = Y) -> X e. _V)
13		pweq 3230	. . . . . . 7 |- (x = X -> ~Px = ~PX)
14	13	eleq1d 2210	. . . . . 6 |- (x = X -> (~Px e. Top <-> ~PX e. Top))
15		visset 2541	. . . . . . 7 |- x e. _V
16	15	distop 9770	. . . . . 6 |- ~Px e. Top
17	14, 16	vtoclg 2588	. . . . 5 |- (X e. _V -> ~PX e. Top)
18	12, 17	syl 13	. . . 4 |- ((C e. PtFin /\ X = Y) -> ~PX e. Top)
19		simpr 442	. . . 4 |- ((C e. PtFin /\ X = Y) -> X = Y)
20	18	3adant3 1140	. . . . . . . 8 |- ((C e. PtFin /\ X = Y /\ x e. X) -> ~PX e. Top)
21	15	snelpw 3665	. . . . . . . . . 10 |- (x e. X <-> {x} e. ~PX)
22	21	biimpi 224	. . . . . . . . 9 |- (x e. X -> {x} e. ~PX)
23	22	3ad2ant3 1143	. . . . . . . 8 |- ((C e. PtFin /\ X = Y /\ x e. X) -> {x} e. ~PX)
24	15	snid 3262	. . . . . . . . 9 |- x e. {x}
25	24	a1i 8	. . . . . . . 8 |- ((C e. PtFin /\ X = Y /\ x e. X) -> x e. {x})
26		opnneip 9874	. . . . . . . 8 |- ((~PX e. Top /\ {x} e. ~PX /\ x e. {x}) -> {x} e. ((nei` ~PX)` {x}))
27	20, 23, 25, 26	syl111anc 1349	. . . . . . 7 |- ((C e. PtFin /\ X = Y /\ x e. X) -> {x} e. ((nei` ~PX)` {x}))
28		disjsn 3280	. . . . . . . . . . . 12 |- ((s i^i {x}) = (/) <-> -. x e. s)
29	28	bicomi 268	. . . . . . . . . . 11 |- (-. x e. s <-> (s i^i {x}) = (/))
30	29	necon1abii 2316	. . . . . . . . . 10 |- ((s i^i {x}) =/= (/) <-> x e. s)
31	30	a1i 8	. . . . . . . . 9 |- (s e. C -> ((s i^i {x}) =/= (/) <-> x e. s))
32	31	rabbiia 2531	. . . . . . . 8 |- {s e. C | (s i^i {x}) =/= (/)} = {s e. C | x e. s}
33		simp1 1120	. . . . . . . . 9 |- ((C e. PtFin /\ X = Y /\ x e. X) -> C e. PtFin)
34		eleq2 2205	. . . . . . . . . . 11 |- (X = Y -> (x e. X <-> x e. Y))
35	34	biimpa 615	. . . . . . . . . 10 |- ((X = Y /\ x e. X) -> x e. Y)
36	35	3adant1 1138	. . . . . . . . 9 |- ((C e. PtFin /\ X = Y /\ x e. X) -> x e. Y)
37	4	ptfinfin 16332	. . . . . . . . 9 |- ((C e. PtFin /\ x e. Y) -> {s e. C | x e. s} e. Fin)
38	33, 36, 37	syl11anc 659	. . . . . . . 8 |- ((C e. PtFin /\ X = Y /\ x e. X) -> {s e. C | x e. s} e. Fin)
39	32, 38	syl5eqel 2222	. . . . . . 7 |- ((C e. PtFin /\ X = Y /\ x e. X) -> {s e. C | (s i^i {x}) =/= (/)} e. Fin)
40		ineq2 3003	. . . . . . . . . . 11 |- (n = {x} -> (s i^i n) = (s i^i {x}))
41	40	neeq1d 2278	. . . . . . . . . 10 |- (n = {x} -> ((s i^i n) =/= (/) <-> (s i^i {x}) =/= (/)))
42	41	rabbidv 2533	. . . . . . . . 9 |- (n = {x} -> {s e. C | (s i^i n) =/= (/)} = {s e. C | (s i^i {x}) =/= (/)})
43	42	eleq1d 2210	. . . . . . . 8 |- (n = {x} -> ({s e. C | (s i^i n) =/= (/)} e. Fin <-> {s e. C | (s i^i {x}) =/= (/)} e. Fin))
44	43	rcla4ev 2620	. . . . . . 7 |- (({x} e. ((nei` ~PX)` {x}) /\ {s e. C | (s i^i {x}) =/= (/)} e. Fin) -> E.n e. ((nei` ~PX)` {x}){s e. C | (s i^i n) =/= (/)} e. Fin)
45	27, 39, 44	syl11anc 659	. . . . . 6 |- ((C e. PtFin /\ X = Y /\ x e. X) -> E.n e. ((nei` ~PX)` {x}){s e. C | (s i^i n) =/= (/)} e. Fin)
46	45	3expia 1319	. . . . 5 |- ((C e. PtFin /\ X = Y) -> (x e. X -> E.n e. ((nei` ~PX)` {x}){s e. C | (s i^i n) =/= (/)} e. Fin))
47	46	r19.21aiv 2425	. . . 4 |- ((C e. PtFin /\ X = Y) -> A.x e. X E.n e. ((nei` ~PX)` {x}){s e. C | (s i^i n) =/= (/)} e. Fin)
48	18, 19, 47	3jca 1300	. . 3 |- ((C e. PtFin /\ X = Y) -> (~PX e. Top /\ X = Y /\ A.x e. X E.n e. ((nei` ~PX)` {x}){s e. C | (s i^i n) =/= (/)} e. Fin))
49	3, 4	islocfin 16330	. . 3 |- (C e. B -> (<.~PX, C>. e. LocFin <-> (~PX e. Top /\ X = Y /\ A.x e. X E.n e. ((nei` ~PX)` {x}){s e. C | (s i^i n) =/= (/)} e. Fin)))
50	48, 49	syl5ibr 257	. 2 |- (C e. B -> ((C e. PtFin /\ X = Y) -> <.~PX, C>. e. LocFin))
51	7, 50	impbid 235	1 |- (C e. B -> (<.~PX, C>. e. LocFin <-> (C e. PtFin /\ X = Y)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 219   /\ wa 337   /\ w3a 1102   = wceq 1586   e. wcel 1588   =/= wne 2266  A.wral 2355  E.wrex 2356  {crab 2358  _Vcvv 2538   i^i cin 2826  (/)c0 3082  ~Pcpw 3227  {csn 3238  <.cop 3240  U.cuni 3366  ` cfv 4131  Fincfn 5587  Topctop 9686  neicnei 9853  PtFincptfin 16283  LocFinclocfin 16284

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

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-ral 2359  df-rex 2360  df-rab 2362  df-v 2540  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-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-er 5479  df-en 5588  df-fin 5591  df-top 9692  df-nei 9854  df-ptfin 16289  df-locfin 16290

Copyright terms: Public domain