Theorem toponmre 20093

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 19995. (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 19926	. . . . . 6 |- ( b e. (TopOn ` B ) -> B = U. b )
2		eqimss2 3517	. . . . . . 7 |- ( B = U. b -> U. b C_ B )
3		sspwuni 4385	. . . . . . 7 |- ( b C_ ~P B <-> U. b C_ B )
4	2, 3	sylibr 215	. . . . . 6 |- ( B = U. b -> b C_ ~P B )
5	1, 4	syl 17	. . . . 5 |- ( b e. (TopOn ` B ) -> b C_ ~P B )
6		selpw 3986	. . . . 5 |- ( b e. ~P ~P B <-> b C_ ~P B )
7	5, 6	sylibr 215	. . . 4 |- ( b e. (TopOn ` B ) -> b e. ~P ~P B )
8	7	ssriv 3468	. . 3 |- (TopOn ` B ) C_ ~P ~P B
9	8	a1i 11	. 2 |- ( B e. V -> (TopOn ` B ) C_ ~P ~P B )
10		distopon 19996	. 2 |- ( B e. V -> ~P B e. (TopOn ` B ) )
11		simpl 458	. . . . . . . . . . . . . 14 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> b C_ (TopOn ` B ) )
12	11	sselda 3464	. . . . . . . . . . . . 13 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ x e. b ) -> x e. (TopOn ` B ) )
13	12	adantrl 720	. . . . . . . . . . . 12 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c C_ |^| b /\ x e. b ) ) -> x e. (TopOn ` B ) )
14		topontop 19925	. . . . . . . . . . . 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 458	. . . . . . . . . . . . 13 |- ( ( c C_ |^| b /\ x e. b ) -> c C_ |^| b )
17		intss1 4267	. . . . . . . . . . . . . 14 |- ( x e. b -> |^| b C_ x )
18	17	adantl 467	. . . . . . . . . . . . 13 |- ( ( c C_ |^| b /\ x e. b ) -> |^| b C_ x )
19	16, 18	sstrd 3474	. . . . . . . . . . . 12 |- ( ( c C_ |^| b /\ x e. b ) -> c C_ x )
20	19	adantl 467	. . . . . . . . . . 11 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c C_ |^| b /\ x e. b ) ) -> c C_ x )
21		uniopn 19911	. . . . . . . . . . 11 |- ( ( x e. Top /\ c C_ x ) -> U. c e. x )
22	15, 20, 21	syl2anc 665	. . . . . . . . . 10 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c C_ |^| b /\ x e. b ) ) -> U. c e. x )
23	22	expr 618	. . . . . . . . 9 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c C_ |^| b ) -> ( x e. b -> U. c e. x ) )
24	23	ralrimiv 2837	. . . . . . . 8 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c C_ |^| b ) -> A. x e. b U. c e. x )
25		vex 3084	. . . . . . . . . 10 |- c e. _V
26	25	uniex 6597	. . . . . . . . 9 |- U. c e. _V
27	26	elint2 4259	. . . . . . . 8 |- ( U. c e. |^| b <-> A. x e. b U. c e. x )
28	24, 27	sylibr 215	. . . . . . 7 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c C_ |^| b ) -> U. c e. |^| b )
29	28	ex 435	. . . . . 6 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> ( c C_ |^| b -> U. c e. |^| b ) )
30	29	alrimiv 1763	. . . . 5 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> A. c ( c C_ |^| b -> U. c e. |^| b ) )
31		simpll 758	. . . . . . . . . . 11 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) -> b C_ (TopOn ` B ) )
32	31	sselda 3464	. . . . . . . . . 10 |- ( ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> y e. (TopOn ` B ) )
33		topontop 19925	. . . . . . . . . 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 4267	. . . . . . . . . . 11 |- ( y e. b -> |^| b C_ y )
36	35	adantl 467	. . . . . . . . . 10 |- ( ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> |^| b C_ y )
37		simplrl 768	. . . . . . . . . 10 |- ( ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> c e. |^| b )
38	36, 37	sseldd 3465	. . . . . . . . 9 |- ( ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> c e. y )
39		simplrr 769	. . . . . . . . . 10 |- ( ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> x e. |^| b )
40	36, 39	sseldd 3465	. . . . . . . . 9 |- ( ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> x e. y )
41		inopn 19913	. . . . . . . . 9 |- ( ( y e. Top /\ c e. y /\ x e. y ) -> ( c i^i x ) e. y )
42	34, 38, 40, 41	syl3anc 1264	. . . . . . . 8 |- ( ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> ( c i^i x ) e. y )
43	42	ralrimiva 2839	. . . . . . 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 4561	. . . . . . . 8 |- ( c i^i x ) e. _V
45	44	elint2 4259	. . . . . . 7 |- ( ( c i^i x ) e. |^| b <-> A. y e. b ( c i^i x ) e. y )
46	43, 45	sylibr 215	. . . . . 6 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) -> ( c i^i x ) e. |^| b )
47	46	ralrimivva 2846	. . . . 5 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> A. c e. |^| b A. x e. |^| b ( c i^i x ) e. |^| b )
48		intex 4576	. . . . . . . 8 |- ( b =/= (/) <-> |^| b e. _V )
49	48	biimpi 197	. . . . . . 7 |- ( b =/= (/) -> |^| b e. _V )
50	49	adantl 467	. . . . . 6 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> |^| b e. _V )
51		istopg 19909	. . . . . 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 930	. . . 4 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> |^| b e. Top )
54	53	3adant1 1023	. . 3 |- ( ( B e. V /\ b C_ (TopOn ` B ) /\ b =/= (/) ) -> |^| b e. Top )
55		n0 3771	. . . . . . . . . . 11 |- ( b =/= (/) <-> E. x x e. b )
56	55	biimpi 197	. . . . . . . . . 10 |- ( b =/= (/) -> E. x x e. b )
57	56	ad2antlr 731	. . . . . . . . 9 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c e. |^| b ) -> E. x x e. b )
58	17	sselda 3464	. . . . . . . . . . . . . . 15 |- ( ( x e. b /\ c e. |^| b ) -> c e. x )
59	58	ancoms 454	. . . . . . . . . . . . . 14 |- ( ( c e. |^| b /\ x e. b ) -> c e. x )
60		elssuni 4245	. . . . . . . . . . . . . 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 467	. . . . . . . . . . . 12 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. b ) ) -> c C_ U. x )
63	12	adantrl 720	. . . . . . . . . . . . 13 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. b ) ) -> x e. (TopOn ` B ) )
64		toponuni 19926	. . . . . . . . . . . . 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 3501	. . . . . . . . . . 11 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. b ) ) -> c C_ B )
67	66	expr 618	. . . . . . . . . 10 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c e. |^| b ) -> ( x e. b -> c C_ B ) )
68	67	exlimdv 1768	. . . . . . . . 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 2839	. . . . . . 7 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> A. c e. |^| b c C_ B )
71		unissb 4247	. . . . . . 7 |- ( U. |^| b C_ B <-> A. c e. |^| b c C_ B )
72	70, 71	sylibr 215	. . . . . 6 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> U. |^| b C_ B )
73	72	3adant1 1023	. . . . 5 |- ( ( B e. V /\ b C_ (TopOn ` B ) /\ b =/= (/) ) -> U. |^| b C_ B )
74	11	sselda 3464	. . . . . . . . . 10 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c e. b ) -> c e. (TopOn ` B ) )
75		toponuni 19926	. . . . . . . . . 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 19925	. . . . . . . . . 10 |- ( c e. (TopOn ` B ) -> c e. Top )
78		eqid 2422	. . . . . . . . . . 11 |- U. c = U. c
79	78	topopn 19920	. . . . . . . . . 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 2510	. . . . . . . 8 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c e. b ) -> B e. c )
82	81	ralrimiva 2839	. . . . . . 7 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> A. c e. b B e. c )
83	82	3adant1 1023	. . . . . 6 |- ( ( B e. V /\ b C_ (TopOn ` B ) /\ b =/= (/) ) -> A. c e. b B e. c )
84		elintg 4260	. . . . . . 7 |- ( B e. V -> ( B e. |^| b <-> A. c e. b B e. c ) )
85	84	3ad2ant1 1026	. . . . . 6 |- ( ( B e. V /\ b C_ (TopOn ` B ) /\ b =/= (/) ) -> ( B e. |^| b <-> A. c e. b B e. c ) )
86	83, 85	mpbird 235	. . . . 5 |- ( ( B e. V /\ b C_ (TopOn ` B ) /\ b =/= (/) ) -> B e. |^| b )
87		unissel 4246	. . . . 5 |- ( ( U. |^| b C_ B /\ B e. |^| b ) -> U. |^| b = B )
88	73, 86, 87	syl2anc 665	. . . 4 |- ( ( B e. V /\ b C_ (TopOn ` B ) /\ b =/= (/) ) -> U. |^| b = B )
89	88	eqcomd 2430	. . 3 |- ( ( B e. V /\ b C_ (TopOn ` B ) /\ b =/= (/) ) -> B = U. |^| b )
90		istopon 19924	. . 3 |- ( |^| b e. (TopOn ` B ) <-> ( |^| b e. Top /\ B = U. |^| b ) )
91	54, 89, 90	sylanbrc 668	. 2 |- ( ( B e. V /\ b C_ (TopOn ` B ) /\ b =/= (/) ) -> |^| b e. (TopOn ` B ) )
92	9, 10, 91	ismred 15493	1 |- ( B e. V -> (TopOn ` B ) e. (Moore ` ~P B ) )

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370   /\ w3a 982   A.wal 1435   = wceq 1437   E.wex 1659   e. wcel 1868   =/= wne 2618   A.wral 2775   _Vcvv 3081   i^i cin 3435   C_ wss 3436   (/)c0 3761   ~Pcpw 3979   U.cuni 4216   |^|cint 4252   ` cfv 5597  Moorecmre 15473   Topctop 19901  TopOnctopon 19902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-int 4253  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4764  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-iota 5561  df-fun 5599  df-fv 5605  df-mre 15477  df-top 19905  df-topon 19907

This theorem is referenced by:  topmtcl  31009