Theorem toponmre 19462

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 19365. (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 19297	. . . . . 6 |- ( b e. (TopOn ` B ) -> B = U. b )
2		eqimss2 3562	. . . . . . 7 |- ( B = U. b -> U. b C_ B )
3		sspwuni 4417	. . . . . . 7 |- ( b C_ ~P B <-> U. b C_ B )
4	2, 3	sylibr 212	. . . . . 6 |- ( B = U. b -> b C_ ~P B )
5	1, 4	syl 16	. . . . 5 |- ( b e. (TopOn ` B ) -> b C_ ~P B )
6		selpw 4023	. . . . 5 |- ( b e. ~P ~P B <-> b C_ ~P B )
7	5, 6	sylibr 212	. . . 4 |- ( b e. (TopOn ` B ) -> b e. ~P ~P B )
8	7	ssriv 3513	. . 3 |- (TopOn ` B ) C_ ~P ~P B
9	8	a1i 11	. 2 |- ( B e. V -> (TopOn ` B ) C_ ~P ~P B )
10		distopon 19366	. 2 |- ( B e. V -> ~P B e. (TopOn ` B ) )
11		simpl 457	. . . . . . . . . . . . . 14 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> b C_ (TopOn ` B ) )
12	11	sselda 3509	. . . . . . . . . . . . 13 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ x e. b ) -> x e. (TopOn ` B ) )
13	12	adantrl 715	. . . . . . . . . . . 12 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c C_ |^| b /\ x e. b ) ) -> x e. (TopOn ` B ) )
14		topontop 19296	. . . . . . . . . . . 12 |- ( x e. (TopOn ` B ) -> x e. Top )
15	13, 14	syl 16	. . . . . . . . . . 11 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c C_ |^| b /\ x e. b ) ) -> x e. Top )
16		simpl 457	. . . . . . . . . . . . 13 |- ( ( c C_ |^| b /\ x e. b ) -> c C_ |^| b )
17		intss1 4303	. . . . . . . . . . . . . 14 |- ( x e. b -> |^| b C_ x )
18	17	adantl 466	. . . . . . . . . . . . 13 |- ( ( c C_ |^| b /\ x e. b ) -> |^| b C_ x )
19	16, 18	sstrd 3519	. . . . . . . . . . . 12 |- ( ( c C_ |^| b /\ x e. b ) -> c C_ x )
20	19	adantl 466	. . . . . . . . . . 11 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c C_ |^| b /\ x e. b ) ) -> c C_ x )
21		uniopn 19275	. . . . . . . . . . 11 |- ( ( x e. Top /\ c C_ x ) -> U. c e. x )
22	15, 20, 21	syl2anc 661	. . . . . . . . . 10 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c C_ |^| b /\ x e. b ) ) -> U. c e. x )
23	22	expr 615	. . . . . . . . 9 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c C_ |^| b ) -> ( x e. b -> U. c e. x ) )
24	23	ralrimiv 2879	. . . . . . . 8 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c C_ |^| b ) -> A. x e. b U. c e. x )
25		vex 3121	. . . . . . . . . 10 |- c e. _V
26	25	uniex 6591	. . . . . . . . 9 |- U. c e. _V
27	26	elint2 4295	. . . . . . . 8 |- ( U. c e. |^| b <-> A. x e. b U. c e. x )
28	24, 27	sylibr 212	. . . . . . 7 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c C_ |^| b ) -> U. c e. |^| b )
29	28	ex 434	. . . . . 6 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> ( c C_ |^| b -> U. c e. |^| b ) )
30	29	alrimiv 1695	. . . . 5 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> A. c ( c C_ |^| b -> U. c e. |^| b ) )
31		simpll 753	. . . . . . . . . . 11 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) -> b C_ (TopOn ` B ) )
32	31	sselda 3509	. . . . . . . . . 10 |- ( ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> y e. (TopOn ` B ) )
33		topontop 19296	. . . . . . . . . 10 |- ( y e. (TopOn ` B ) -> y e. Top )
34	32, 33	syl 16	. . . . . . . . 9 |- ( ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> y e. Top )
35		intss1 4303	. . . . . . . . . . 11 |- ( y e. b -> |^| b C_ y )
36	35	adantl 466	. . . . . . . . . 10 |- ( ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> |^| b C_ y )
37		simplrl 759	. . . . . . . . . 10 |- ( ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> c e. |^| b )
38	36, 37	sseldd 3510	. . . . . . . . 9 |- ( ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> c e. y )
39		simplrr 760	. . . . . . . . . 10 |- ( ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> x e. |^| b )
40	36, 39	sseldd 3510	. . . . . . . . 9 |- ( ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> x e. y )
41		inopn 19277	. . . . . . . . 9 |- ( ( y e. Top /\ c e. y /\ x e. y ) -> ( c i^i x ) e. y )
42	34, 38, 40, 41	syl3anc 1228	. . . . . . . 8 |- ( ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> ( c i^i x ) e. y )
43	42	ralrimiva 2881	. . . . . . 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 4594	. . . . . . . 8 |- ( c i^i x ) e. _V
45	44	elint2 4295	. . . . . . 7 |- ( ( c i^i x ) e. |^| b <-> A. y e. b ( c i^i x ) e. y )
46	43, 45	sylibr 212	. . . . . 6 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) -> ( c i^i x ) e. |^| b )
47	46	ralrimivva 2888	. . . . 5 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> A. c e. |^| b A. x e. |^| b ( c i^i x ) e. |^| b )
48		intex 4609	. . . . . . . 8 |- ( b =/= (/) <-> |^| b e. _V )
49	48	biimpi 194	. . . . . . 7 |- ( b =/= (/) -> |^| b e. _V )
50	49	adantl 466	. . . . . 6 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> |^| b e. _V )
51		istopg 19273	. . . . . 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 16	. . . . 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 920	. . . 4 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> |^| b e. Top )
54	53	3adant1 1014	. . 3 |- ( ( B e. V /\ b C_ (TopOn ` B ) /\ b =/= (/) ) -> |^| b e. Top )
55		n0 3799	. . . . . . . . . . 11 |- ( b =/= (/) <-> E. x x e. b )
56	55	biimpi 194	. . . . . . . . . 10 |- ( b =/= (/) -> E. x x e. b )
57	56	ad2antlr 726	. . . . . . . . 9 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c e. |^| b ) -> E. x x e. b )
58	17	sselda 3509	. . . . . . . . . . . . . . 15 |- ( ( x e. b /\ c e. |^| b ) -> c e. x )
59	58	ancoms 453	. . . . . . . . . . . . . 14 |- ( ( c e. |^| b /\ x e. b ) -> c e. x )
60		elssuni 4281	. . . . . . . . . . . . . 14 |- ( c e. x -> c C_ U. x )
61	59, 60	syl 16	. . . . . . . . . . . . 13 |- ( ( c e. |^| b /\ x e. b ) -> c C_ U. x )
62	61	adantl 466	. . . . . . . . . . . 12 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. b ) ) -> c C_ U. x )
63	12	adantrl 715	. . . . . . . . . . . . 13 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. b ) ) -> x e. (TopOn ` B ) )
64		toponuni 19297	. . . . . . . . . . . . 13 |- ( x e. (TopOn ` B ) -> B = U. x )
65	63, 64	syl 16	. . . . . . . . . . . 12 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. b ) ) -> B = U. x )
66	62, 65	sseqtr4d 3546	. . . . . . . . . . 11 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. b ) ) -> c C_ B )
67	66	expr 615	. . . . . . . . . 10 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c e. |^| b ) -> ( x e. b -> c C_ B ) )
68	67	exlimdv 1700	. . . . . . . . 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 2881	. . . . . . 7 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> A. c e. |^| b c C_ B )
71		unissb 4283	. . . . . . 7 |- ( U. |^| b C_ B <-> A. c e. |^| b c C_ B )
72	70, 71	sylibr 212	. . . . . 6 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> U. |^| b C_ B )
73	72	3adant1 1014	. . . . 5 |- ( ( B e. V /\ b C_ (TopOn ` B ) /\ b =/= (/) ) -> U. |^| b C_ B )
74	11	sselda 3509	. . . . . . . . . 10 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c e. b ) -> c e. (TopOn ` B ) )
75		toponuni 19297	. . . . . . . . . 10 |- ( c e. (TopOn ` B ) -> B = U. c )
76	74, 75	syl 16	. . . . . . . . 9 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c e. b ) -> B = U. c )
77		topontop 19296	. . . . . . . . . 10 |- ( c e. (TopOn ` B ) -> c e. Top )
78		eqid 2467	. . . . . . . . . . 11 |- U. c = U. c
79	78	topopn 19284	. . . . . . . . . 10 |- ( c e. Top -> U. c e. c )
80	74, 77, 79	3syl 20	. . . . . . . . 9 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c e. b ) -> U. c e. c )
81	76, 80	eqeltrd 2555	. . . . . . . 8 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c e. b ) -> B e. c )
82	81	ralrimiva 2881	. . . . . . 7 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> A. c e. b B e. c )
83	82	3adant1 1014	. . . . . 6 |- ( ( B e. V /\ b C_ (TopOn ` B ) /\ b =/= (/) ) -> A. c e. b B e. c )
84		elintg 4296	. . . . . . 7 |- ( B e. V -> ( B e. |^| b <-> A. c e. b B e. c ) )
85	84	3ad2ant1 1017	. . . . . 6 |- ( ( B e. V /\ b C_ (TopOn ` B ) /\ b =/= (/) ) -> ( B e. |^| b <-> A. c e. b B e. c ) )
86	83, 85	mpbird 232	. . . . 5 |- ( ( B e. V /\ b C_ (TopOn ` B ) /\ b =/= (/) ) -> B e. |^| b )
87		unissel 4282	. . . . 5 |- ( ( U. |^| b C_ B /\ B e. |^| b ) -> U. |^| b = B )
88	73, 86, 87	syl2anc 661	. . . 4 |- ( ( B e. V /\ b C_ (TopOn ` B ) /\ b =/= (/) ) -> U. |^| b = B )
89	88	eqcomd 2475	. . 3 |- ( ( B e. V /\ b C_ (TopOn ` B ) /\ b =/= (/) ) -> B = U. |^| b )
90		istopon 19295	. . 3 |- ( |^| b e. (TopOn ` B ) <-> ( |^| b e. Top /\ B = U. |^| b ) )
91	54, 89, 90	sylanbrc 664	. 2 |- ( ( B e. V /\ b C_ (TopOn ` B ) /\ b =/= (/) ) -> |^| b e. (TopOn ` B ) )
92	9, 10, 91	ismred 14874	1 |- ( B e. V -> (TopOn ` B ) e. (Moore ` ~P B ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 973   A.wal 1377   = wceq 1379   E.wex 1596   e. wcel 1767   =/= wne 2662   A.wral 2817   _Vcvv 3118   i^i cin 3480   C_ wss 3481   (/)c0 3790   ~Pcpw 4016   U.cuni 4251   |^|cint 4288   ` cfv 5594  Moorecmre 14854   Topctop 19263  TopOnctopon 19264

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-rab 2826  df-v 3120  df-sbc 3337  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-op 4040  df-uni 4252  df-int 4289  df-br 4454  df-opab 4512  df-mpt 4513  df-id 4801  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-iota 5557  df-fun 5596  df-fv 5602  df-mre 14858  df-top 19268  df-topon 19271

This theorem is referenced by:  topmtcl  30108