Theorem locfincmp 19895

Description: For a compact space, the locally finite covers are precisely the finite covers. Sadly, this property does not properly characterize all compact spaces. (Contributed by Jeff Hankins, 22-Jan-2010.) (Proof shortened by Mario Carneiro, 11-Sep-2015.)

Hypotheses

Ref	Expression
locfincmp.1	|- X = U. J
locfincmp.2	|- Y = U. C

Assertion

Ref	Expression
locfincmp	|- ( J e. Comp -> ( C e. ( LocFin ` J ) <-> ( C e. Fin /\ X = Y ) ) )

Proof of Theorem locfincmp

Dummy variables o c s x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		locfincmp.1	. . . . . . . . . 10 |- X = U. J
2	1	locfinnei 19892	. . . . . . . . 9 |- ( ( C e. ( LocFin ` J ) /\ x e. X ) -> E. o e. J ( x e. o /\ { s e. C | ( s i^i o ) =/= (/) } e. Fin ) )
3	2	ralrimiva 2881	. . . . . . . 8 |- ( C e. ( LocFin ` J ) -> A. x e. X E. o e. J ( x e. o /\ { s e. C | ( s i^i o ) =/= (/) } e. Fin ) )
4	1	cmpcov2 19758	. . . . . . . 8 |- ( ( J e. Comp /\ A. x e. X E. o e. J ( x e. o /\ { s e. C | ( s i^i o ) =/= (/) } e. Fin ) ) -> E. c e. ( ~P J i^i Fin ) ( X = U. c /\ A. o e. c { s e. C | ( s i^i o ) =/= (/) } e. Fin ) )
5	3, 4	sylan2 474	. . . . . . 7 |- ( ( J e. Comp /\ C e. ( LocFin ` J ) ) -> E. c e. ( ~P J i^i Fin ) ( X = U. c /\ A. o e. c { s e. C | ( s i^i o ) =/= (/) } e. Fin ) )
6		elfpw 7834	. . . . . . . . 9 |- ( c e. ( ~P J i^i Fin ) <-> ( c C_ J /\ c e. Fin ) )
7		simplrr 760	. . . . . . . . . . 11 |- ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) -> c e. Fin )
8		eldifsn 4158	. . . . . . . . . . . . 13 |- ( x e. ( C \ { (/) } ) <-> ( x e. C /\ x =/= (/) ) )
9		elunii 4256	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( y e. x /\ x e. C ) -> y e. U. C )
10		locfincmp.2	. . . . . . . . . . . . . . . . . . . . . . . 24 |- Y = U. C
11	9, 10	syl6eleqr 2566	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( y e. x /\ x e. C ) -> y e. Y )
12	11	ancoms 453	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( x e. C /\ y e. x ) -> y e. Y )
13	12	adantl 466	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) /\ ( x e. C /\ y e. x ) ) -> y e. Y )
14	1, 10	locfinbas 19891	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( C e. ( LocFin ` J ) -> X = Y )
15	14	adantl 466	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( J e. Comp /\ C e. ( LocFin ` J ) ) -> X = Y )
16	15	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) /\ ( x e. C /\ y e. x ) ) -> X = Y )
17	13, 16	eleqtrrd 2558	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) /\ ( x e. C /\ y e. x ) ) -> y e. X )
18		simplr 754	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) /\ ( x e. C /\ y e. x ) ) -> X = U. c )
19	17, 18	eleqtrd 2557	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) /\ ( x e. C /\ y e. x ) ) -> y e. U. c )
20		eluni2 4255	. . . . . . . . . . . . . . . . . . 19 |- ( y e. U. c <-> E. o e. c y e. o )
21	19, 20	sylib 196	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) /\ ( x e. C /\ y e. x ) ) -> E. o e. c y e. o )
22		simplrl 759	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) /\ ( x e. C /\ y e. x ) ) /\ ( o e. c /\ y e. o ) ) -> x e. C )
23		simplrr 760	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) /\ ( x e. C /\ y e. x ) ) /\ ( o e. c /\ y e. o ) ) -> y e. x )
24		simprr 756	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) /\ ( x e. C /\ y e. x ) ) /\ ( o e. c /\ y e. o ) ) -> y e. o )
25		inelcm 3886	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( y e. x /\ y e. o ) -> ( x i^i o ) =/= (/) )
26	23, 24, 25	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) /\ ( x e. C /\ y e. x ) ) /\ ( o e. c /\ y e. o ) ) -> ( x i^i o ) =/= (/) )
27		ineq1 3698	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( s = x -> ( s i^i o ) = ( x i^i o ) )
28	27	neeq1d 2744	. . . . . . . . . . . . . . . . . . . . . 22 |- ( s = x -> ( ( s i^i o ) =/= (/) <-> ( x i^i o ) =/= (/) ) )
29	28	elrab 3266	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. { s e. C | ( s i^i o ) =/= (/) } <-> ( x e. C /\ ( x i^i o ) =/= (/) ) )
30	22, 26, 29	sylanbrc 664	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) /\ ( x e. C /\ y e. x ) ) /\ ( o e. c /\ y e. o ) ) -> x e. { s e. C | ( s i^i o ) =/= (/) } )
31	30	expr 615	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) /\ ( x e. C /\ y e. x ) ) /\ o e. c ) -> ( y e. o -> x e. { s e. C | ( s i^i o ) =/= (/) } ) )
32	31	reximdva 2942	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) /\ ( x e. C /\ y e. x ) ) -> ( E. o e. c y e. o -> E. o e. c x e. { s e. C | ( s i^i o ) =/= (/) } ) )
33	21, 32	mpd 15	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) /\ ( x e. C /\ y e. x ) ) -> E. o e. c x e. { s e. C | ( s i^i o ) =/= (/) } )
34	33	expr 615	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) /\ x e. C ) -> ( y e. x -> E. o e. c x e. { s e. C | ( s i^i o ) =/= (/) } ) )
35	34	exlimdv 1700	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) /\ x e. C ) -> ( E. y y e. x -> E. o e. c x e. { s e. C | ( s i^i o ) =/= (/) } ) )
36		n0 3799	. . . . . . . . . . . . . . 15 |- ( x =/= (/) <-> E. y y e. x )
37		eliun 4336	. . . . . . . . . . . . . . 15 |- ( x e. U_ o e. c { s e. C | ( s i^i o ) =/= (/) } <-> E. o e. c x e. { s e. C | ( s i^i o ) =/= (/) } )
38	35, 36, 37	3imtr4g 270	. . . . . . . . . . . . . 14 |- ( ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) /\ x e. C ) -> ( x =/= (/) -> x e. U_ o e. c { s e. C | ( s i^i o ) =/= (/) } ) )
39	38	expimpd 603	. . . . . . . . . . . . 13 |- ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) -> ( ( x e. C /\ x =/= (/) ) -> x e. U_ o e. c { s e. C | ( s i^i o ) =/= (/) } ) )
40	8, 39	syl5bi 217	. . . . . . . . . . . 12 |- ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) -> ( x e. ( C \ { (/) } ) -> x e. U_ o e. c { s e. C | ( s i^i o ) =/= (/) } ) )
41	40	ssrdv 3515	. . . . . . . . . . 11 |- ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) -> ( C \ { (/) } ) C_ U_ o e. c { s e. C | ( s i^i o ) =/= (/) } )
42		iunfi 7820	. . . . . . . . . . . . 13 |- ( ( c e. Fin /\ A. o e. c { s e. C | ( s i^i o ) =/= (/) } e. Fin ) -> U_ o e. c { s e. C | ( s i^i o ) =/= (/) } e. Fin )
43	42	ex 434	. . . . . . . . . . . 12 |- ( c e. Fin -> ( A. o e. c { s e. C | ( s i^i o ) =/= (/) } e. Fin -> U_ o e. c { s e. C | ( s i^i o ) =/= (/) } e. Fin ) )
44		ssfi 7752	. . . . . . . . . . . . 13 |- ( ( U_ o e. c { s e. C | ( s i^i o ) =/= (/) } e. Fin /\ ( C \ { (/) } ) C_ U_ o e. c { s e. C | ( s i^i o ) =/= (/) } ) -> ( C \ { (/) } ) e. Fin )
45	44	expcom 435	. . . . . . . . . . . 12 |- ( ( C \ { (/) } ) C_ U_ o e. c { s e. C | ( s i^i o ) =/= (/) } -> ( U_ o e. c { s e. C | ( s i^i o ) =/= (/) } e. Fin -> ( C \ { (/) } ) e. Fin ) )
46	43, 45	sylan9 657	. . . . . . . . . . 11 |- ( ( c e. Fin /\ ( C \ { (/) } ) C_ U_ o e. c { s e. C | ( s i^i o ) =/= (/) } ) -> ( A. o e. c { s e. C | ( s i^i o ) =/= (/) } e. Fin -> ( C \ { (/) } ) e. Fin ) )
47	7, 41, 46	syl2anc 661	. . . . . . . . . 10 |- ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) -> ( A. o e. c { s e. C | ( s i^i o ) =/= (/) } e. Fin -> ( C \ { (/) } ) e. Fin ) )
48	47	expimpd 603	. . . . . . . . 9 |- ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) -> ( ( X = U. c /\ A. o e. c { s e. C | ( s i^i o ) =/= (/) } e. Fin ) -> ( C \ { (/) } ) e. Fin ) )
49	6, 48	sylan2b 475	. . . . . . . 8 |- ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ c e. ( ~P J i^i Fin ) ) -> ( ( X = U. c /\ A. o e. c { s e. C | ( s i^i o ) =/= (/) } e. Fin ) -> ( C \ { (/) } ) e. Fin ) )
50	49	rexlimdva 2959	. . . . . . 7 |- ( ( J e. Comp /\ C e. ( LocFin ` J ) ) -> ( E. c e. ( ~P J i^i Fin ) ( X = U. c /\ A. o e. c { s e. C | ( s i^i o ) =/= (/) } e. Fin ) -> ( C \ { (/) } ) e. Fin ) )
51	5, 50	mpd 15	. . . . . 6 |- ( ( J e. Comp /\ C e. ( LocFin ` J ) ) -> ( C \ { (/) } ) e. Fin )
52		snfi 7608	. . . . . 6 |- { (/) } e. Fin
53		unfi 7799	. . . . . 6 |- ( ( ( C \ { (/) } ) e. Fin /\ { (/) } e. Fin ) -> ( ( C \ { (/) } ) u. { (/) } ) e. Fin )
54	51, 52, 53	sylancl 662	. . . . 5 |- ( ( J e. Comp /\ C e. ( LocFin ` J ) ) -> ( ( C \ { (/) } ) u. { (/) } ) e. Fin )
55		ssun1 3672	. . . . . 6 |- C C_ ( C u. { (/) } )
56		undif1 3908	. . . . . 6 |- ( ( C \ { (/) } ) u. { (/) } ) = ( C u. { (/) } )
57	55, 56	sseqtr4i 3542	. . . . 5 |- C C_ ( ( C \ { (/) } ) u. { (/) } )
58		ssfi 7752	. . . . 5 |- ( ( ( ( C \ { (/) } ) u. { (/) } ) e. Fin /\ C C_ ( ( C \ { (/) } ) u. { (/) } ) ) -> C e. Fin )
59	54, 57, 58	sylancl 662	. . . 4 |- ( ( J e. Comp /\ C e. ( LocFin ` J ) ) -> C e. Fin )
60	59, 15	jca 532	. . 3 |- ( ( J e. Comp /\ C e. ( LocFin ` J ) ) -> ( C e. Fin /\ X = Y ) )
61	60	ex 434	. 2 |- ( J e. Comp -> ( C e. ( LocFin ` J ) -> ( C e. Fin /\ X = Y ) ) )
62		cmptop 19763	. . 3 |- ( J e. Comp -> J e. Top )
63	1, 10	finlocfin 19889	. . . 4 |- ( ( J e. Top /\ C e. Fin /\ X = Y ) -> C e. ( LocFin ` J ) )
64	63	3expib 1199	. . 3 |- ( J e. Top -> ( ( C e. Fin /\ X = Y ) -> C e. ( LocFin ` J ) ) )
65	62, 64	syl 16	. 2 |- ( J e. Comp -> ( ( C e. Fin /\ X = Y ) -> C e. ( LocFin ` J ) ) )
66	61, 65	impbid 191	1 |- ( J e. Comp -> ( C e. ( LocFin ` J ) <-> ( C e. Fin /\ X = Y ) ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1379   E.wex 1596   e. wcel 1767   =/= wne 2662   A.wral 2817   E.wrex 2818   {crab 2821   \ cdif 3478   u. cun 3479   i^i cin 3480   C_ wss 3481   (/)c0 3790   ~Pcpw 4016   {csn 4033   U.cuni 4251   U_ciun 4331   ` cfv 5594   Fincfn 7528   Topctop 19263   Compccmp 19754   LocFinclocfin 19873

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-reu 2824  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-pss 3497  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-tp 4038  df-op 4040  df-uni 4252  df-int 4289  df-iun 4333  df-br 4454  df-opab 4512  df-mpt 4513  df-tr 4547  df-eprel 4797  df-id 4801  df-po 4806  df-so 4807  df-fr 4844  df-we 4846  df-ord 4887  df-on 4888  df-lim 4889  df-suc 4890  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-om 6696  df-recs 7054  df-rdg 7088  df-1o 7142  df-oadd 7146  df-er 7323  df-en 7529  df-fin 7532  df-top 19268  df-cmp 19755  df-locfin 19876

This theorem is referenced by: (None)