Theorem cctop 7545

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

Hypothesis

Ref	Expression
indistop.1	|- A e. V

Assertion

Ref	Expression
cctop	|- {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} e. Top

Distinct variable group:   x,A

Proof of Theorem cctop

Step	Hyp	Ref	Expression
1		indistop.1	. . . 4 |- A e. V
2		abssexg 2715	. . . 4 |- (A e. V -> {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} e. V)
3	1, 2	ax-mp 7	. . 3 |- {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} e. V
4		istopg 7489	. . 3 |- ({x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} e. V -> ({x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} e. Top <-> (A.y(y (_ {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} -> U.y e. {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))}) /\ A.y e. {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))}A.z e. {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} (y i^i z) e. {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))})))
5	3, 4	ax-mp 7	. 2 |- ({x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} e. Top <-> (A.y(y (_ {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} -> U.y e. {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))}) /\ A.y e. {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))}A.z e. {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} (y i^i z) e. {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))}))
6		uniss 2489	. . . . . 6 |- (y (_ {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} -> U.y (_ U.{x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))})
7		pm3.26 319	. . . . . . . . . . 11 |- ((x (_ A /\ ((A \ x) ~<_ om \/ x = (/))) -> x (_ A)
8	7	a1i 8	. . . . . . . . . 10 |- (x e. V -> ((x (_ A /\ ((A \ x) ~<_ om \/ x = (/))) -> x (_ A))
9	8	ss2rabi 2099	. . . . . . . . 9 |- {x e. V | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} (_ {x e. V | x (_ A}
10		uniss 2489	. . . . . . . . 9 |- ({x e. V | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} (_ {x e. V | x (_ A} -> U.{x e. V | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} (_ U.{x e. V | x (_ A})
11	9, 10	ax-mp 7	. . . . . . . 8 |- U.{x e. V | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} (_ U.{x e. V | x (_ A}
12		rabab 1797	. . . . . . . . 9 |- {x e. V | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} = {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))}
13	12	unieqi 2479	. . . . . . . 8 |- U.{x e. V | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} = U.{x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))}
14		unimax 2500	. . . . . . . . 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 2070	. . . . . . 7 |- U.{x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} (_ A
17		sstr 2043	. . . . . . 7 |- ((U.y (_ U.{x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} /\ U.{x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} (_ A) -> U.y (_ A)
18	16, 17	mpan2 693	. . . . . 6 |- (U.y (_ U.{x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} -> U.y (_ A)
19	6, 18	syl 10	. . . . 5 |- (y (_ {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} -> U.y (_ A)
20		ssel2 2035	. . . . . . . . . . . . . . . 16 |- ((y (_ {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} /\ z e. y) -> z e. {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))})
21		visset 1788	. . . . . . . . . . . . . . . . 17 |- z e. V
22		sseq1 2053	. . . . . . . . . . . . . . . . . 18 |- (x = z -> (x (_ A <-> z (_ A))
23		difeq2 2125	. . . . . . . . . . . . . . . . . . . 20 |- (x = z -> (A \ x) = (A \ z))
24	23	breq1d 2597	. . . . . . . . . . . . . . . . . . 19 |- (x = z -> ((A \ x) ~<_ om <-> (A \ z) ~<_ om))
25		eqeq1 1457	. . . . . . . . . . . . . . . . . . 19 |- (x = z -> (x = (/) <-> z = (/)))
26	24, 25	orbi12d 625	. . . . . . . . . . . . . . . . . 18 |- (x = z -> (((A \ x) ~<_ om \/ x = (/)) <-> ((A \ z) ~<_ om \/ z = (/))))
27	22, 26	anbi12d 626	. . . . . . . . . . . . . . . . 17 |- (x = z -> ((x (_ A /\ ((A \ x) ~<_ om \/ x = (/))) <-> (z (_ A /\ ((A \ z) ~<_ om \/ z = (/)))))
28	21, 27	elab 1869	. . . . . . . . . . . . . . . 16 |- (z e. {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} <-> (z (_ A /\ ((A \ z) ~<_ om \/ z = (/))))
29	20, 28	sylib 198	. . . . . . . . . . . . . . 15 |- ((y (_ {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} /\ z e. y) -> (z (_ A /\ ((A \ z) ~<_ om \/ z = (/))))
30	29	pm3.27d 325	. . . . . . . . . . . . . 14 |- ((y (_ {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} /\ z e. y) -> ((A \ z) ~<_ om \/ z = (/)))
31	30	ord 232	. . . . . . . . . . . . 13 |- ((y (_ {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} /\ z e. y) -> (-. (A \ z) ~<_ om -> z = (/)))
32	31	con1d 93	. . . . . . . . . . . 12 |- ((y (_ {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} /\ z e. y) -> (-. z = (/) -> (A \ z) ~<_ om))
33	32	imp 350	. . . . . . . . . . 11 |- (((y (_ {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} /\ z e. y) /\ -. z = (/)) -> (A \ z) ~<_ om)
34		domtr 4350	. . . . . . . . . . . 12 |- (((A \ U.y) ~<_ (A \ z) /\ (A \ z) ~<_ om) -> (A \ U.y) ~<_ om)
35		pm3.27 323	. . . . . . . . . . . . . . 15 |- ((y (_ {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} /\ z e. y) -> z e. y)
36	35	ad2antrr 404	. . . . . . . . . . . . . 14 |- ((((y (_ {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} /\ z e. y) /\ -. z = (/)) /\ (A \ z) ~<_ om) -> z e. y)
37		elssuni 2494	. . . . . . . . . . . . . 14 |- (z e. y -> z (_ U.y)
38	36, 37	syl 10	. . . . . . . . . . . . 13 |- ((((y (_ {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} /\ z e. y) /\ -. z = (/)) /\ (A \ z) ~<_ om) -> z (_ U.y)
39		sscon 2142	. . . . . . . . . . . . 13 |- (z (_ U.y -> (A \ U.y) (_ (A \ z))
40		difexg 2690	. . . . . . . . . . . . . . 15 |- (A e. V -> (A \ z) e. V)
41	1, 40	ax-mp 7	. . . . . . . . . . . . . 14 |- (A \ z) e. V
42		ssdom2g 4344	. . . . . . . . . . . . . 14 |- ((A \ z) e. V -> ((A \ U.y) (_ (A \ z) -> (A \ U.y) ~<_ (A \ z)))
43	41, 42	ax-mp 7	. . . . . . . . . . . . 13 |- ((A \ U.y) (_ (A \ z) -> (A \ U.y) ~<_ (A \ z))
44	38, 39, 43	3syl 20	. . . . . . . . . . . 12 |- ((((y (_ {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} /\ z e. y) /\ -. z = (/)) /\ (A \ z) ~<_ om) -> (A \ U.y) ~<_ (A \ z))
45		pm3.27 323	. . . . . . . . . . . 12 |- ((((y (_ {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} /\ z e. y) /\ -. z = (/)) /\ (A \ z) ~<_ om) -> (A \ z) ~<_ om)
46	34, 44, 45	sylanc 471	. . . . . . . . . . 11 |- ((((y (_ {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} /\ z e. y) /\ -. z = (/)) /\ (A \ z) ~<_ om) -> (A \