Theorem fctop 7592

Description: The finite complement topology on a set A. Example 3 in [Munkres] p. 77. (Contributed by FL, 15-Aug-2006.)

Hypothesis

Ref	Expression
indistop.1	|- A e. V

Assertion

Ref	Expression
fctop	|- {x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))} e. Top

Distinct variable group:   x,n,A

Proof of Theorem fctop

Step	Hyp	Ref	Expression
1		indistop.1	. . . 4 |- A e. V
2		abssexg 2737	. . . 4 |- (A e. V -> {x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))} e. V)
3	1, 2	ax-mp 7	. . 3 |- {x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))} e. V
4		istopg 7538	. . 3 |- ({x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))} e. V -> ({x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))} e. Top <-> (A.y(y (_ {x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))} -> U.y e. {x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))}) /\ A.y e. {x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))}A.z e. {x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))} (y i^i z) e. {x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))})))
5	3, 4	ax-mp 7	. 2 |- ({x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))} e. Top <-> (A.y(y (_ {x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))} -> U.y e. {x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))}) /\ A.y e. {x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))}A.z e. {x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))} (y i^i z) e. {x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))}))
6		uniss 2511	. . . . . 6 |- (y (_ {x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))} -> U.y (_ U.{x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))})
7		pm3.26 319	. . . . . . . . . . 11 |- ((x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/))) -> x (_ A)
8	7	a1i 8	. . . . . . . . . 10 |- (x e. V -> ((x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/))) -> x (_ A))
9	8	ss2rabi 2118	. . . . . . . . 9 |- {x e. V | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))} (_ {x e. V | x (_ A}
10		uniss 2511	. . . . . . . . 9 |- ({x e. V | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))} (_ {x e. V | x (_ A} -> U.{x e. V | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))} (_ U.{x e. V | x (_ A})
11	9, 10	ax-mp 7	. . . . . . . 8 |- U.{x e. V | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))} (_ U.{x e. V | x (_ A}
12		rabab 1813	. . . . . . . . 9 |- {x e. V | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))} = {x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))}
13	12	unieqi 2501	. . . . . . . 8 |- U.{x e. V | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))} = U.{x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))}
14		unimax 2522	. . . . . . . . 9 |- (A e. V -> U.{x e. V | x (_ A} = A)
15	1, 14	ax-mp 7	. . . . . . . 8 |- U.{x e. V | x (_ A} = A
16	11, 13, 15	3sstr3 2089	. . . . . . 7 |- U.{x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))} (_ A
17		sstr 2062	. . . . . . 7 |- ((U.y (_ U.{x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))} /\ U.{x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))} (_ A) -> U.y (_ A)
18	16, 17	mpan2 694	. . . . . 6 |- (U.y (_ U.{x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))} -> U.y (_ A)
19	6, 18	syl 10	. . . . 5 |- (y (_ {x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))} -> U.y (_ A)
20		ssel2 2054	. . . . . . . . . . . . . . . 16 |- ((y (_ {x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))} /\ z e. y) -> z e. {x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))})
21		visset 1804	. . . . . . . . . . . . . . . . 17 |- z e. V
22		sseq1 2072	. . . . . . . . . . . . . . . . . 18 |- (x = z -> (x (_ A <-> z (_ A))
23		difeq2 2144	. . . . . . . . . . . . . . . . . . . . 21 |- (x = z -> (A \ x) = (A \ z))
24	23	breq1d 2619	. . . . . . . . . . . . . . . . . . . 20 |- (x = z -> ((A \ x) ~~ n <-> (A \ z) ~~ n))
25	24	rexbidv 1656	. . . . . . . . . . . . . . . . . . 19 |- (x = z -> (E.n e. om (A \ x) ~~ n <-> E.n e. om (A \ z) ~~ n))
26		eqeq1 1473	. . . . . . . . . . . . . . . . . . 19 |- (x = z -> (x = (/) <-> z = (/)))
27	25, 26	orbi12d 625	. . . . . . . . . . . . . . . . . 18 |- (x = z -> ((E.n e. om (A \ x) ~~ n \/ x = (/)) <-> (E.n e. om (A \ z) ~~ n \/ z = (/))))
28	22, 27	anbi12d 626	. . . . . . . . . . . . . . . . 17 |- (x = z -> ((x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/))) <-> (z (_ A /\ (E.n e. om (A \ z) ~~ n \/ z = (/)))))
29	21, 28	elab 1888	. . . . . . . . . . . . . . . 16 |- (z e. {x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))} <-> (z (_ A /\ (E.n e. om (A \ z) ~~ n \/ z = (/))))
30	20, 29	sylib 198	. . . . . . . . . . . . . . 15 |- ((y (_ {x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))} /\ z e. y) -> (z (_ A /\ (E.n e. om (A \ z) ~~ n \/ z = (/))))
31	30	pm3.27d 325	. . . . . . . . . . . . . 14 |- ((y (_ {x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))} /\ z e. y) -> (E.n e. om (A \ z) ~~ n \/ z = (/)))
32	31	ord 232	. . . . . . . . . . . . 13 |- ((y (_ {x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))} /\ z e. y) -> (-. E.n e. om (A \ z) ~~ n -> z = (/)))
33	32	con1d 93	. . . . . . . . . . . 12 |- ((y (_ {x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))} /\ z e. y) -> (-. z = (/) -> E.n e. om (A \ z) ~~ n))
34	33	imp 350	. . . . . . . . . . 11 |- (((y (_ {x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))} /\ z e. y) /\ -. z = (/)) -> E.n e. om (A \ z) ~~ n)
35		ssfi 4515	. . . . . . . . . . . . . 14 |- ((E.n e. om (A \ z) ~~ n /\ (A \ U.y) (_ (A \ z)) -> E.n e. om (A \ U.y) ~~ n)
36		elssuni 2516	. . . . . . . . . . . . . . 15 |- (z e. y -> z (_ U.y)
37		sscon 2161	. . . . . . . . . . . . . . 15 |- (z (_ U.y -> (A \ U.y) (_ (A \ z))
38	36, 37	syl 10	. . . . . . . . . . . . . 14 |- (z e. y -> (A \ U.y) (_ (A \ z))
39	35, 38	sylan2 451	. . . . . . . . . . . . 13 |- ((E.n e. om (A \ z) ~~ n /\ z e. y) -> E.n e. om (A \ U.y) ~~ n)
40	39	expcom 374	. . . . . . . . . . . 12 |- (z e. y -> (E.n e. om (A \ z) ~~ n -> E.n e. om (A \ U.y) ~~ n))
41	40	ad2antlr 405	. . . . . . . . . . 11 |- (((y (_ {x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))} /\ z e. y) /\ -. z = (/)) -> (E.n e. om (A \ z) ~~ n -> E.n e. om (A \ U.y) ~~ n))
42	34, 41	mpd 26	. . . . . . . . . 10 |- (((y (_ {x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))} /\ z e. y) /\ -. z = (/)) -> E.n