Theorem mretopd 18708

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 4111	. . . . . . . . 9 |- ( a = (/) -> U. a = U. (/) )
2		uni0 4130	. . . . . . . . 9 |- U. (/) = (/)
3	1, 2	syl6eq 2491	. . . . . . . 8 |- ( a = (/) -> U. a = (/) )
4	3	eleq1d 2509	. . . . . . 7 |- ( a = (/) -> ( U. a e. J <-> (/) e. J ) )
5		mretopd.j	. . . . . . . . . . . . . 14 |- J = { z e. ~P B | ( B \ z ) e. M }
6		ssrab2 3449	. . . . . . . . . . . . . 14 |- { z e. ~P B | ( B \ z ) e. M } C_ ~P B
7	5, 6	eqsstri 3398	. . . . . . . . . . . . 13 |- J C_ ~P B
8		sstr 3376	. . . . . . . . . . . . 13 |- ( ( a C_ J /\ J C_ ~P B ) -> a C_ ~P B )
9	7, 8	mpan2 671	. . . . . . . . . . . 12 |- ( a C_ J -> a C_ ~P B )
10	9	adantl 466	. . . . . . . . . . 11 |- ( ( ph /\ a C_ J ) -> a C_ ~P B )
11		sspwuni 4268	. . . . . . . . . . 11 |- ( a C_ ~P B <-> U. a C_ B )
12	10, 11	sylib 196	. . . . . . . . . 10 |- ( ( ph /\ a C_ J ) -> U. a C_ B )
13		vex 2987	. . . . . . . . . . . 12 |- a e. _V
14	13	uniex 6388	. . . . . . . . . . 11 |- U. a e. _V
15	14	elpw 3878	. . . . . . . . . 10 |- ( U. a e. ~P B <-> U. a C_ B )
16	12, 15	sylibr 212	. . . . . . . . 9 |- ( ( ph /\ a C_ J ) -> U. a e. ~P B )
17	16	adantr 465	. . . . . . . 8 |- ( ( ( ph /\ a C_ J ) /\ a =/= (/) ) -> U. a e. ~P B )
18		uniiun 4235	. . . . . . . . . 10 |- U. a = U_ b e. a b
19	18	difeq2i 3483	. . . . . . . . 9 |- ( B \ U. a ) = ( B \ U_ b e. a b )
20		iindif2 4251	. . . . . . . . . . 11 |- ( a =/= (/) -> |^|_ b e. a ( B \ b ) = ( B \ U_ b e. a b ) )
21	20	adantl 466	. . . . . . . . . 10 |- ( ( ( ph /\ a C_ J ) /\ a =/= (/) ) -> |^|_ b e. a ( B \ b ) = ( B \ U_ b e. a b ) )
22		mretopd.m	. . . . . . . . . . . 12 |- ( ph -> M e. (Moore ` B ) )
23	22	ad2antrr 725	. . . . . . . . . . 11 |- ( ( ( ph /\ a C_ J ) /\ a =/= (/) ) -> M e. (Moore ` B ) )
24		simpr 461	. . . . . . . . . . 11 |- ( ( ( ph /\ a C_ J ) /\ a =/= (/) ) -> a =/= (/) )
25		difeq2 3480	. . . . . . . . . . . . . . . . 17 |- ( z = b -> ( B \ z ) = ( B \ b ) )
26	25	eleq1d 2509	. . . . . . . . . . . . . . . 16 |- ( z = b -> ( ( B \ z ) e. M <-> ( B \ b ) e. M ) )
27	26, 5	elrab2 3131	. . . . . . . . . . . . . . 15 |- ( b e. J <-> ( b e. ~P B /\ ( B \ b ) e. M ) )
28	27	simprbi 464	. . . . . . . . . . . . . 14 |- ( b e. J -> ( B \ b ) e. M )
29	28	rgen 2793	. . . . . . . . . . . . 13 |- A. b e. J ( B \ b ) e. M
30		ssralv 3428	. . . . . . . . . . . . . 14 |- ( a C_ J -> ( A. b e. J ( B \ b ) e. M -> A. b e. a ( B \ b ) e. M ) )
31	30	adantl 466	. . . . . . . . . . . . 13 |- ( ( ph /\ a C_ J ) -> ( A. b e. J ( B \ b ) e. M -> A. b e. a ( B \ b ) e. M ) )
32	29, 31	mpi 17	. . . . . . . . . . . 12 |- ( ( ph /\ a C_ J ) -> A. b e. a ( B \ b ) e. M )
33	32	adantr 465	. . . . . . . . . . 11 |- ( ( ( ph /\ a C_ J ) /\ a =/= (/) ) -> A. b e. a ( B \ b ) e. M )
34		mreiincl 14546	. . . . . . . . . . 11 |- ( ( M e. (Moore ` B ) /\ a =/= (/) /\ A. b e. a ( B \ b ) e. M ) -> |^|_ b e. a ( B \ b ) e. M )
35	23, 24, 33, 34	syl3anc 1218	. . . . . . . . . 10 |- ( ( ( ph /\ a C_ J ) /\ a =/= (/) ) -> |^|_ b e. a ( B \ b ) e. M )
36	21, 35	eqeltrrd 2518	. . . . . . . . 9 |- ( ( ( ph /\ a C_ J ) /\ a =/= (/) ) -> ( B \ U_ b e. a b ) e. M )
37	19, 36	syl5eqel 2527	. . . . . . . 8 |- ( ( ( ph /\ a C_ J ) /\ a =/= (/) ) -> ( B \ U. a ) e. M )
38		difeq2 3480	. . . . . . . . . 10 |- ( z = U. a -> ( B \ z ) = ( B \ U. a ) )
39	38	eleq1d 2509	. . . . . . . . 9 |- ( z = U. a -> ( ( B \ z ) e. M <-> ( B \ U. a ) e. M ) )
40	39, 5	elrab2 3131	. . . . . . . 8 |- ( U. a e. J <-> ( U. a e. ~P B /\ ( B \ U. a ) e. M ) )
41	17, 37, 40	sylanbrc 664	. . . . . . 7 |- ( ( ( ph /\ a C_ J ) /\ a =/= (/) ) -> U. a e. J )
42		0elpw 4473	. . . . . . . . . 10 |- (/) e. ~P B
43	42	a1i 11	. . . . . . . . 9 |- ( ph -> (/) e. ~P B )
44		mre1cl 14544	. . . . . . . . . 10 |- ( M e. (Moore ` B ) -> B e. M )
45	22, 44	syl 16	. . . . . . . . 9 |- ( ph -> B e. M )
46		difeq2 3480	. . . . . . . . . . . 12 |- ( z = (/) -> ( B \ z ) = ( B \ (/) ) )
47		dif0 3761	. . . . . . . . . . . 12 |- ( B \ (/) ) = B
48	46, 47	syl6eq 2491	. . . . . . . . . . 11 |- ( z = (/) -> ( B \ z ) = B )
49	48	eleq1d 2509	. . . . . . . . . 10 |- ( z = (/) -> ( ( B \ z ) e. M <-> B e. M ) )
50	49, 5	elrab2 3131	. . . . . . . . 9 |- ( (/) e. J <-> ( (/) e. ~P B /\ B e. M ) )
51	43, 45, 50	sylanbrc 664	. . . . . . . 8 |- ( ph -> (/) e. J )
52	51	adantr 465	. . . . . . 7 |- ( ( ph /\ a C_ J ) -> (/) e. J )
53	4, 41, 52	pm2.61ne 2698	. . . . . 6 |- ( ( ph /\ a C_ J ) -> U. a e. J )
54	53	ex 434	. . . . 5 |- ( ph -> ( a C_ J -> U. a e. J ) )
55	54	alrimiv 1685	. . . 4 |- ( ph -> A. a ( a C_ J -> U. a e. J ) )
56		inss1 3582	. . . . . . . 8 |- ( a i^i b ) C_ a
57		difeq2 3480	. . . . . . . . . . . . 13 |- ( z = a -> ( B \ z ) = ( B \ a ) )
58	57	eleq1d 2509	. . . . . . . . . . . 12 |- ( z = a -> ( ( B \ z ) e. M <-> ( B \ a ) e. M ) )
59	58, 5	elrab2 3131	. . . . . . . . . . 11 |- ( a e. J <-> ( a e. ~P B /\ ( B \ a ) e. M ) )
60	59	simplbi 460	. . . . . . . . . 10 |- ( a e. J -> a e. ~P B )
61	60	elpwid 3882	. . . . . . . . 9 |- ( a e. J -> a C_ B )
62	61	ad2antrl 727	. . . . . . . 8 |- ( ( ph /\ ( a e. J /\ b e. J ) ) -> a C_ B )
63	56, 62	syl5ss 3379	. . . . . . 7 |- ( ( ph /\ ( a e. J /\ b e. J ) ) -> ( a i^i b ) C_ B )
64	13	inex1 4445	. . . . . . . 8 |- ( a i^i b ) e. _V
65	64	elpw 3878	. . . . . . 7 |- ( ( a i^i b ) e. ~P B <-> ( a i^i b ) C_ B )
66	63, 65	sylibr 212	. . . . . 6 |- ( ( ph /\ ( a e. J /\ b e. J ) ) -> ( a i^i b ) e. ~P B )
67		difindi 3616	. . . . . . 7 |- ( B \ ( a i^i b ) ) = ( ( B \ a ) u. ( B \ b ) )
68	59	simprbi 464	. . . . . . . . 9 |- ( a e. J -> ( B \ a ) e. M )
69	68	ad2antrl 727	. . . . . . . 8 |- ( ( ph /\ ( a e. J /\ b e. J ) ) -> ( B \ a ) e. M )
70	28	ad2antll 728	. . . . . . . 8 |- ( ( ph /\ ( a e. J /\ b e. J ) ) -> ( B \ b ) e. M )
71		simpl 457	. . . . . . . 8 |- ( ( ph /\ ( a e. J /\ b e. J ) ) -> ph )
72		uneq1 3515	. . . . . . . . . . . 12 |- ( x = ( B \ a ) -> ( x u. y ) = ( ( B \ a ) u. y ) )
73	72	eleq1d 2509	. . . . . . . . . . 11 |- ( x = ( B \ a ) -> ( ( x u. y ) e. M <-> ( ( B \ a ) u. y ) e. M ) )
74	73	imbi2d 316	. . . . . . . . . 10 |- ( x = ( B \ a ) -> ( ( ph -> ( x u. y ) e. M ) <-> ( ph -> ( ( B \ a ) u. y ) e. M ) ) )
75		uneq2 3516	. . . . . . . . . . . 12 |- ( y = ( B \ b ) -> ( ( B \ a ) u. y ) = ( ( B \ a ) u. ( B \ b ) ) )
76	75	eleq1d 2509	. . . . . . . . . . 11 |- ( y = ( B \ b ) -> ( ( ( B \ a ) u. y ) e. M <-> ( ( B \ a ) u. ( B \ b ) ) e. M ) )
77	76	imbi2d 316	. . . . . . . . . 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 1188	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. M /\ y e. M ) ) -> ( x u. y ) e. M )
80	79	expcom 435	. . . . . . . . . 10 |- ( ( x e. M /\ y e. M ) -> ( ph -> ( x u. y ) e. M ) )
81	74, 77, 80	vtocl2ga 3050	. . . . . . . . 9 |- ( ( ( B \ a ) e. M /\ ( B \ b ) e. M ) -> ( ph -> ( ( B \ a ) u. ( B \ b ) ) e. M ) )
82	81	imp 429	. . . . . . . 8 |- ( ( ( ( B \ a ) e. M /\ ( B \ b ) e. M ) /\ ph ) -> ( ( B \ a ) u. ( B \ b ) ) e. M )
83	69, 70, 71, 82	syl21anc 1217	. . . . . . 7 |- ( ( ph /\ ( a e. J /\ b e. J ) ) -> ( ( B \ a ) u. ( B \ b ) ) e. M )
84	67, 83	syl5eqel 2527	. . . . . 6 |- ( ( ph /\ ( a e. J /\ b e. J ) ) -> ( B \ ( a i^i b ) ) e. M )
85		difeq2 3480	. . . . . . . 8 |- ( z = ( a i^i b ) -> ( B \ z ) = ( B \ ( a i^i b ) ) )
86	85	eleq1d 2509	. . . . . . 7 |- ( z = ( a i^i b ) -> ( ( B \ z ) e. M <-> ( B \ ( a i^i b ) ) e. M ) )
87	86, 5	elrab2 3131	. . . . . 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 664	. . . . 5 |- ( ( ph /\ ( a e. J /\ b e. J ) ) -> ( a i^i b ) e. J )
89	88	ralrimivva 2820	. . . 4 |- ( ph -> A. a e. J A. b e. J ( a i^i b ) e. J )
90		pwexg 4488	. . . . . . . 8 |- ( B e. M -> ~P B e. _V )
91	45, 90	syl 16	. . . . . . 7 |- ( ph -> ~P B e. _V )
92		rabexg 4454	. . . . . . 7 |- ( ~P B e. _V -> { z e. ~P B | ( B \ z ) e. M } e. _V )
93	91, 92	syl 16	. . . . . 6 |- ( ph -> { z e. ~P B | ( B \ z ) e. M } e. _V )
94	5, 93	syl5eqel 2527	. . . . 5 |- ( ph -> J e. _V )
95		istopg 18520	. . . . 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 ) ) )
96	94, 95	syl 16	. . . 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 ) ) )
97	55, 89, 96	mpbir2and 913	. . 3 |- ( ph -> J e. Top )
98	7	unissi 4126	. . . . . 6 |- U. J C_ U. ~P B
99		unipw 4554	. . . . . 6 |- U. ~P B = B
100	98, 99	sseqtri 3400	. . . . 5 |- U. J C_ B
101		pwidg 3885	. . . . . . 7 |- ( B e. M -> B e. ~P B )
102	45, 101	syl 16	. . . . . 6 |- ( ph -> B e. ~P B )
103		difid 3759	. . . . . . 7 |- ( B \ B ) = (/)
104		mretopd.z	. . . . . . 7 |- ( ph -> (/) e. M )
105	103, 104	syl5eqel 2527	. . . . . 6 |- ( ph -> ( B \ B ) e. M )
106		difeq2 3480	. . . . . . . 8 |- ( z = B -> ( B \ z ) = ( B \ B ) )
107	106	eleq1d 2509	. . . . . . 7 |- ( z = B -> ( ( B \ z ) e. M <-> ( B \ B ) e. M ) )
108	107, 5	elrab2 3131	. . . . . 6 |- ( B e. J <-> ( B e. ~P B /\ ( B \ B ) e. M ) )
109	102, 105, 108	sylanbrc 664	. . . . 5 |- ( ph -> B e. J )
110		unissel 4134	. . . . 5 |- ( ( U. J C_ B /\ B e. J ) -> U. J = B )
111	100, 109, 110	sylancr 663	. . . 4 |- ( ph -> U. J = B )
112	111	eqcomd 2448	. . 3 |- ( ph -> B = U. J )
113		istopon 18542	. . 3 |- ( J e. (TopOn ` B ) <-> ( J e. Top /\ B = U. J ) )
114	97, 112, 113	sylanbrc 664	. 2 |- ( ph -> J e. (TopOn ` B ) )
115		eqid 2443	. . . . 5 |- U. J = U. J
116	115	cldval 18639	. . . 4 |- ( J e. Top -> ( Clsd ` J ) = { x e. ~P U. J | ( U. J \ x ) e. J } )
117	97, 116	syl 16	. . 3 |- ( ph -> ( Clsd ` J ) = { x e. ~P U. J | ( U. J \ x ) e. J } )
118	111	pweqd 3877	. . . 4 |- ( ph -> ~P U. J = ~P B )
119	111	difeq1d 3485	. . . . 5 |- ( ph -> ( U. J \ x ) = ( B \ x ) )
120	119	eleq1d 2509	. . . 4 |- ( ph -> ( ( U. J \ x ) e. J <-> ( B \ x ) e. J ) )
121	118, 120	rabeqbidv 2979	. . 3 |- ( ph -> { x e. ~P U. J | ( U. J \ x ) e. J } = { x e. ~P B | ( B \ x ) e. J } )
122	5	eleq2i 2507	. . . . . . 7 |- ( ( B \ x ) e. J <-> ( B \ x ) e. { z e. ~P B | ( B \ z ) e. M } )
123		difss 3495	. . . . . . . . . 10 |- ( B \ x ) C_ B
124		elpw2g 4467	. . . . . . . . . . 11 |- ( B e. M -> ( ( B \ x ) e. ~P B <-> ( B \ x ) C_ B ) )
125	45, 124	syl 16	. . . . . . . . . 10 |- ( ph -> ( ( B \ x ) e. ~P B <-> ( B \ x ) C_ B ) )
126	123, 125	mpbiri 233	. . . . . . . . 9 |- ( ph -> ( B \ x ) e. ~P B )
127		difeq2 3480	. . . . . . . . . . 11 |- ( z = ( B \ x ) -> ( B \ z ) = ( B \ ( B \ x ) ) )
128	127	eleq1d 2509	. . . . . . . . . 10 |- ( z = ( B \ x ) -> ( ( B \ z ) e. M <-> ( B \ ( B \ x ) ) e. M ) )
129	128	elrab3 3130	. . . . . . . . 9 |- ( ( B \ x ) e. ~P B -> ( ( B \ x ) e. { z e. ~P B | ( B \ z ) e. M } <-> ( B \ ( B \ x ) ) e. M ) )
130	126, 129	syl 16	. . . . . . . 8 |- ( ph -> ( ( B \ x ) e. { z e. ~P B | ( B \ z ) e. M } <-> ( B \ ( B \ x ) ) e. M ) )
131	130	adantr 465	. . . . . . 7 |- ( ( ph /\ x e. ~P B ) -> ( ( B \ x ) e. { z e. ~P B | ( B \ z ) e. M } <-> ( B \ ( B \ x ) ) e. M ) )
132	122, 131	syl5bb 257	. . . . . 6 |- ( ( ph /\ x e. ~P B ) -> ( ( B \ x ) e. J <-> ( B \ ( B \ x ) ) e. M ) )
133		elpwi 3881	. . . . . . . . 9 |- ( x e. ~P B -> x C_ B )
134		dfss4 3596	. . . . . . . . 9 |- ( x C_ B <-> ( B \ ( B \ x ) ) = x )
135	133, 134	sylib 196	. . . . . . . 8 |- ( x e. ~P B -> ( B \ ( B \ x ) ) = x )
136	135	adantl 466	. . . . . . 7 |- ( ( ph /\ x e. ~P B ) -> ( B \ ( B \ x ) ) = x )
137	136	eleq1d 2509	. . . . . 6 |- ( ( ph /\ x e. ~P B ) -> ( ( B \ ( B \ x ) ) e. M <-> x e. M ) )
138	132, 137	bitrd 253	. . . . 5 |- ( ( ph /\ x e. ~P B ) -> ( ( B \ x ) e. J <-> x e. M ) )
139	138	rabbidva 2975	. . . 4 |- ( ph -> { x e. ~P B | ( B \ x ) e. J } = { x e. ~P B | x e. M } )
140		incom 3555	. . . . . 6 |- ( M i^i ~P B ) = ( ~P B i^i M )
141		dfin5 3348	. . . . . 6 |- ( ~P B i^i M ) = { x e. ~P B | x e. M }
142	140, 141	eqtri 2463	. . . . 5 |- ( M i^i ~P B ) = { x e. ~P B | x e. M }
143		mresspw 14542	. . . . . . 7 |- ( M e. (Moore ` B ) -> M C_ ~P B )
144	22, 143	syl 16	. . . . . 6 |- ( ph -> M C_ ~P B )
145		df-ss 3354	. . . . . 6 |- ( M C_ ~P B <-> ( M i^i ~P B ) = M )
146	144, 145	sylib 196	. . . . 5 |- ( ph -> ( M i^i ~P B ) = M )
147	142, 146	syl5eqr 2489	. . . 4 |- ( ph -> { x e. ~P B | x e. M } = M )
148	139, 147	eqtrd 2475	. . 3 |- ( ph -> { x e. ~P B | ( B \ x ) e. J } = M )
149	117, 121, 148	3eqtrrd 2480	. 2 |- ( ph -> M = ( Clsd ` J ) )
150	114, 149	jca 532	1 |- ( ph -> ( J e. (TopOn ` B ) /\ M = ( Clsd ` J ) ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 965   A.wal 1367   = wceq 1369   e. wcel 1756   =/= wne 2618   A.wral 2727   {crab 2731   _Vcvv 2984   \ cdif 3337   u. cun 3338   i^i cin 3339   C_ wss 3340   (/)c0 3649   ~Pcpw 3872   U.cuni 4103   U_ciun 4183   |^|_ciin 4184   ` cfv 5430  Moorecmre 14532   Topctop 18510  TopOnctopon 18511   Clsdccld 18632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4425  ax-nul 4433  ax-pow 4482  ax-pr 4543  ax-un 6384

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2620  df-ral 2732  df-rex 2733  df-rab 2736  df-v 2986  df-sbc 3199  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-nul 3650  df-if 3804  df-pw 3874  df-sn 3890  df-pr 3892  df-op 3896  df-uni 4104  df-int 4141  df-iun 4185  df-iin 4186  df-br 4305  df-opab 4363  df-mpt 4364  df-id 4648  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-iota 5393  df-fun 5432  df-fv 5438  df-mre 14536  df-top 18515  df-topon 18518  df-cld 18635

This theorem is referenced by:  iscldtop  18711  istopclsd  29048