Theorem toponmre 20186

Description: The topologies over a given base set form a Moore collection: the intersection of any family of them is a topology, including the empty (relative) intersection which gives the discrete topology distop 20088. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Revised by Mario Carneiro, 5-May-2015.)

Assertion

Ref	Expression
toponmre	|- ( B e. V -> (TopOn ` B ) e. (Moore ` ~P B ) )

Proof of Theorem toponmre

Dummy variables b c x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		toponuni 20019	. . . . . 6 |- ( b e. (TopOn ` B ) -> B = U. b )
2		eqimss2 3471	. . . . . . 7 |- ( B = U. b -> U. b C_ B )
3		sspwuni 4360	. . . . . . 7 |- ( b C_ ~P B <-> U. b C_ B )
4	2, 3	sylibr 217	. . . . . 6 |- ( B = U. b -> b C_ ~P B )
5	1, 4	syl 17	. . . . 5 |- ( b e. (TopOn ` B ) -> b C_ ~P B )
6		selpw 3949	. . . . 5 |- ( b e. ~P ~P B <-> b C_ ~P B )
7	5, 6	sylibr 217	. . . 4 |- ( b e. (TopOn ` B ) -> b e. ~P ~P B )
8	7	ssriv 3422	. . 3 |- (TopOn ` B ) C_ ~P ~P B
9	8	a1i 11	. 2 |- ( B e. V -> (TopOn ` B ) C_ ~P ~P B )
10		distopon 20089	. 2 |- ( B e. V -> ~P B e. (TopOn ` B ) )
11		simpl 464	. . . . . . . . . . . . . 14 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> b C_ (TopOn ` B ) )
12	11	sselda 3418	. . . . . . . . . . . . 13 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ x e. b ) -> x e. (TopOn ` B ) )
13	12	adantrl 730	. . . . . . . . . . . 12 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c C_ |^| b /\ x e. b ) ) -> x e. (TopOn ` B ) )
14		topontop 20018	. . . . . . . . . . . 12 |- ( x e. (TopOn ` B ) -> x e. Top )
15	13, 14	syl 17	. . . . . . . . . . 11 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c C_ |^| b /\ x e. b ) ) -> x e. Top )
16		simpl 464	. . . . . . . . . . . . 13 |- ( ( c C_ |^| b /\ x e. b ) -> c C_ |^| b )
17		intss1 4241	. . . . . . . . . . . . . 14 |- ( x e. b -> |^| b C_ x )
18	17	adantl 473	. . . . . . . . . . . . 13 |- ( ( c C_ |^| b /\ x e. b ) -> |^| b C_ x )
19	16, 18	sstrd 3428	. . . . . . . . . . . 12 |- ( ( c C_ |^| b /\ x e. b ) -> c C_ x )
20	19	adantl 473	. . . . . . . . . . 11 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c C_ |^| b /\ x e. b ) ) -> c C_ x )
21		uniopn 20004	. . . . . . . . . . 11 |- ( ( x e. Top /\ c C_ x ) -> U. c e. x )
22	15, 20, 21	syl2anc 673	. . . . . . . . . 10 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c C_ |^| b /\ x e. b ) ) -> U. c e. x )
23	22	expr 626	. . . . . . . . 9 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c C_ |^| b ) -> ( x e. b -> U. c e. x ) )
24	23	ralrimiv 2808	. . . . . . . 8 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c C_ |^| b ) -> A. x e. b U. c e. x )
25		vex 3034	. . . . . . . . . 10 |- c e. _V
26	25	uniex 6606	. . . . . . . . 9 |- U. c e. _V
27	26	elint2 4233	. . . . . . . 8 |- ( U. c e. |^| b <-> A. x e. b U. c e. x )
28	24, 27	sylibr 217	. . . . . . 7 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c C_ |^| b ) -> U. c e. |^| b )
29	28	ex 441	. . . . . 6 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> ( c C_ |^| b -> U. c e. |^| b ) )
30	29	alrimiv 1781	. . . . 5 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> A. c ( c C_ |^| b -> U. c e. |^| b ) )
31		simpll 768	. . . . . . . . . . 11 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) -> b C_ (TopOn ` B ) )
32	31	sselda 3418	. . . . . . . . . 10 |- ( ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> y e. (TopOn ` B ) )
33		topontop 20018	. . . . . . . . . 10 |- ( y e. (TopOn ` B ) -> y e. Top )
34	32, 33	syl 17	. . . . . . . . 9 |- ( ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> y e. Top )
35		intss1 4241	. . . . . . . . . . 11 |- ( y e. b -> |^| b C_ y )
36	35	adantl 473	. . . . . . . . . 10 |- ( ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> |^| b C_ y )
37		simplrl 778	. . . . . . . . . 10 |- ( ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> c e. |^| b )
38	36, 37	sseldd 3419	. . . . . . . . 9 |- ( ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> c e. y )
39		simplrr 779	. . . . . . . . . 10 |- ( ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> x e. |^| b )
40	36, 39	sseldd 3419	. . . . . . . . 9 |- ( ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> x e. y )
41		inopn 20006	. . . . . . . . 9 |- ( ( y e. Top /\ c e. y /\ x e. y ) -> ( c i^i x ) e. y )
42	34, 38, 40, 41	syl3anc 1292	. . . . . . . 8 |- ( ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> ( c i^i x ) e. y )
43	42	ralrimiva 2809	. . . . . . 7 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) -> A. y e. b ( c i^i x ) e. y )
44	25	inex1 4537	. . . . . . . 8 |- ( c i^i x ) e. _V
45	44	elint2 4233	. . . . . . 7 |- ( ( c i^i x ) e. |^| b <-> A. y e. b ( c i^i x ) e. y )
46	43, 45	sylibr 217	. . . . . 6 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) -> ( c i^i x ) e. |^| b )
47	46	ralrimivva 2814	. . . . 5 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> A. c e. |^| b A. x e. |^| b ( c i^i x ) e. |^| b )
48		intex 4557	. . . . . . . 8 |- ( b =/= (/) <-> |^| b e. _V )
49	48	biimpi 199	. . . . . . 7 |- ( b =/= (/) -> |^| b e. _V )
50	49	adantl 473	. . . . . 6 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> |^| b e. _V )
51		istopg 20002	. . . . . 6 |- ( |^| b e. _V -> ( |^| b e. Top <-> ( A. c ( c C_ |^| b -> U. c e. |^| b ) /\ A. c e. |^| b A. x e. |^| b ( c i^i x ) e. |^| b ) ) )
52	50, 51	syl 17	. . . . 5 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> ( |^| b e. Top <-> ( A. c ( c C_ |^| b -> U. c e. |^| b ) /\ A. c e. |^| b A. x e. |^| b ( c i^i x ) e. |^| b ) ) )
53	30, 47, 52	mpbir2and 936	. . . 4 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> |^| b e. Top )
54	53	3adant1 1048	. . 3 |- ( ( B e. V /\ b C_ (TopOn ` B ) /\ b =/= (/) ) -> |^| b e. Top )
55		n0 3732	. . . . . . . . . . 11 |- ( b =/= (/) <-> E. x x e. b )
56	55	biimpi 199	. . . . . . . . . 10 |- ( b =/= (/) -> E. x x e. b )
57	56	ad2antlr 741	. . . . . . . . 9 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c e. |^| b ) -> E. x x e. b )
58	17	sselda 3418	. . . . . . . . . . . . . . 15 |- ( ( x e. b /\ c e. |^| b ) -> c e. x )
59	58	ancoms 460	. . . . . . . . . . . . . 14 |- ( ( c e. |^| b /\ x e. b ) -> c e. x )
60		elssuni 4219	. . . . . . . . . . . . . 14 |- ( c e. x -> c C_ U. x )
61	59, 60	syl 17	. . . . . . . . . . . . 13 |- ( ( c e. |^| b /\ x e. b ) -> c C_ U. x )
62	61	adantl 473	. . . . . . . . . . . 12 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. b ) ) -> c C_ U. x )
63	12	adantrl 730	. . . . . . . . . . . . 13 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. b ) ) -> x e. (TopOn ` B ) )
64		toponuni 20019	. . . . . . . . . . . . 13 |- ( x e. (TopOn ` B ) -> B = U. x )
65	63, 64	syl 17	. . . . . . . . . . . 12 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. b ) ) -> B = U. x )
66	62, 65	sseqtr4d 3455	. . . . . . . . . . 11 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. b ) ) -> c C_ B )
67	66	expr 626	. . . . . . . . . 10 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c e. |^| b ) -> ( x e. b -> c C_ B ) )
68	67	exlimdv 1787	. . . . . . . . 9 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c e. |^| b ) -> ( E. x x e. b -> c C_ B ) )
69	57, 68	mpd 15	. . . . . . . 8 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c e. |^| b ) -> c C_ B )
70	69	ralrimiva 2809	. . . . . . 7 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> A. c e. |^| b c C_ B )
71		unissb 4221	. . . . . . 7 |- ( U. |^| b C_ B <-> A. c e. |^| b c C_ B )
72	70, 71	sylibr 217	. . . . . 6 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> U. |^| b C_ B )
73	72	3adant1 1048	. . . . 5 |- ( ( B e. V /\ b C_ (TopOn ` B ) /\ b =/= (/) ) -> U. |^| b C_ B )
74	11	sselda 3418	. . . . . . . . . 10 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c e. b ) -> c e. (TopOn ` B ) )
75		toponuni 20019	. . . . . . . . . 10 |- ( c e. (TopOn ` B ) -> B = U. c )
76	74, 75	syl 17	. . . . . . . . 9 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c e. b ) -> B = U. c )
77		topontop 20018	. . . . . . . . . 10 |- ( c e. (TopOn ` B ) -> c e. Top )
78		eqid 2471	. . . . . . . . . . 11 |- U. c = U. c
79	78	topopn 20013	. . . . . . . . . 10 |- ( c e. Top -> U. c e. c )
80	74, 77, 79	3syl 18	. . . . . . . . 9 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c e. b ) -> U. c e. c )
81	76, 80	eqeltrd 2549	. . . . . . . 8 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c e. b ) -> B e. c )
82	81	ralrimiva 2809	. . . . . . 7 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> A. c e. b B e. c )
83	82	3adant1 1048	. . . . . 6 |- ( ( B e. V /\ b C_ (TopOn ` B ) /\ b =/= (/) ) -> A. c e. b B e. c )
84		elintg 4234	. . . . . . 7 |- ( B e. V -> ( B e. |^| b <-> A. c e. b B e. c ) )
85	84	3ad2ant1 1051	. . . . . 6 |- ( ( B e. V /\ b C_ (TopOn ` B ) /\ b =/= (/) ) -> ( B e. |^| b <-> A. c e. b B e. c ) )
86	83, 85	mpbird 240	. . . . 5 |- ( ( B e. V /\ b C_ (TopOn ` B ) /\ b =/= (/) ) -> B e. |^| b )
87		unissel 4220	. . . . 5 |- ( ( U. |^| b C_ B /\ B e. |^| b ) -> U. |^| b = B )
88	73, 86, 87	syl2anc 673	. . . 4 |- ( ( B e. V /\ b C_ (TopOn ` B ) /\ b =/= (/) ) -> U. |^| b = B )
89	88	eqcomd 2477	. . 3 |- ( ( B e. V /\ b C_ (TopOn ` B ) /\ b =/= (/) ) -> B = U. |^| b )
90		istopon 20017	. . 3 |- ( |^| b e. (TopOn ` B ) <-> ( |^| b e. Top /\ B = U. |^| b ) )
91	54, 89, 90	sylanbrc 677	. 2 |- ( ( B e. V /\ b C_ (TopOn ` B ) /\ b =/= (/) ) -> |^| b e. (TopOn ` B ) )
92	9, 10, 91	ismred 15586	1 |- ( B e. V -> (TopOn ` B ) e. (Moore ` ~P B ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 376   /\ w3a 1007   A.wal 1450   = wceq 1452   E.wex 1671   e. wcel 1904   =/= wne 2641   A.wral 2756   _Vcvv 3031   i^i cin 3389   C_ wss 3390   (/)c0 3722   ~Pcpw 3942   U.cuni 4190   |^|cint 4226   ` cfv 5589  Moorecmre 15566   Topctop 19994  TopOnctopon 19995

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-sbc 3256  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-int 4227  df-br 4396  df-opab 4455  df-mpt 4456  df-id 4754  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-iota 5553  df-fun 5591  df-fv 5597  df-mre 15570  df-top 19998  df-topon 20000

This theorem is referenced by:  topmtcl  31090