Theorem cctop 7602

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 2742	. . . 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 7546	. . 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 2516	. . . . . 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 2124	. . . . . . . . 9 |- {x e. V | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} (_ {x e. V | x (_ A}
10		uniss 2516	. . . . . . . . 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 1818	. . . . . . . . 9 |- {x e. V | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} = {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))}
13	12	unieqi 2506	. . . . . . . 8 |- U.{x e. V | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} = U.{x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))}
14		unimax 2527	. . . . . . . . 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 2095	. . . . . . 7 |- U.{x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} (_ A
17		sstr 2068	. . . . . . 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 695	. . . . . 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 2060	. . . . . . . . . . . . . . . 16 |- ((y (_ {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} /\ z e. y) -> z e. {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))})
21		visset 1809	. . . . . . . . . . . . . . . . 17 |- z e. V
22		sseq1 2078	. . . . . . . . . . . . . . . . . 18 |- (x = z -> (x (_ A <-> z (_ A))
23		difeq2 2150	. . . . . . . . . . . . . . . . . . . 20 |- (x = z -> (A \ x) = (A \ z))
24	23	breq1d 2624	. . . . . . . . . . . . . . . . . . 19 |- (x = z -> ((A \ x) ~<_ om <-> (A \ z) ~<_ om))
25		eqeq1 1478	. . . . . . . . . . . . . . . . . . 19 |- (x = z -> (x = (/) <-> z = (/)))
26	24, 25	orbi12d 626	. . . . . . . . . . . . . . . . . 18 |- (x = z -> (((A \ x) ~<_ om \/ x = (/)) <-> ((A \ z) ~<_ om \/ z = (/))))
27	22, 26	anbi12d 627	. . . . . . . . . . . . . . . . 17 |- (x = z -> ((x (_ A /\ ((A \ x) ~<_ om \/ x = (/))) <-> (z (_ A /\ ((A \ z) ~<_ om \/ z = (/)))))
28	21, 27	elab 1893	. . . . . . . . . . . . . . . 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		pm3.27 323	. . . . . . . . . . . . . . 15 |- ((y (_ {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} /\ z e. y) -> z e. y)
35	34	ad2antrr 404	. . . . . . . . . . . . . 14 |- ((((y (_ {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} /\ z e. y) /\ -. z = (/)) /\ (A \ z) ~<_ om) -> z e. y)
36		elssuni 2521	. . . . . . . . . . . . . 14 |- (z e. y -> z (_ U.y)
37	35, 36	syl 10	. . . . . . . . . . . . 13 |- ((((y (_ {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} /\ z e. y) /\ -. z = (/)) /\ (A \ z) ~<_ om) -> z (_ U.y)
38		sscon 2167	. . . . . . . . . . . . 13 |- (z (_ U.y -> (A \ U.y) (_ (A \ z))
39		difexg 2717	. . . . . . . . . . . . . . 15 |- (A e. V -> (A \ z) e. V)
40	1, 39	ax-mp 7	. . . . . . . . . . . . . 14 |- (A \ z) e. V
41		ssdom2g 4396	. . . . . . . . . . . . . 14 |- ((A \ z) e. V -> ((A \ U.y) (_ (A \ z) -> (A \ U.y) ~<_ (A \ z)))
42	40, 41	ax-mp 7	. . . . . . . . . . . . 13 |- ((A \ U.y) (_ (A \ z) -> (A \ U.y) ~<_ (A \ z))
43	37, 38, 42	3syl 20	. . . . . . . . . . . 12 |- ((((y (_ {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} /\ z e. y) /\ -. z = (/)) /\ (A \ z) ~<_ om) -> (A \ U.y) ~<_ (A \ z))
44		domtr 4402	. . . . . . . . . . . 12 |- (((A \ U.y) ~<_ (A \ z) /\ (A \ z) ~<_ om) -> (A \ U.y) ~<_ om)
45	43, 44	sylancom 475	. . . . . . . . . . 11 |- ((((y (_ {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} /\ z e. y) /\ -. z = (/)) /\ (A \ z) ~<_ om) -> (A \ U.y) ~<_ om)
46	33, 45	mpdan 703	. . . . . . . . . 10 |- (((y (_ {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} /\ z e. y) /\ -. z = (/)) -> (A \ U.y) ~<_ om)
47	46	exp31 376	. . . . . . . . 9 |- (y