Theorem locfincmp 28485

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 28483	. . . . . . . . 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 2797	. . . . . . . 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 18893	. . . . . . . 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 471	. . . . . . 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 7609	. . . . . . . . 9 |- ( c e. ( ~P J i^i Fin ) <-> ( c C_ J /\ c e. Fin ) )
7		simplrr 755	. . . . . . . . . . 11 |- ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) -> c e. Fin )
8		eldifsn 3997	. . . . . . . . . . . . 13 |- ( x e. ( C \ { (/) } ) <-> ( x e. C /\ x =/= (/) ) )
9		elunii 4093	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( y e. x /\ x e. C ) -> y e. U. C )
10		locfincmp.2	. . . . . . . . . . . . . . . . . . . . . . . 24 |- Y = U. C
11	9, 10	syl6eleqr 2532	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( y e. x /\ x e. C ) -> y e. Y )
12	11	ancoms 450	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( x e. C /\ y e. x ) -> y e. Y )
13	12	adantl 463	. . . . . . . . . . . . . . . . . . . . 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 28482	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( C e. ( LocFin ` J ) -> X = Y )
15	14	adantl 463	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( J e. Comp /\ C e. ( LocFin ` J ) ) -> X = Y )
16	15	ad3antrrr 724	. . . . . . . . . . . . . . . . . . . . 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 2518	. . . . . . . . . . . . . . . . . . . 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 749	. . . . . . . . . . . . . . . . . . . 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 2517	. . . . . . . . . . . . . . . . . . 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 4092	. . . . . . . . . . . . . . . . . . 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 754	. . . . . . . . . . . . . . . . . . . . 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 755	. . . . . . . . . . . . . . . . . . . . . 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 751	. . . . . . . . . . . . . . . . . . . . . 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 3730	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( y e. x /\ y e. o ) -> ( x i^i o ) =/= (/) )
26	23, 24, 25	syl2anc 656	. . . . . . . . . . . . . . . . . . . . 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 3542	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( s = x -> ( s i^i o ) = ( x i^i o ) )
28	27	neeq1d 2619	. . . . . . . . . . . . . . . . . . . . . 22 |- ( s = x -> ( ( s i^i o ) =/= (/) <-> ( x i^i o ) =/= (/) ) )
29	28	elrab 3114	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. { s e. C | ( s i^i o ) =/= (/) } <-> ( x e. C /\ ( x i^i o ) =/= (/) ) )
30	22, 26, 29	sylanbrc 659	. . . . . . . . . . . . . . . . . . . 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 612	. . . . . . . . . . . . . . . . . . 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 2826	. . . . . . . . . . . . . . . . . 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 612	. . . . . . . . . . . . . . . 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 1695	. . . . . . . . . . . . . . 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 3643	. . . . . . . . . . . . . . 15 |- ( x =/= (/) <-> E. y y e. x )
37		eliun 4172	. . . . . . . . . . . . . . 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 600	. . . . . . . . . . . . 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 3359	. . . . . . . . . . 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 7595	. . . . . . . . . . . . 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 7529	. . . . . . . . . . . . 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 652	. . . . . . . . . . 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 656	. . . . . . . . . 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 600	. . . . . . . . 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 472	. . . . . . . 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 2839	. . . . . . 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 7386	. . . . . 6 |- { (/) } e. Fin
53		unfi 7575	. . . . . 6 |- ( ( ( C \ { (/) } ) e. Fin /\ { (/) } e. Fin ) -> ( ( C \ { (/) } ) u. { (/) } ) e. Fin )
54	51, 52, 53	sylancl 657	. . . . 5 |- ( ( J e. Comp /\ C e. ( LocFin ` J ) ) -> ( ( C \ { (/) } ) u. { (/) } ) e. Fin )
55		ssun1 3516	. . . . . 6 |- C C_ ( C u. { (/) } )
56		undif1 3751	. . . . . 6 |- ( ( C \ { (/) } ) u. { (/) } ) = ( C u. { (/) } )
57	55, 56	sseqtr4i 3386	. . . . 5 |- C C_ ( ( C \ { (/) } ) u. { (/) } )
58		ssfi 7529	. . . . 5 |- ( ( ( ( C \ { (/) } ) u. { (/) } ) e. Fin /\ C C_ ( ( C \ { (/) } ) u. { (/) } ) ) -> C e. Fin )
59	54, 57, 58	sylancl 657	. . . 4 |- ( ( J e. Comp /\ C e. ( LocFin ` J ) ) -> C e. Fin )
60	59, 15	jca 529	. . 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 18898	. . 3 |- ( J e. Comp -> J e. Top )
63	1, 10	finlocfin 28480	. . . 4 |- ( ( J e. Top /\ C e. Fin /\ X = Y ) -> C e. ( LocFin ` J ) )
64	63	3expib 1185	. . 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 1364   E.wex 1591   e. wcel 1761   =/= wne 2604   A.wral 2713   E.wrex 2714   {crab 2717   \ cdif 3322   u. cun 3323   i^i cin 3324   C_ wss 3325   (/)c0 3634   ~Pcpw 3857   {csn 3874   U.cuni 4088   U_ciun 4168   ` cfv 5415   Fincfn 7306   Topctop 18398   Compccmp 18889   LocFinclocfin 28443

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2263  df-mo 2264  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-reu 2720  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-pss 3341  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-tp 3879  df-op 3881  df-uni 4089  df-int 4126  df-iun 4170  df-br 4290  df-opab 4348  df-mpt 4349  df-tr 4383  df-eprel 4628  df-id 4632  df-po 4637  df-so 4638  df-fr 4675  df-we 4677  df-ord 4718  df-on 4719  df-lim 4720  df-suc 4721  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-om 6476  df-recs 6828  df-rdg 6862  df-1o 6916  df-oadd 6920  df-er 7097  df-en 7307  df-fin 7310  df-top 18403  df-cmp 18890  df-locfin 28447

This theorem is referenced by: (None)