Theorem toponmre 20897

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 20799. (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 20719	. . . . . 6 |- ( b e. (TopOn ` B ) -> B = U. b )
2		eqimss2 3658	. . . . . . 7 |- ( B = U. b -> U. b C_ B )
3		sspwuni 4611	. . . . . . 7 |- ( b C_ ~P B <-> U. b C_ B )
4	2, 3	sylibr 224	. . . . . 6 |- ( B = U. b -> b C_ ~P B )
5	1, 4	syl 17	. . . . 5 |- ( b e. (TopOn ` B ) -> b C_ ~P B )
6		selpw 4165	. . . . 5 |- ( b e. ~P ~P B <-> b C_ ~P B )
7	5, 6	sylibr 224	. . . 4 |- ( b e. (TopOn ` B ) -> b e. ~P ~P B )
8	7	ssriv 3607	. . 3 |- (TopOn ` B ) C_ ~P ~P B
9	8	a1i 11	. 2 |- ( B e. V -> (TopOn ` B ) C_ ~P ~P B )
10		distopon 20801	. 2 |- ( B e. V -> ~P B e. (TopOn ` B ) )
11		simpl 473	. . . . . . . . . . . . . 14 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> b C_ (TopOn ` B ) )
12	11	sselda 3603	. . . . . . . . . . . . 13 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ x e. b ) -> x e. (TopOn ` B ) )
13	12	adantrl 752	. . . . . . . . . . . 12 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c C_ |^| b /\ x e. b ) ) -> x e. (TopOn ` B ) )
14		topontop 20718	. . . . . . . . . . . 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 473	. . . . . . . . . . . . 13 |- ( ( c C_ |^| b /\ x e. b ) -> c C_ |^| b )
17		intss1 4492	. . . . . . . . . . . . . 14 |- ( x e. b -> |^| b C_ x )
18	17	adantl 482	. . . . . . . . . . . . 13 |- ( ( c C_ |^| b /\ x e. b ) -> |^| b C_ x )
19	16, 18	sstrd 3613	. . . . . . . . . . . 12 |- ( ( c C_ |^| b /\ x e. b ) -> c C_ x )
20	19	adantl 482	. . . . . . . . . . 11 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c C_ |^| b /\ x e. b ) ) -> c C_ x )
21		uniopn 20702	. . . . . . . . . . 11 |- ( ( x e. Top /\ c C_ x ) -> U. c e. x )
22	15, 20, 21	syl2anc 693	. . . . . . . . . 10 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c C_ |^| b /\ x e. b ) ) -> U. c e. x )
23	22	expr 643	. . . . . . . . 9 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c C_ |^| b ) -> ( x e. b -> U. c e. x ) )
24	23	ralrimiv 2965	. . . . . . . 8 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c C_ |^| b ) -> A. x e. b U. c e. x )
25		vuniex 6954	. . . . . . . . 9 |- U. c e. _V
26	25	elint2 4482	. . . . . . . 8 |- ( U. c e. |^| b <-> A. x e. b U. c e. x )
27	24, 26	sylibr 224	. . . . . . 7 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c C_ |^| b ) -> U. c e. |^| b )
28	27	ex 450	. . . . . 6 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> ( c C_ |^| b -> U. c e. |^| b ) )
29	28	alrimiv 1855	. . . . 5 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> A. c ( c C_ |^| b -> U. c e. |^| b ) )
30		simpll 790	. . . . . . . . . . 11 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) -> b C_ (TopOn ` B ) )
31	30	sselda 3603	. . . . . . . . . 10 |- ( ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> y e. (TopOn ` B ) )
32		topontop 20718	. . . . . . . . . 10 |- ( y e. (TopOn ` B ) -> y e. Top )
33	31, 32	syl 17	. . . . . . . . 9 |- ( ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> y e. Top )
34		intss1 4492	. . . . . . . . . . 11 |- ( y e. b -> |^| b C_ y )
35	34	adantl 482	. . . . . . . . . 10 |- ( ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> |^| b C_ y )
36		simplrl 800	. . . . . . . . . 10 |- ( ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> c e. |^| b )
37	35, 36	sseldd 3604	. . . . . . . . 9 |- ( ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> c e. y )
38		simplrr 801	. . . . . . . . . 10 |- ( ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> x e. |^| b )
39	35, 38	sseldd 3604	. . . . . . . . 9 |- ( ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> x e. y )
40		inopn 20704	. . . . . . . . 9 |- ( ( y e. Top /\ c e. y /\ x e. y ) -> ( c i^i x ) e. y )
41	33, 37, 39, 40	syl3anc 1326	. . . . . . . 8 |- ( ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> ( c i^i x ) e. y )
42	41	ralrimiva 2966	. . . . . . 7 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) -> A. y e. b ( c i^i x ) e. y )
43		vex 3203	. . . . . . . . 9 |- c e. _V
44	43	inex1 4799	. . . . . . . 8 |- ( c i^i x ) e. _V
45	44	elint2 4482	. . . . . . 7 |- ( ( c i^i x ) e. |^| b <-> A. y e. b ( c i^i x ) e. y )
46	42, 45	sylibr 224	. . . . . 6 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) -> ( c i^i x ) e. |^| b )
47	46	ralrimivva 2971	. . . . 5 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> A. c e. |^| b A. x e. |^| b ( c i^i x ) e. |^| b )
48		intex 4820	. . . . . . . 8 |- ( b =/= (/) <-> |^| b e. _V )
49	48	biimpi 206	. . . . . . 7 |- ( b =/= (/) -> |^| b e. _V )
50	49	adantl 482	. . . . . 6 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> |^| b e. _V )
51		istopg 20700	. . . . . 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	29, 47, 52	mpbir2and 957	. . . 4 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> |^| b e. Top )
54	53	3adant1 1079	. . 3 |- ( ( B e. V /\ b C_ (TopOn ` B ) /\ b =/= (/) ) -> |^| b e. Top )
55		n0 3931	. . . . . . . . . . 11 |- ( b =/= (/) <-> E. x x e. b )
56	55	biimpi 206	. . . . . . . . . 10 |- ( b =/= (/) -> E. x x e. b )
57	56	ad2antlr 763	. . . . . . . . 9 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c e. |^| b ) -> E. x x e. b )
58	17	sselda 3603	. . . . . . . . . . . . . . 15 |- ( ( x e. b /\ c e. |^| b ) -> c e. x )
59	58	ancoms 469	. . . . . . . . . . . . . 14 |- ( ( c e. |^| b /\ x e. b ) -> c e. x )
60		elssuni 4467	. . . . . . . . . . . . . 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 482	. . . . . . . . . . . 12 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. b ) ) -> c C_ U. x )
63	12	adantrl 752	. . . . . . . . . . . . 13 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. b ) ) -> x e. (TopOn ` B ) )
64		toponuni 20719	. . . . . . . . . . . . 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 3642	. . . . . . . . . . 11 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. b ) ) -> c C_ B )
67	66	expr 643	. . . . . . . . . 10 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c e. |^| b ) -> ( x e. b -> c C_ B ) )
68	67	exlimdv 1861	. . . . . . . . 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 2966	. . . . . . 7 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> A. c e. |^| b c C_ B )
71		unissb 4469	. . . . . . 7 |- ( U. |^| b C_ B <-> A. c e. |^| b c C_ B )
72	70, 71	sylibr 224	. . . . . 6 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> U. |^| b C_ B )
73	72	3adant1 1079	. . . . 5 |- ( ( B e. V /\ b C_ (TopOn ` B ) /\ b =/= (/) ) -> U. |^| b C_ B )
74	11	sselda 3603	. . . . . . . . . 10 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c e. b ) -> c e. (TopOn ` B ) )
75		toponuni 20719	. . . . . . . . . 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 20718	. . . . . . . . . 10 |- ( c e. (TopOn ` B ) -> c e. Top )
78		eqid 2622	. . . . . . . . . . 11 |- U. c = U. c
79	78	topopn 20711	. . . . . . . . . 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 2701	. . . . . . . 8 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c e. b ) -> B e. c )
82	81	ralrimiva 2966	. . . . . . 7 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> A. c e. b B e. c )
83	82	3adant1 1079	. . . . . 6 |- ( ( B e. V /\ b C_ (TopOn ` B ) /\ b =/= (/) ) -> A. c e. b B e. c )
84		elintg 4483	. . . . . . 7 |- ( B e. V -> ( B e. |^| b <-> A. c e. b B e. c ) )
85	84	3ad2ant1 1082	. . . . . 6 |- ( ( B e. V /\ b C_ (TopOn ` B ) /\ b =/= (/) ) -> ( B e. |^| b <-> A. c e. b B e. c ) )
86	83, 85	mpbird 247	. . . . 5 |- ( ( B e. V /\ b C_ (TopOn ` B ) /\ b =/= (/) ) -> B e. |^| b )
87		unissel 4468	. . . . 5 |- ( ( U. |^| b C_ B /\ B e. |^| b ) -> U. |^| b = B )
88	73, 86, 87	syl2anc 693	. . . 4 |- ( ( B e. V /\ b C_ (TopOn ` B ) /\ b =/= (/) ) -> U. |^| b = B )
89	88	eqcomd 2628	. . 3 |- ( ( B e. V /\ b C_ (TopOn ` B ) /\ b =/= (/) ) -> B = U. |^| b )
90		istopon 20717	. . 3 |- ( |^| b e. (TopOn ` B ) <-> ( |^| b e. Top /\ B = U. |^| b ) )
91	54, 89, 90	sylanbrc 698	. 2 |- ( ( B e. V /\ b C_ (TopOn ` B ) /\ b =/= (/) ) -> |^| b e. (TopOn ` B ) )
92	9, 10, 91	ismred 16262	1 |- ( B e. V -> (TopOn ` B ) e. (Moore ` ~P B ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   A.wal 1481   = wceq 1483   E.wex 1704   e. wcel 1990   =/= wne 2794   A.wral 2912   _Vcvv 3200   i^i cin 3573   C_ wss 3574   (/)c0 3915   ~Pcpw 4158   U.cuni 4436   |^|cint 4475   ` cfv 5888  Moorecmre 16242   Topctop 20698  TopOnctopon 20715

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-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

This theorem is referenced by:  topmtcl  32358