Theorem locfincomp 15514

Description: For a compact space, the locally finite covers are precisely the finite covers. Sadly, this property does not properly characterize all compact spaces.

Hypotheses

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

Assertion

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

Proof of Theorem locfincomp

Step	Hyp	Ref	Expression
1		simp1 876	. . . . . 6 |- ((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) -> J e. Comp)
2		ssrab2 2692	. . . . . . 7 |- {o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} C_ J
3	2	a1i 8	. . . . . 6 |- ((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) -> {o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} C_ J)
4		simpl2 880	. . . . . . . . . . . 12 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ x e. X) -> C e. A)
5		simpl3 881	. . . . . . . . . . . 12 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ x e. X) -> <.J, C>. e. LocFin)
6		simpr 350	. . . . . . . . . . . 12 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ x e. X) -> x e. X)
7		locfincomp.1	. . . . . . . . . . . . 13 |- X = U.J
8	7	locfinnei 15512	. . . . . . . . . . . 12 |- ((C e. A /\ <.J, C>. e. LocFin /\ x e. X) -> E.n e. ((nei` J)` {x}){s e. C | (s i^i n) =/= (/)} e. Fin)
9	4, 5, 6, 8	syl111anc 1100	. . . . . . . . . . 11 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ x e. X) -> E.n e. ((nei` J)` {x}){s e. C | (s i^i n) =/= (/)} e. Fin)
10		comptop 15428	. . . . . . . . . . . . . . . 16 |- (J e. Comp -> J e. Top)
11		neii2 8998	. . . . . . . . . . . . . . . . 17 |- ((J e. Top /\ n e. ((nei` J)` {x})) -> E.o e. J ({x} C_ o /\ o C_ n))
12	11	ex 402	. . . . . . . . . . . . . . . 16 |- (J e. Top -> (n e. ((nei` J)` {x}) -> E.o e. J ({x} C_ o /\ o C_ n)))
13	10, 12	syl 12	. . . . . . . . . . . . . . 15 |- (J e. Comp -> (n e. ((nei` J)` {x}) -> E.o e. J ({x} C_ o /\ o C_ n)))
14	13	3ad2ant1 897	. . . . . . . . . . . . . 14 |- ((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) -> (n e. ((nei` J)` {x}) -> E.o e. J ({x} C_ o /\ o C_ n)))
15	14	adantr 425	. . . . . . . . . . . . 13 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ x e. X) -> (n e. ((nei` J)` {x}) -> E.o e. J ({x} C_ o /\ o C_ n)))
16		visset 2295	. . . . . . . . . . . . . . . . . . . 20 |- x e. _V
17	16	snss 3122	. . . . . . . . . . . . . . . . . . 19 |- (x e. o <-> {x} C_ o)
18	17	biimpri 169	. . . . . . . . . . . . . . . . . 18 |- ({x} C_ o -> x e. o)
19	18	a1i 8	. . . . . . . . . . . . . . . . 17 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ (x e. X /\ {s e. C | (s i^i n) =/= (/)} e. Fin)) -> ({x} C_ o -> x e. o))
20		ssfi 5630	. . . . . . . . . . . . . . . . . . . 20 |- (({s e. C | (s i^i n) =/= (/)} e. Fin /\ {s e. C | (s i^i o) =/= (/)} C_ {s e. C | (s i^i n) =/= (/)}) -> {s e. C | (s i^i o) =/= (/)} e. Fin)
21	20	ex 402	. . . . . . . . . . . . . . . . . . 19 |- ({s e. C | (s i^i n) =/= (/)} e. Fin -> ({s e. C | (s i^i o) =/= (/)} C_ {s e. C | (s i^i n) =/= (/)} -> {s e. C | (s i^i o) =/= (/)} e. Fin))
22		sslin 2819	. . . . . . . . . . . . . . . . . . . . . . 23 |- (o C_ n -> (s i^i o) C_ (s i^i n))
23		ssn0 2905	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((s i^i o) C_ (s i^i n) /\ (s i^i o) =/= (/)) -> (s i^i n) =/= (/))
24	23	ex 402	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((s i^i o) C_ (s i^i n) -> ((s i^i o) =/= (/) -> (s i^i n) =/= (/)))
25	22, 24	syl 12	. . . . . . . . . . . . . . . . . . . . . 22 |- (o C_ n -> ((s i^i o) =/= (/) -> (s i^i n) =/= (/)))
26	25	a1d 15	. . . . . . . . . . . . . . . . . . . . 21 |- (o C_ n -> (s e. C -> ((s i^i o) =/= (/) -> (s i^i n) =/= (/))))
27	26	r19.21aiv 2175	. . . . . . . . . . . . . . . . . . . 20 |- (o C_ n -> A.s e. C ((s i^i o) =/= (/) -> (s i^i n) =/= (/)))
28		ss2rab 2683	. . . . . . . . . . . . . . . . . . . 20 |- ({s e. C | (s i^i o) =/= (/)} C_ {s e. C | (s i^i n) =/= (/)} <-> A.s e. C ((s i^i o) =/= (/) -> (s i^i n) =/= (/)))
29	27, 28	sylibr 217	. . . . . . . . . . . . . . . . . . 19 |- (o C_ n -> {s e. C | (s i^i o) =/= (/)} C_ {s e. C | (s i^i n) =/= (/)})
30	21, 29	syl5 20	. . . . . . . . . . . . . . . . . 18 |- ({s e. C | (s i^i n) =/= (/)} e. Fin -> (o C_ n -> {s e. C | (s i^i o) =/= (/)} e. Fin))
31	30	ad2antll 443	. . . . . . . . . . . . . . . . 17 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ (x e. X /\ {s e. C | (s i^i n) =/= (/)} e. Fin)) -> (o C_ n -> {s e. C | (s i^i o) =/= (/)} e. Fin))
32	19, 31	anim12d 617	. . . . . . . . . . . . . . . 16 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ (x e. X /\ {s e. C | (s i^i n) =/= (/)} e. Fin)) -> (({x} C_ o /\ o C_ n) -> (x e. o /\ {s e. C | (s i^i o) =/= (/)} e. Fin)))
33	32	reximdv 2202	. . . . . . . . . . . . . . 15 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ (x e. X /\ {s e. C | (s i^i n) =/= (/)} e. Fin)) -> (E.o e. J ({x} C_ o /\ o C_ n) -> E.o e. J (x e. o /\ {s e. C | (s i^i o) =/= (/)} e. Fin)))
34	33	expr 418	. . . . . . . . . . . . . 14 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ x e. X) -> ({s e. C | (s i^i n) =/= (/)} e. Fin -> (E.o e. J ({x} C_ o /\ o C_ n) -> E.o e. J (x e. o /\ {s e. C | (s i^i o) =/= (/)} e. Fin))))
35	34	com23 36	. . . . . . . . . . . . 13 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ x e. X) -> (E.o e. J ({x} C_ o /\ o C_ n) -> ({s e. C | (s i^i n) =/= (/)} e. Fin -> E.o e. J (x e. o /\ {s e. C | (s i^i o) =/= (/)} e. Fin))))
36	15, 35	syld 30	. . . . . . . . . . . 12 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ x e. X) -> (n e. ((nei` J)` {x}) -> ({s e. C | (s i^i n) =/= (/)} e. Fin -> E.o e. J (x e. o /\ {s e. C | (s i^i o) =/= (/)} e. Fin))))
37	36	r19.23adv 2215	. . . . . . . . . . 11 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ x e. X) -> (E.n e. ((nei` J)` {x}){s e. C | (s i^i n) =/= (/)} e. Fin -> E.o e. J (x e. o /\ {s e. C | (s i^i o) =/= (/)} e. Fin)))
38	9, 37	mpd 29	. . . . . . . . . 10 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ x e. X) -> E.o e. J (x e. o /\ {s e. C | (s i^i o) =/= (/)} e. Fin))
39	38	ex 402	. . . . . . . . 9 |- ((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) -> (x e. X -> E.o e. J (x e. o /\ {s e. C | (s i^i o) =/= (/)} e. Fin)))
40		elunirab 3190	. . . . . . . . 9 |- (x e. U.{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} <-> E.o e. J (x e. o /\ {s e. C | (s i^i o) =/= (/)} e. Fin))
41	39, 40	syl6ibr 230	. . . . . . . 8 |- ((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) -> (x e. X -> x e. U.{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin}))
42	41	ssrdv 2622	. . . . . . 7 |- ((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) -> X C_ U.{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin})
43		uniss 3199	. . . . . . . . . 10 |- ({o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} C_ J -> U.{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} C_ U.J)
44	2, 43	ax-mp 7	. . . . . . . . 9 |- U.{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} C_ U.J
45	44, 7	sseqtr4i 2650	. . . . . . . 8 |- U.{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} C_ X
46	45	a1i 8	. . . . . . 7 |- ((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) -> U.{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} C_ X)
47	42, 46	eqssd 2633	. . . . . 6 |- ((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) -> X = U.{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin})
48	7	compcov 15429	. . . . . 6 |- ((J e. Comp /\ {o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} C_ J /\ X = U.{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin}) -> E.c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin)X = U.c)
49	1, 3, 47, 48	syl111anc 1100	. . . . 5 |- ((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) -> E.c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin)X = U.c)
50		elunii 3182	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((x e. p /\ p e. C) -> x e. U.C)
51	50	ad2antll 443	. . . . . . . . . . . . . . . . . . . . . 22 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ ((c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) /\ X = U.c) /\ (x e. p /\ p e. C))) -> x e. U.C)
52		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- U.C = U.C
53	7, 52	locfinbas 15511	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((C e. A /\ <.J, C>. e. LocFin) -> X = U.C)
54	53	3adant1 894	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) -> X = U.C)
55	54	adantr 425	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ ((c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) /\ X = U.c) /\ (x e. p /\ p e. C))) -> X = U.C)
56		simprlr 457	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ ((c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) /\ X = U.c) /\ (x e. p /\ p e. C))) -> X = U.c)
57	55, 56	eqtr3d 1927	. . . . . . . . . . . . . . . . . . . . . 22 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ ((c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) /\ X = U.c) /\ (x e. p /\ p e. C))) -> U.C = U.c)
58	51, 57	eleqtrd 1973	. . . . . . . . . . . . . . . . . . . . 21 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ ((c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) /\ X = U.c) /\ (x e. p /\ p e. C))) -> x e. U.c)
59		eluni2 3181	. . . . . . . . . . . . . . . . . . . . 21 |- (x e. U.c <-> E.d e. c x e. d)
60	58, 59	sylib 215	. . . . . . . . . . . . . . . . . . . 20 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ ((c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) /\ X = U.c) /\ (x e. p /\ p e. C))) -> E.d e. c x e. d)
61		inelcm 2928	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((x e. p /\ x e. d) -> (p i^i d) =/= (/))
62	61	ex 402	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (x e. p -> (x e. d -> (p i^i d) =/= (/)))
63	62	adantr 425	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((x e. p /\ p e. C) -> (x e. d -> (p i^i d) =/= (/)))
64	63	ad2antll 443	. . . . . . . . . . . . . . . . . . . . . 22 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ ((c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) /\ X = U.c) /\ (x e. p /\ p e. C))) -> (x e. d -> (p i^i d) =/= (/)))
65		simprrr 459	. . . . . . . . . . . . . . . . . . . . . 22 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ ((c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) /\ X = U.c) /\ (x e. p /\ p e. C))) -> p e. C)
66	64, 65	jctild 662	. . . . . . . . . . . . . . . . . . . . 21 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ ((c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) /\ X = U.c) /\ (x e. p /\ p e. C))) -> (x e. d -> (p e. C /\ (p i^i d) =/= (/))))
67	66	reximdv 2202	. . . . . . . . . . . . . . . . . . . 20 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ ((c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) /\ X = U.c) /\ (x e. p /\ p e. C))) -> (E.d e. c x e. d -> E.d e. c (p e. C /\ (p i^i d) =/= (/))))
68	60, 67	mpd 29	. . . . . . . . . . . . . . . . . . 19 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ ((c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) /\ X = U.c) /\ (x e. p /\ p e. C))) -> E.d e. c (p e. C /\ (p i^i d) =/= (/)))
69	68	exp45 417	. . . . . . . . . . . . . . . . . 18 |- ((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) -> ((c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) /\ X = U.c) -> (x e. p -> (p e. C -> E.d e. c (p e. C /\ (p i^i d) =/= (/))))))
70	69	imp 377	. . . . . . . . . . . . . . . . 17 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ (c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) /\ X = U.c)) -> (x e. p -> (p e. C -> E.d e. c (p e. C /\ (p i^i d) =/= (/)))))
71	70	19.23adv 1584	. . . . . . . . . . . . . . . 16 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ (c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) /\ X = U.c)) -> (E.x x e. p -> (p e. C -> E.d e. c (p e. C /\ (p i^i d) =/= (/)))))
72		neq0 2885	. . . . . . . . . . . . . . . 16 |- (-. p = (/) <-> E.x x e. p)
73	71, 72	syl5ib 223	. . . . . . . . . . . . . . 15 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ (c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) /\ X = U.c)) -> (-. p = (/) -> (p e. C -> E.d e. c (p e. C /\ (p i^i d) =/= (/)))))
74	73	com23 36	. . . . . . . . . . . . . 14 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ (c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) /\ X = U.c)) -> (p e. C -> (-. p = (/) -> E.d e. c (p e. C /\ (p i^i d) =/= (/)))))
75	74	imp3a 388	. . . . . . . . . . . . 13 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ (c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) /\ X = U.c)) -> ((p e. C /\ -. p = (/)) -> E.d e. c (p e. C /\ (p i^i d) =/= (/))))
76		eliun 3259	. . . . . . . . . . . . . 14 |- (p e. U_d e. c {s e. C | (s i^i d) =/= (/)} <-> E.d e. c p e. {s e. C | (s i^i d) =/= (/)})
77		ineq1 2789	. . . . . . . . . . . . . . . . 17 |- (s = p -> (s i^i d) = (p i^i d))
78	77	neeq1d 2028	. . . . . . . . . . . . . . . 16 |- (s = p -> ((s i^i d) =/= (/) <-> (p i^i d) =/= (/)))
79	78	elrab 2414	. . . . . . . . . . . . . . 15 |- (p e. {s e. C | (s i^i d) =/= (/)} <-> (p e. C /\ (p i^i d) =/= (/)))
80	79	rexbii 2128	. . . . . . . . . . . . . 14 |- (E.d e. c p e. {s e. C | (s i^i d) =/= (/)} <-> E.d e. c (p e. C /\ (p i^i d) =/= (/)))
81	76, 80	bitr2i 191	. . . . . . . . . . . . 13 |- (E.d e. c (p e. C /\ (p i^i d) =/= (/)) <-> p e. U_d e. c {s e. C | (s i^i d) =/= (/)})
82	75, 81	syl6ib 229	. . . . . . . . . . . 12 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ (c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) /\ X = U.c)) -> ((p e. C /\ -. p = (/)) -> p e. U_d e. c {s e. C | (s i^i d) =/= (/)}))
83		eldif 2609	. . . . . . . . . . . . 13 |- (p e. (C \ {(/)}) <-> (p e. C /\ -. p e. {(/)}))
84		elsn 3058	. . . . . . . . . . . . . . 15 |- (p e. {(/)} <-> p = (/))
85	84	notbii 204	. . . . . . . . . . . . . 14 |- (-. p e. {(/)} <-> -. p = (/))
86	85	anbi2i 538	. . . . . . . . . . . . 13 |- ((p e. C /\ -. p e. {(/)}) <-> (p e. C /\ -. p = (/)))
87	83, 86	bitri 190	. . . . . . . . . . . 12 |- (p e. (C \ {(/)}) <-> (p e. C /\ -. p = (/)))
88	82, 87	syl5ib 223	. . . . . . . . . . 11 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ (c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) /\ X = U.c)) -> (p e. (C \ {(/)}) -> p e. U_d e. c {s e. C | (s i^i d) =/= (/)}))
89	88	ssrdv 2622	. . . . . . . . . 10 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ (c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) /\ X = U.c)) -> (C \ {(/)}) C_ U_d e. c {s e. C | (s i^i d) =/= (/)})
90		incom 2787	. . . . . . . . . . . . . . . . 17 |- ((/) i^i d) = (d i^i (/))
91		in0 2897	. . . . . . . . . . . . . . . . 17 |- (d i^i (/)) = (/)
92	90, 91	eqtri 1908	. . . . . . . . . . . . . . . 16 |- ((/) i^i d) = (/)
93		nne 2021	. . . . . . . . . . . . . . . 16 |- (-. ((/) i^i d) =/= (/) <-> ((/) i^i d) = (/))
94	92, 93	mpbir 207	. . . . . . . . . . . . . . 15 |- -. ((/) i^i d) =/= (/)
95	94	a1i12 9	. . . . . . . . . . . . . 14 |- (d e. c -> ((/) e. C -> -. ((/) i^i d) =/= (/)))
96	95	rgen 2159	. . . . . . . . . . . . 13 |- A.d e. c ((/) e. C -> -. ((/) i^i d) =/= (/))
97	96	a1i 8	. . . . . . . . . . . 12 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ (c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) /\ X = U.c)) -> A.d e. c ((/) e. C -> -. ((/) i^i d) =/= (/)))
98		eliun 3259	. . . . . . . . . . . . . . 15 |- ((/) e. U_d e. c {s e. C | (s i^i d) =/= (/)} <-> E.d e. c (/) e. {s e. C | (s i^i d) =/= (/)})
99		ineq1 2789	. . . . . . . . . . . . . . . . . 18 |- (s = (/) -> (s i^i d) = ((/) i^i d))
100	99	neeq1d 2028	. . . . . . . . . . . . . . . . 17 |- (s = (/) -> ((s i^i d) =/= (/) <-> ((/) i^i d) =/= (/)))
101	100	elrab 2414	. . . . . . . . . . . . . . . 16 |- ((/) e. {s e. C | (s i^i d) =/= (/)} <-> ((/) e. C /\ ((/) i^i d) =/= (/)))
102	101	rexbii 2128	. . . . . . . . . . . . . . 15 |- (E.d e. c (/) e. {s e. C | (s i^i d) =/= (/)} <-> E.d e. c ((/) e. C /\ ((/) i^i d) =/= (/)))
103	98, 102	bitr2i 191	. . . . . . . . . . . . . 14 |- (E.d e. c ((/) e. C /\ ((/) i^i d) =/= (/)) <-> (/) e. U_d e. c {s e. C | (s i^i d) =/= (/)})
104	103	notbii 204	. . . . . . . . . . . . 13 |- (-. E.d e. c ((/) e. C /\ ((/) i^i d) =/= (/)) <-> -. (/) e. U_d e. c {s e. C | (s i^i d) =/= (/)})
105		ralinexa 2143	. . . . . . . . . . . . 13 |- (A.d e. c ((/) e. C -> -. ((/) i^i d) =/= (/)) <-> -. E.d e. c ((/) e. C /\ ((/) i^i d) =/= (/)))
106		disjsn 3089	. . . . . . . . . . . . 13 |- ((U_d e. c {s e. C | (s i^i d) =/= (/)} i^i {(/)}) = (/) <-> -. (/) e. U_d e. c {s e. C | (s i^i d) =/= (/)})
107	104, 105, 106	3bitr4i 200	. . . . . . . . . . . 12 |- (A.d e. c ((/) e. C -> -. ((/) i^i d) =/= (/)) <-> (U_d e. c {s e. C | (s i^i d) =/= (/)} i^i {(/)}) = (/))
108	97, 107	sylib 215	. . . . . . . . . . 11 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ (c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) /\ X = U.c)) -> (U_d e. c {s e. C | (s i^i d) =/= (/)} i^i {(/)}) = (/))
109		iunss 3291	. . . . . . . . . . . . . 14 |- (U_d e. c {s e. C | (s i^i d) =/= (/)} C_ C <-> A.d e. c {s e. C | (s i^i d) =/= (/)} C_ C)
110		ssrab2 2692	. . . . . . . . . . . . . . 15 |- {s e. C | (s i^i d) =/= (/)} C_ C
111	110	a1i 8	. . . . . . . . . . . . . 14 |- (d e. c -> {s e. C | (s i^i d) =/= (/)} C_ C)
112	109, 111	mprgbir 2163	. . . . . . . . . . . . 13 |- U_d e. c {s e. C | (s i^i d) =/= (/)} C_ C
113	112	a1i 8	. . . . . . . . . . . 12 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ (c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) /\ X = U.c)) -> U_d e. c {s e. C | (s i^i d) =/= (/)} C_ C)
114		reldisj 2916	. . . . . . . . . . . 12 |- (U_d e. c {s e. C | (s i^i d) =/= (/)} C_ C -> ((U_d e. c {s e. C | (s i^i d) =/= (/)} i^i {(/)}) = (/) <-> U_d e. c {s e. C | (s i^i d) =/= (/)} C_ (C \ {(/)})))
115	113, 114	syl 12	. . . . . . . . . . 11 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ (c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) /\ X = U.c)) -> ((U_d e. c {s e. C | (s i^i d) =/= (/)} i^i {(/)}) = (/) <-> U_d e. c {s e. C | (s i^i d) =/= (/)} C_ (C \ {(/)})))
116	108, 115	mpbid 212	. . . . . . . . . 10 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ (c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) /\ X = U.c)) -> U_d e. c {s e. C | (s i^i d) =/= (/)} C_ (C \ {(/)}))
117	89, 116	eqssd 2633	. . . . . . . . 9 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ (c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) /\ X = U.c)) -> (C \ {(/)}) = U_d e. c {s e. C | (s i^i d) =/= (/)})
118		inss2 2813	. . . . . . . . . . . 12 |- (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) C_ Fin
119	118	sseli 2617	. . . . . . . . . . 11 |- (c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) -> c e. Fin)
120	119	ad2antrl 442	. . . . . . . . . 10 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ (c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) /\ X = U.c)) -> c e. Fin)
121		inss1 2812	. . . . . . . . . . . . 13 |- (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) C_ ~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin}
122	121	sseli 2617	. . . . . . . . . . . 12 |- (c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) -> c e. ~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin})
123		visset 2295	. . . . . . . . . . . . . 14 |- c e. _V
124	123	elpw 3037	. . . . . . . . . . . . 13 |- (c e. ~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} <-> c C_ {o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin})
125		ssel 2615	. . . . . . . . . . . . . . 15 |- (c C_ {o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} -> (d e. c -> d e. {o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin}))
126		ineq2 2790	. . . . . . . . . . . . . . . . . . . 20 |- (o = d -> (s i^i o) = (s i^i d))
127	126	neeq1d 2028	. . . . . . . . . . . . . . . . . . 19 |- (o = d -> ((s i^i o) =/= (/) <-> (s i^i d) =/= (/)))
128	127	rabbidv 2287	. . . . . . . . . . . . . . . . . 18 |- (o = d -> {s e. C | (s i^i o) =/= (/)} = {s e. C | (s i^i d) =/= (/)})
129	128	eleq1d 1963	. . . . . . . . . . . . . . . . 17 |- (o = d -> ({s e. C | (s i^i o) =/= (/)} e. Fin <-> {s e. C | (s i^i d) =/= (/)} e. Fin))
130	129	elrab 2414	. . . . . . . . . . . . . . . 16 |- (d e. {o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} <-> (d e. J /\ {s e. C | (s i^i d) =/= (/)} e. Fin))
131	130	simprbi 353	. . . . . . . . . . . . . . 15 |- (d e. {o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} -> {s e. C | (s i^i d) =/= (/)} e. Fin)
132	125, 131	syl6 25	. . . . . . . . . . . . . 14 |- (c C_ {o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} -> (d e. c -> {s e. C | (s i^i d) =/= (/)} e. Fin))
133	132	r19.21aiv 2175	. . . . . . . . . . . . 13 |- (c C_ {o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} -> A.d e. c {s e. C | (s i^i d) =/= (/)} e. Fin)
134	124, 133	sylbi 216	. . . . . . . . . . . 12 |- (c e. ~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} -> A.d e. c {s e. C | (s i^i d) =/= (/)} e. Fin)
135	122, 134	syl 12	. . . . . . . . . . 11 |- (c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) -> A.d e. c {s e. C | (s i^i d) =/= (/)} e. Fin)
136	135	ad2antrl 442	. . . . . . . . . 10 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ (c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) /\ X = U.c)) -> A.d e. c {s e. C | (s i^i d) =/= (/)} e. Fin)
137		iunfi 5659	. . . . . . . . . 10 |- ((c e. Fin /\ A.d e. c {s e. C | (s i^i d) =/= (/)} e. Fin) -> U_d e. c {s e. C | (s i^i d) =/= (/)} e. Fin)
138	120, 136, 137	syl11anc 524	. . . . . . . . 9 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ (c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) /\ X = U.c)) -> U_d e. c {s e. C | (s i^i d) =/= (/)} e. Fin)
139	117, 138	eqeltrd 1971	. . . . . . . 8 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ (c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) /\ X = U.c)) -> (C \ {(/)}) e. Fin)
140		snfi 5491	. . . . . . . . 9 |- {(/)} e. Fin
141		unfi 5644	. . . . . . . . 9 |- (((C \ {(/)}) e. Fin /\ {(/)} e. Fin) -> ((C \ {(/)}) u. {(/)}) e. Fin)
142	140, 141	mpan2 760	. . . . . . . 8 |- ((C \ {(/)}) e. Fin -> ((C \ {(/)}) u. {(/)}) e. Fin)
143		pm2.27 76	. . . . . . . . . . . 12 |- (d e. C -> ((d e. C -> d e. {(/)}) -> d e. {(/)}))
144		iman 256	. . . . . . . . . . . 12 |- ((d e. C -> d e. {(/)}) <-> -. (d e. C /\ -. d e. {(/)}))
145		elsn 3058	. . . . . . . . . . . 12 |- (d e. {(/)} <-> d = (/))
146	143, 144, 145	3imtr3g 611	. . . . . . . . . . 11 |- (d e. C -> (-. (d e. C /\ -. d e. {(/)}) -> d = (/)))
147		elun 2741	. . . . . . . . . . . 12 |- (d e. ((C \ {(/)}) u. {(/)}) <-> (d e. (C \ {(/)}) \/ d e. {(/)}))
148		eldif 2609	. . . . . . . . . . . . 13 |- (d e. (C \ {(/)}) <-> (d e. C /\ -. d e. {(/)}))
149	148, 145	orbi12i 277	. . . . . . . . . . . 12 |- ((d e. (C \ {(/)}) \/ d e. {(/)}) <-> ((d e. C /\ -. d e. {(/)}) \/ d = (/)))
150		df-or 241	. . . . . . . . . . . 12 |- (((d e. C /\ -. d e. {(/)}) \/ d = (/)) <-> (-. (d e. C /\ -. d e. {(/)}) -> d = (/)))
151	147, 149, 150	3bitrri 195	. . . . . . . . . . 11 |- ((-. (d e. C /\ -. d e. {(/)}) -> d = (/)) <-> d e. ((C \ {(/)}) u. {(/)}))
152	146, 151	sylib 215	. . . . . . . . . 10 |- (d e. C -> d e. ((C \ {(/)}) u. {(/)}))
153	152	ssriv 2621	. . . . . . . . 9 |- C C_ ((C \ {(/)}) u. {(/)})
154		ssfi 5630	. . . . . . . . 9 |- ((((C \ {(/)}) u. {(/)}) e. Fin /\ C C_ ((C \ {(/)}) u. {(/)})) -> C e. Fin)
155	153, 154	mpan2 760	. . . . . . . 8 |- (((C \ {(/)}) u. {(/)}) e. Fin -> C e. Fin)
156	139, 142, 155	3syl 24	. . . . . . 7 |- (((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) /\ (c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) /\ X = U.c)) -> C e. Fin)
157	156	exp32 408	. . . . . 6 |- ((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) -> (c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin) -> (X = U.c -> C e. Fin)))
158	157	r19.23adv 2215	. . . . 5 |- ((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) -> (E.c e. (~P{o e. J | {s e. C | (s i^i o) =/= (/)} e. Fin} i^i Fin)X = U.c -> C e. Fin))
159	49, 158	mpd 29	. . . 4 |- ((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) -> C e. Fin)
160		locfincomp.2	. . . . . 6 |- Y = U.C
161	7, 160	locfinbas 15511	. . . . 5 |- ((C e. A /\ <.J, C>. e. LocFin) -> X = Y)
162	161	3adant1 894	. . . 4 |- ((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) -> X = Y)
163	159, 162	jca 310	. . 3 |- ((J e. Comp /\ C e. A /\ <.J, C>. e. LocFin) -> (C e. Fin /\ X = Y))
164	163	3expia 1069	. 2 |- ((J e. Comp /\ C e. A) -> (<.J, C>. e. LocFin -> (C e. Fin /\ X = Y)))
165	7, 160	finlocfin 15509	. . . . 5 |- ((J e. Top /\ C e. Fin /\ X = Y) -> <.J, C>. e. LocFin)
166	165	3expib 1070	. . . 4 |- (J e. Top -> ((C e. Fin /\ X = Y) -> <.J, C>. e. LocFin))
167	10, 166	syl 12	. . 3 |- (J e. Comp -> ((C e. Fin /\ X = Y) -> <.J, C>. e. LocFin))
168	167	adantr 425	. 2 |- ((J e. Comp /\ C e. A) -> ((C e. Fin /\ X = Y) -> <.J, C>. e. LocFin))
169	164, 168	impbid 574	1 |- ((J e. Comp /\ C e. A) -> (<.J, C>. e. LocFin <-> (C e. Fin /\ X = Y)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326   =/= wne 2017  A.wral 2105  E.wrex 2106  {crab 2108   \ cdif 2590   u. cun 2591   i^i cin 2592   C_ wss 2593  (/)c0 2875  ~Pcpw 3032  {csn 3044  <.cop 3046  U.cuni 3177  U_ciun 3255  ` cfv 3998  Fincfn 5426  Topctop 8857  neicnei 8988  Compccomp 10328  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-3or 859  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-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  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-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-rdg 5140  df-1o 5177  df-oadd 5179  df-er 5318  df-en 5427  df-dom 5428  df-fin 5430  df-top 8861  df-nei 8989  df-comp 10329  df-locfin 15466

Copyright terms: Public domain