Theorem toponmre 18813

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 18716. (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 18648	. . . . . 6 |- ( b e. (TopOn ` B ) -> B = U. b )
2		eqimss2 3507	. . . . . . 7 |- ( B = U. b -> U. b C_ B )
3		sspwuni 4354	. . . . . . 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 3965	. . . . 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 3458	. . 3 |- (TopOn ` B ) C_ ~P ~P B
9	8	a1i 11	. 2 |- ( B e. V -> (TopOn ` B ) C_ ~P ~P B )
10		distopon 18717	. 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 3454	. . . . . . . . . . . . 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 18647	. . . . . . . . . . . 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 4241	. . . . . . . . . . . . . 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 3464	. . . . . . . . . . . 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 18626	. . . . . . . . . . 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 2820	. . . . . . . 8 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c C_ |^| b ) -> A. x e. b U. c e. x )
25		vex 3071	. . . . . . . . . 10 |- c e. _V
26	25	uniex 6476	. . . . . . . . 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 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 1686	. . . . 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 3454	. . . . . . . . . 10 |- ( ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> y e. (TopOn ` B ) )
33		topontop 18647	. . . . . . . . . 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 4241	. . . . . . . . . . 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 3455	. . . . . . . . 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 3455	. . . . . . . . 9 |- ( ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> x e. y )
41		inopn 18628	. . . . . . . . 9 |- ( ( y e. Top /\ c e. y /\ x e. y ) -> ( c i^i x ) e. y )
42	34, 38, 40, 41	syl3anc 1219	. . . . . . . 8 |- ( ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> ( c i^i x ) e. y )
43	42	ralrimiva 2822	. . . . . . 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 4531	. . . . . . . 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 212	. . . . . 6 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) -> ( c i^i x ) e. |^| b )
47	46	ralrimivva 2904	. . . . 5 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> A. c e. |^| b A. x e. |^| b ( c i^i x ) e. |^| b )
48		intex 4546	. . . . . . . 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 18624	. . . . . 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 913	. . . 4 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> |^| b e. Top )
54	53	3adant1 1006	. . 3 |- ( ( B e. V /\ b C_ (TopOn ` B ) /\ b =/= (/) ) -> |^| b e. Top )
55		n0 3744	. . . . . . . . . . 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 3454	. . . . . . . . . . . . . . 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 4219	. . . . . . . . . . . . . 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 18648	. . . . . . . . . . . . 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 3491	. . . . . . . . . . 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 1691	. . . . . . . . 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 2822	. . . . . . 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 212	. . . . . 6 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> U. |^| b C_ B )
73	72	3adant1 1006	. . . . 5 |- ( ( B e. V /\ b C_ (TopOn ` B ) /\ b =/= (/) ) -> U. |^| b C_ B )
74	11	sselda 3454	. . . . . . . . . 10 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c e. b ) -> c e. (TopOn ` B ) )
75		toponuni 18648	. . . . . . . . . 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 18647	. . . . . . . . . 10 |- ( c e. (TopOn ` B ) -> c e. Top )
78		eqid 2451	. . . . . . . . . . 11 |- U. c = U. c
79	78	topopn 18635	. . . . . . . . . 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 2539	. . . . . . . 8 |- ( ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) /\ c e. b ) -> B e. c )
82	81	ralrimiva 2822	. . . . . . 7 |- ( ( b C_ (TopOn ` B ) /\ b =/= (/) ) -> A. c e. b B e. c )
83	82	3adant1 1006	. . . . . 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 1009	. . . . . 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 4220	. . . . 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 2459	. . 3 |- ( ( B e. V /\ b C_ (TopOn ` B ) /\ b =/= (/) ) -> B = U. |^| b )
90		istopon 18646	. . 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 14642	1 |- ( B e. V -> (TopOn ` B ) e. (Moore ` ~P B ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 965   A.wal 1368   = wceq 1370   E.wex 1587   e. wcel 1758   =/= wne 2644   A.wral 2795   _Vcvv 3068   i^i cin 3425   C_ wss 3426   (/)c0 3735   ~Pcpw 3958   U.cuni 4189   |^|cint 4226   ` cfv 5516  Moorecmre 14622   Topctop 18614  TopOnctopon 18615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pow 4568  ax-pr 4629  ax-un 6472

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3070  df-sbc 3285  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-pw 3960  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-int 4227  df-br 4391  df-opab 4449  df-mpt 4450  df-id 4734  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-iota 5479  df-fun 5518  df-fv 5524  df-mre 14626  df-top 18619  df-topon 18622

This theorem is referenced by:  topmtcl  28722