Theorem mretopd 20896

Description: A Moore collection which is closed under finite unions called topological; such a collection is the closed sets of a canonically associated topology. (Contributed by Stefan O'Rear, 1-Feb-2015.)

Hypotheses

Ref	Expression
mretopd.m	|- ( ph -> M e. (Moore ` B ) )
mretopd.z	|- ( ph -> (/) e. M )
mretopd.u	|- ( ( ph /\ x e. M /\ y e. M ) -> ( x u. y ) e. M )
mretopd.j	|- J = { z e. ~P B | ( B \ z ) e. M }

Assertion

Ref	Expression
mretopd	|- ( ph -> ( J e. (TopOn ` B ) /\ M = ( Clsd ` J ) ) )

Distinct variable groups:   ph, x, y, z   x, M, y, z   x, J, y   x, B, y, z

Allowed substitution hint:   J( z)

Proof of Theorem mretopd

Dummy variables a b are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		unieq 4444	. . . . . . . . 9 |- ( a = (/) -> U. a = U. (/) )
2		uni0 4465	. . . . . . . . 9 |- U. (/) = (/)
3	1, 2	syl6eq 2672	. . . . . . . 8 |- ( a = (/) -> U. a = (/) )
4	3	eleq1d 2686	. . . . . . 7 |- ( a = (/) -> ( U. a e. J <-> (/) e. J ) )
5		mretopd.j	. . . . . . . . . . . . . 14 |- J = { z e. ~P B | ( B \ z ) e. M }
6		ssrab2 3687	. . . . . . . . . . . . . 14 |- { z e. ~P B | ( B \ z ) e. M } C_ ~P B
7	5, 6	eqsstri 3635	. . . . . . . . . . . . 13 |- J C_ ~P B
8		sstr 3611	. . . . . . . . . . . . 13 |- ( ( a C_ J /\ J C_ ~P B ) -> a C_ ~P B )
9	7, 8	mpan2 707	. . . . . . . . . . . 12 |- ( a C_ J -> a C_ ~P B )
10	9	adantl 482	. . . . . . . . . . 11 |- ( ( ph /\ a C_ J ) -> a C_ ~P B )
11		sspwuni 4611	. . . . . . . . . . 11 |- ( a C_ ~P B <-> U. a C_ B )
12	10, 11	sylib 208	. . . . . . . . . 10 |- ( ( ph /\ a C_ J ) -> U. a C_ B )
13		vuniex 6954	. . . . . . . . . . 11 |- U. a e. _V
14	13	elpw 4164	. . . . . . . . . 10 |- ( U. a e. ~P B <-> U. a C_ B )
15	12, 14	sylibr 224	. . . . . . . . 9 |- ( ( ph /\ a C_ J ) -> U. a e. ~P B )
16	15	adantr 481	. . . . . . . 8 |- ( ( ( ph /\ a C_ J ) /\ a =/= (/) ) -> U. a e. ~P B )
17		uniiun 4573	. . . . . . . . . 10 |- U. a = U_ b e. a b
18	17	difeq2i 3725	. . . . . . . . 9 |- ( B \ U. a ) = ( B \ U_ b e. a b )
19		iindif2 4589	. . . . . . . . . . 11 |- ( a =/= (/) -> |^|_ b e. a ( B \ b ) = ( B \ U_ b e. a b ) )
20	19	adantl 482	. . . . . . . . . 10 |- ( ( ( ph /\ a C_ J ) /\ a =/= (/) ) -> |^|_ b e. a ( B \ b ) = ( B \ U_ b e. a b ) )
21		mretopd.m	. . . . . . . . . . . 12 |- ( ph -> M e. (Moore ` B ) )
22	21	ad2antrr 762	. . . . . . . . . . 11 |- ( ( ( ph /\ a C_ J ) /\ a =/= (/) ) -> M e. (Moore ` B ) )
23		simpr 477	. . . . . . . . . . 11 |- ( ( ( ph /\ a C_ J ) /\ a =/= (/) ) -> a =/= (/) )
24		difeq2 3722	. . . . . . . . . . . . . . . . 17 |- ( z = b -> ( B \ z ) = ( B \ b ) )
25	24	eleq1d 2686	. . . . . . . . . . . . . . . 16 |- ( z = b -> ( ( B \ z ) e. M <-> ( B \ b ) e. M ) )
26	25, 5	elrab2 3366	. . . . . . . . . . . . . . 15 |- ( b e. J <-> ( b e. ~P B /\ ( B \ b ) e. M ) )
27	26	simprbi 480	. . . . . . . . . . . . . 14 |- ( b e. J -> ( B \ b ) e. M )
28	27	rgen 2922	. . . . . . . . . . . . 13 |- A. b e. J ( B \ b ) e. M
29		ssralv 3666	. . . . . . . . . . . . . 14 |- ( a C_ J -> ( A. b e. J ( B \ b ) e. M -> A. b e. a ( B \ b ) e. M ) )
30	29	adantl 482	. . . . . . . . . . . . 13 |- ( ( ph /\ a C_ J ) -> ( A. b e. J ( B \ b ) e. M -> A. b e. a ( B \ b ) e. M ) )
31	28, 30	mpi 20	. . . . . . . . . . . 12 |- ( ( ph /\ a C_ J ) -> A. b e. a ( B \ b ) e. M )
32	31	adantr 481	. . . . . . . . . . 11 |- ( ( ( ph /\ a C_ J ) /\ a =/= (/) ) -> A. b e. a ( B \ b ) e. M )
33		mreiincl 16256	. . . . . . . . . . 11 |- ( ( M e. (Moore ` B ) /\ a =/= (/) /\ A. b e. a ( B \ b ) e. M ) -> |^|_ b e. a ( B \ b ) e. M )
34	22, 23, 32, 33	syl3anc 1326	. . . . . . . . . 10 |- ( ( ( ph /\ a C_ J ) /\ a =/= (/) ) -> |^|_ b e. a ( B \ b ) e. M )
35	20, 34	eqeltrrd 2702	. . . . . . . . 9 |- ( ( ( ph /\ a C_ J ) /\ a =/= (/) ) -> ( B \ U_ b e. a b ) e. M )
36	18, 35	syl5eqel 2705	. . . . . . . 8 |- ( ( ( ph /\ a C_ J ) /\ a =/= (/) ) -> ( B \ U. a ) e. M )
37		difeq2 3722	. . . . . . . . . 10 |- ( z = U. a -> ( B \ z ) = ( B \ U. a ) )
38	37	eleq1d 2686	. . . . . . . . 9 |- ( z = U. a -> ( ( B \ z ) e. M <-> ( B \ U. a ) e. M ) )
39	38, 5	elrab2 3366	. . . . . . . 8 |- ( U. a e. J <-> ( U. a e. ~P B /\ ( B \ U. a ) e. M ) )
40	16, 36, 39	sylanbrc 698	. . . . . . 7 |- ( ( ( ph /\ a C_ J ) /\ a =/= (/) ) -> U. a e. J )
41		0elpw 4834	. . . . . . . . . 10 |- (/) e. ~P B
42	41	a1i 11	. . . . . . . . 9 |- ( ph -> (/) e. ~P B )
43		mre1cl 16254	. . . . . . . . . 10 |- ( M e. (Moore ` B ) -> B e. M )
44	21, 43	syl 17	. . . . . . . . 9 |- ( ph -> B e. M )
45		difeq2 3722	. . . . . . . . . . . 12 |- ( z = (/) -> ( B \ z ) = ( B \ (/) ) )
46		dif0 3950	. . . . . . . . . . . 12 |- ( B \ (/) ) = B
47	45, 46	syl6eq 2672	. . . . . . . . . . 11 |- ( z = (/) -> ( B \ z ) = B )
48	47	eleq1d 2686	. . . . . . . . . 10 |- ( z = (/) -> ( ( B \ z ) e. M <-> B e. M ) )
49	48, 5	elrab2 3366	. . . . . . . . 9 |- ( (/) e. J <-> ( (/) e. ~P B /\ B e. M ) )
50	42, 44, 49	sylanbrc 698	. . . . . . . 8 |- ( ph -> (/) e. J )
51	50	adantr 481	. . . . . . 7 |- ( ( ph /\ a C_ J ) -> (/) e. J )
52	4, 40, 51	pm2.61ne 2879	. . . . . 6 |- ( ( ph /\ a C_ J ) -> U. a e. J )
53	52	ex 450	. . . . 5 |- ( ph -> ( a C_ J -> U. a e. J ) )
54	53	alrimiv 1855	. . . 4 |- ( ph -> A. a ( a C_ J -> U. a e. J ) )
55		inss1 3833	. . . . . . . 8 |- ( a i^i b ) C_ a
56		difeq2 3722	. . . . . . . . . . . . 13 |- ( z = a -> ( B \ z ) = ( B \ a ) )
57	56	eleq1d 2686	. . . . . . . . . . . 12 |- ( z = a -> ( ( B \ z ) e. M <-> ( B \ a ) e. M ) )
58	57, 5	elrab2 3366	. . . . . . . . . . 11 |- ( a e. J <-> ( a e. ~P B /\ ( B \ a ) e. M ) )
59	58	simplbi 476	. . . . . . . . . 10 |- ( a e. J -> a e. ~P B )
60	59	elpwid 4170	. . . . . . . . 9 |- ( a e. J -> a C_ B )
61	60	ad2antrl 764	. . . . . . . 8 |- ( ( ph /\ ( a e. J /\ b e. J ) ) -> a C_ B )
62	55, 61	syl5ss 3614	. . . . . . 7 |- ( ( ph /\ ( a e. J /\ b e. J ) ) -> ( a i^i b ) C_ B )
63		vex 3203	. . . . . . . . 9 |- a e. _V
64	63	inex1 4799	. . . . . . . 8 |- ( a i^i b ) e. _V
65	64	elpw 4164	. . . . . . 7 |- ( ( a i^i b ) e. ~P B <-> ( a i^i b ) C_ B )
66	62, 65	sylibr 224	. . . . . 6 |- ( ( ph /\ ( a e. J /\ b e. J ) ) -> ( a i^i b ) e. ~P B )
67		difindi 3881	. . . . . . 7 |- ( B \ ( a i^i b ) ) = ( ( B \ a ) u. ( B \ b ) )
68	58	simprbi 480	. . . . . . . . 9 |- ( a e. J -> ( B \ a ) e. M )
69	68	ad2antrl 764	. . . . . . . 8 |- ( ( ph /\ ( a e. J /\ b e. J ) ) -> ( B \ a ) e. M )
70	27	ad2antll 765	. . . . . . . 8 |- ( ( ph /\ ( a e. J /\ b e. J ) ) -> ( B \ b ) e. M )
71		simpl 473	. . . . . . . 8 |- ( ( ph /\ ( a e. J /\ b e. J ) ) -> ph )
72		uneq1 3760	. . . . . . . . . . . 12 |- ( x = ( B \ a ) -> ( x u. y ) = ( ( B \ a ) u. y ) )
73	72	eleq1d 2686	. . . . . . . . . . 11 |- ( x = ( B \ a ) -> ( ( x u. y ) e. M <-> ( ( B \ a ) u. y ) e. M ) )
74	73	imbi2d 330	. . . . . . . . . 10 |- ( x = ( B \ a ) -> ( ( ph -> ( x u. y ) e. M ) <-> ( ph -> ( ( B \ a ) u. y ) e. M ) ) )
75		uneq2 3761	. . . . . . . . . . . 12 |- ( y = ( B \ b ) -> ( ( B \ a ) u. y ) = ( ( B \ a ) u. ( B \ b ) ) )
76	75	eleq1d 2686	. . . . . . . . . . 11 |- ( y = ( B \ b ) -> ( ( ( B \ a ) u. y ) e. M <-> ( ( B \ a ) u. ( B \ b ) ) e. M ) )
77	76	imbi2d 330	. . . . . . . . . 10 |- ( y = ( B \ b ) -> ( ( ph -> ( ( B \ a ) u. y ) e. M ) <-> ( ph -> ( ( B \ a ) u. ( B \ b ) ) e. M ) ) )
78		mretopd.u	. . . . . . . . . . . 12 |- ( ( ph /\ x e. M /\ y e. M ) -> ( x u. y ) e. M )
79	78	3expb 1266	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. M /\ y e. M ) ) -> ( x u. y ) e. M )
80	79	expcom 451	. . . . . . . . . 10 |- ( ( x e. M /\ y e. M ) -> ( ph -> ( x u. y ) e. M ) )
81	74, 77, 80	vtocl2ga 3274	. . . . . . . . 9 |- ( ( ( B \ a ) e. M /\ ( B \ b ) e. M ) -> ( ph -> ( ( B \ a ) u. ( B \ b ) ) e. M ) )
82	81	imp 445	. . . . . . . 8 |- ( ( ( ( B \ a ) e. M /\ ( B \ b ) e. M ) /\ ph ) -> ( ( B \ a ) u. ( B \ b ) ) e. M )
83	69, 70, 71, 82	syl21anc 1325	. . . . . . 7 |- ( ( ph /\ ( a e. J /\ b e. J ) ) -> ( ( B \ a ) u. ( B \ b ) ) e. M )
84	67, 83	syl5eqel 2705	. . . . . 6 |- ( ( ph /\ ( a e. J /\ b e. J ) ) -> ( B \ ( a i^i b ) ) e. M )
85		difeq2 3722	. . . . . . . 8 |- ( z = ( a i^i b ) -> ( B \ z ) = ( B \ ( a i^i b ) ) )
86	85	eleq1d 2686	. . . . . . 7 |- ( z = ( a i^i b ) -> ( ( B \ z ) e. M <-> ( B \ ( a i^i b ) ) e. M ) )
87	86, 5	elrab2 3366	. . . . . 6 |- ( ( a i^i b ) e. J <-> ( ( a i^i b ) e. ~P B /\ ( B \ ( a i^i b ) ) e. M ) )
88	66, 84, 87	sylanbrc 698	. . . . 5 |- ( ( ph /\ ( a e. J /\ b e. J ) ) -> ( a i^i b ) e. J )
89	88	ralrimivva 2971	. . . 4 |- ( ph -> A. a e. J A. b e. J ( a i^i b ) e. J )
90		pwexg 4850	. . . . . . 7 |- ( B e. M -> ~P B e. _V )
91	44, 90	syl 17	. . . . . 6 |- ( ph -> ~P B e. _V )
92	5, 91	rabexd 4814	. . . . 5 |- ( ph -> J e. _V )
93		istopg 20700	. . . . 5 |- ( J e. _V -> ( J e. Top <-> ( A. a ( a C_ J -> U. a e. J ) /\ A. a e. J A. b e. J ( a i^i b ) e. J ) ) )
94	92, 93	syl 17	. . . 4 |- ( ph -> ( J e. Top <-> ( A. a ( a C_ J -> U. a e. J ) /\ A. a e. J A. b e. J ( a i^i b ) e. J ) ) )
95	54, 89, 94	mpbir2and 957	. . 3 |- ( ph -> J e. Top )
96	7	unissi 4461	. . . . . 6 |- U. J C_ U. ~P B
97		unipw 4918	. . . . . 6 |- U. ~P B = B
98	96, 97	sseqtri 3637	. . . . 5 |- U. J C_ B
99		pwidg 4173	. . . . . . 7 |- ( B e. M -> B e. ~P B )
100	44, 99	syl 17	. . . . . 6 |- ( ph -> B e. ~P B )
101		difid 3948	. . . . . . 7 |- ( B \ B ) = (/)
102		mretopd.z	. . . . . . 7 |- ( ph -> (/) e. M )
103	101, 102	syl5eqel 2705	. . . . . 6 |- ( ph -> ( B \ B ) e. M )
104		difeq2 3722	. . . . . . . 8 |- ( z = B -> ( B \ z ) = ( B \ B ) )
105	104	eleq1d 2686	. . . . . . 7 |- ( z = B -> ( ( B \ z ) e. M <-> ( B \ B ) e. M ) )
106	105, 5	elrab2 3366	. . . . . 6 |- ( B e. J <-> ( B e. ~P B /\ ( B \ B ) e. M ) )
107	100, 103, 106	sylanbrc 698	. . . . 5 |- ( ph -> B e. J )
108		unissel 4468	. . . . 5 |- ( ( U. J C_ B /\ B e. J ) -> U. J = B )
109	98, 107, 108	sylancr 695	. . . 4 |- ( ph -> U. J = B )
110	109	eqcomd 2628	. . 3 |- ( ph -> B = U. J )
111		istopon 20717	. . 3 |- ( J e. (TopOn ` B ) <-> ( J e. Top /\ B = U. J ) )
112	95, 110, 111	sylanbrc 698	. 2 |- ( ph -> J e. (TopOn ` B ) )
113		eqid 2622	. . . . 5 |- U. J = U. J
114	113	cldval 20827	. . . 4 |- ( J e. Top -> ( Clsd ` J ) = { x e. ~P U. J | ( U. J \ x ) e. J } )
115	95, 114	syl 17	. . 3 |- ( ph -> ( Clsd ` J ) = { x e. ~P U. J | ( U. J \ x ) e. J } )
116	109	pweqd 4163	. . . 4 |- ( ph -> ~P U. J = ~P B )
117	109	difeq1d 3727	. . . . 5 |- ( ph -> ( U. J \ x ) = ( B \ x ) )
118	117	eleq1d 2686	. . . 4 |- ( ph -> ( ( U. J \ x ) e. J <-> ( B \ x ) e. J ) )
119	116, 118	rabeqbidv 3195	. . 3 |- ( ph -> { x e. ~P U. J | ( U. J \ x ) e. J } = { x e. ~P B | ( B \ x ) e. J } )
120	5	eleq2i 2693	. . . . . . 7 |- ( ( B \ x ) e. J <-> ( B \ x ) e. { z e. ~P B | ( B \ z ) e. M } )
121		difss 3737	. . . . . . . . . 10 |- ( B \ x ) C_ B
122		elpw2g 4827	. . . . . . . . . . 11 |- ( B e. M -> ( ( B \ x ) e. ~P B <-> ( B \ x ) C_ B ) )
123	44, 122	syl 17	. . . . . . . . . 10 |- ( ph -> ( ( B \ x ) e. ~P B <-> ( B \ x ) C_ B ) )
124	121, 123	mpbiri 248	. . . . . . . . 9 |- ( ph -> ( B \ x ) e. ~P B )
125		difeq2 3722	. . . . . . . . . . 11 |- ( z = ( B \ x ) -> ( B \ z ) = ( B \ ( B \ x ) ) )
126	125	eleq1d 2686	. . . . . . . . . 10 |- ( z = ( B \ x ) -> ( ( B \ z ) e. M <-> ( B \ ( B \ x ) ) e. M ) )
127	126	elrab3 3364	. . . . . . . . 9 |- ( ( B \ x ) e. ~P B -> ( ( B \ x ) e. { z e. ~P B | ( B \ z ) e. M } <-> ( B \ ( B \ x ) ) e. M ) )
128	124, 127	syl 17	. . . . . . . 8 |- ( ph -> ( ( B \ x ) e. { z e. ~P B | ( B \ z ) e. M } <-> ( B \ ( B \ x ) ) e. M ) )
129	128	adantr 481	. . . . . . 7 |- ( ( ph /\ x e. ~P B ) -> ( ( B \ x ) e. { z e. ~P B | ( B \ z ) e. M } <-> ( B \ ( B \ x ) ) e. M ) )
130	120, 129	syl5bb 272	. . . . . 6 |- ( ( ph /\ x e. ~P B ) -> ( ( B \ x ) e. J <-> ( B \ ( B \ x ) ) e. M ) )
131		elpwi 4168	. . . . . . . . 9 |- ( x e. ~P B -> x C_ B )
132		dfss4 3858	. . . . . . . . 9 |- ( x C_ B <-> ( B \ ( B \ x ) ) = x )
133	131, 132	sylib 208	. . . . . . . 8 |- ( x e. ~P B -> ( B \ ( B \ x ) ) = x )
134	133	adantl 482	. . . . . . 7 |- ( ( ph /\ x e. ~P B ) -> ( B \ ( B \ x ) ) = x )
135	134	eleq1d 2686	. . . . . 6 |- ( ( ph /\ x e. ~P B ) -> ( ( B \ ( B \ x ) ) e. M <-> x e. M ) )
136	130, 135	bitrd 268	. . . . 5 |- ( ( ph /\ x e. ~P B ) -> ( ( B \ x ) e. J <-> x e. M ) )
137	136	rabbidva 3188	. . . 4 |- ( ph -> { x e. ~P B | ( B \ x ) e. J } = { x e. ~P B | x e. M } )
138		incom 3805	. . . . . 6 |- ( M i^i ~P B ) = ( ~P B i^i M )
139		dfin5 3582	. . . . . 6 |- ( ~P B i^i M ) = { x e. ~P B | x e. M }
140	138, 139	eqtri 2644	. . . . 5 |- ( M i^i ~P B ) = { x e. ~P B | x e. M }
141		mresspw 16252	. . . . . . 7 |- ( M e. (Moore ` B ) -> M C_ ~P B )
142	21, 141	syl 17	. . . . . 6 |- ( ph -> M C_ ~P B )
143		df-ss 3588	. . . . . 6 |- ( M C_ ~P B <-> ( M i^i ~P B ) = M )
144	142, 143	sylib 208	. . . . 5 |- ( ph -> ( M i^i ~P B ) = M )
145	140, 144	syl5eqr 2670	. . . 4 |- ( ph -> { x e. ~P B | x e. M } = M )
146	137, 145	eqtrd 2656	. . 3 |- ( ph -> { x e. ~P B | ( B \ x ) e. J } = M )
147	115, 119, 146	3eqtrrd 2661	. 2 |- ( ph -> M = ( Clsd ` J ) )
148	112, 147	jca 554	1 |- ( ph -> ( J e. (TopOn ` B ) /\ M = ( Clsd ` J ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   A.wal 1481   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   {crab 2916   _Vcvv 3200   \ cdif 3571   u. cun 3572   i^i cin 3573   C_ wss 3574   (/)c0 3915   ~Pcpw 4158   U.cuni 4436   U_ciun 4520   |^|_ciin 4521   ` cfv 5888  Moorecmre 16242   Topctop 20698  TopOnctopon 20715   Clsdccld 20820

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-iota 5851  df-fun 5890  df-fv 5896  df-mre 16246  df-top 20699  df-topon 20716  df-cld 20823

This theorem is referenced by:  iscldtop  20899  istopclsd  37263