Metamath Proof Explorer

Theorem toponmre

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 . (Contributed by Stefan O'Rear, 31-Jan-2015) (Revised by Mario Carneiro, 5-May-2015)

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

Proof

Step Hyp Ref Expression
1 toponsspwpw 
 |-  ( TopOn ` B ) C_ ~P ~P B
2 1 a1i 
 |-  ( B e. V -> ( TopOn ` B ) C_ ~P ~P B )
3 distopon 
 |-  ( B e. V -> ~P B e. ( TopOn ` B ) )
4 simpl 
 |-  ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) -> b C_ ( TopOn ` B ) )
5 4 sselda 
 |-  ( ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) /\ x e. b ) -> x e. ( TopOn ` B ) )
6 5 adantrl 
 |-  ( ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) /\ ( c C_ |^| b /\ x e. b ) ) -> x e. ( TopOn ` B ) )
7 topontop 
 |-  ( x e. ( TopOn ` B ) -> x e. Top )
8 6 7 syl 
 |-  ( ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) /\ ( c C_ |^| b /\ x e. b ) ) -> x e. Top )
9 simpl 
 |-  ( ( c C_ |^| b /\ x e. b ) -> c C_ |^| b )
10 intss1 
 |-  ( x e. b -> |^| b C_ x )
11 10 adantl 
 |-  ( ( c C_ |^| b /\ x e. b ) -> |^| b C_ x )
12 9 11 sstrd 
 |-  ( ( c C_ |^| b /\ x e. b ) -> c C_ x )
13 12 adantl 
 |-  ( ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) /\ ( c C_ |^| b /\ x e. b ) ) -> c C_ x )
14 uniopn 
 |-  ( ( x e. Top /\ c C_ x ) -> U. c e. x )
15 8 13 14 syl2anc 
 |-  ( ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) /\ ( c C_ |^| b /\ x e. b ) ) -> U. c e. x )
16 15 expr 
 |-  ( ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) /\ c C_ |^| b ) -> ( x e. b -> U. c e. x ) )
17 16 ralrimiv 
 |-  ( ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) /\ c C_ |^| b ) -> A. x e. b U. c e. x )
18 vuniex 
 |-  U. c e. _V
19 18 elint2 
 |-  ( U. c e. |^| b <-> A. x e. b U. c e. x )
20 17 19 sylibr 
 |-  ( ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) /\ c C_ |^| b ) -> U. c e. |^| b )
21 20 ex 
 |-  ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) -> ( c C_ |^| b -> U. c e. |^| b ) )
22 21 alrimiv 
 |-  ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) -> A. c ( c C_ |^| b -> U. c e. |^| b ) )
23 simpll 
 |-  ( ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) -> b C_ ( TopOn ` B ) )
24 23 sselda 
 |-  ( ( ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> y e. ( TopOn ` B ) )
25 topontop 
 |-  ( y e. ( TopOn ` B ) -> y e. Top )
26 24 25 syl 
 |-  ( ( ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> y e. Top )
27 intss1 
 |-  ( y e. b -> |^| b C_ y )
28 27 adantl 
 |-  ( ( ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> |^| b C_ y )
29 simplrl 
 |-  ( ( ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> c e. |^| b )
30 28 29 sseldd 
 |-  ( ( ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> c e. y )
31 simplrr 
 |-  ( ( ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> x e. |^| b )
32 28 31 sseldd 
 |-  ( ( ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> x e. y )
33 inopn 
 |-  ( ( y e. Top /\ c e. y /\ x e. y ) -> ( c i^i x ) e. y )
34 26 30 32 33 syl3anc 
 |-  ( ( ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) /\ y e. b ) -> ( c i^i x ) e. y )
35 34 ralrimiva 
 |-  ( ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) -> A. y e. b ( c i^i x ) e. y )
36 vex 
 |-  c e. _V
37 36 inex1 
 |-  ( c i^i x ) e. _V
38 37 elint2 
 |-  ( ( c i^i x ) e. |^| b <-> A. y e. b ( c i^i x ) e. y )
39 35 38 sylibr 
 |-  ( ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. |^| b ) ) -> ( c i^i x ) e. |^| b )
40 39 ralrimivva 
 |-  ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) -> A. c e. |^| b A. x e. |^| b ( c i^i x ) e. |^| b )
41 intex 
 |-  ( b =/= (/) <-> |^| b e. _V )
42 41 biimpi 
 |-  ( b =/= (/) -> |^| b e. _V )
43 42 adantl 
 |-  ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) -> |^| b e. _V )
44 istopg 
 |-  ( |^| 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 ) ) )
45 43 44 syl 
 |-  ( ( 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 ) ) )
46 22 40 45 mpbir2and 
 |-  ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) -> |^| b e. Top )
47 46 3adant1 
 |-  ( ( B e. V /\ b C_ ( TopOn ` B ) /\ b =/= (/) ) -> |^| b e. Top )
48 n0 
 |-  ( b =/= (/) <-> E. x x e. b )
49 48 biimpi 
 |-  ( b =/= (/) -> E. x x e. b )
50 49 ad2antlr 
 |-  ( ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) /\ c e. |^| b ) -> E. x x e. b )
51 10 sselda 
 |-  ( ( x e. b /\ c e. |^| b ) -> c e. x )
52 51 ancoms 
 |-  ( ( c e. |^| b /\ x e. b ) -> c e. x )
53 elssuni 
 |-  ( c e. x -> c C_ U. x )
54 52 53 syl 
 |-  ( ( c e. |^| b /\ x e. b ) -> c C_ U. x )
55 54 adantl 
 |-  ( ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. b ) ) -> c C_ U. x )
56 5 adantrl 
 |-  ( ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. b ) ) -> x e. ( TopOn ` B ) )
57 toponuni 
 |-  ( x e. ( TopOn ` B ) -> B = U. x )
58 56 57 syl 
 |-  ( ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. b ) ) -> B = U. x )
59 55 58 sseqtrrd 
 |-  ( ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) /\ ( c e. |^| b /\ x e. b ) ) -> c C_ B )
60 59 expr 
 |-  ( ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) /\ c e. |^| b ) -> ( x e. b -> c C_ B ) )
61 60 exlimdv 
 |-  ( ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) /\ c e. |^| b ) -> ( E. x x e. b -> c C_ B ) )
62 50 61 mpd 
 |-  ( ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) /\ c e. |^| b ) -> c C_ B )
63 62 ralrimiva 
 |-  ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) -> A. c e. |^| b c C_ B )
64 unissb 
 |-  ( U. |^| b C_ B <-> A. c e. |^| b c C_ B )
65 63 64 sylibr 
 |-  ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) -> U. |^| b C_ B )
66 65 3adant1 
 |-  ( ( B e. V /\ b C_ ( TopOn ` B ) /\ b =/= (/) ) -> U. |^| b C_ B )
67 4 sselda 
 |-  ( ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) /\ c e. b ) -> c e. ( TopOn ` B ) )
68 toponuni 
 |-  ( c e. ( TopOn ` B ) -> B = U. c )
69 67 68 syl 
 |-  ( ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) /\ c e. b ) -> B = U. c )
70 topontop 
 |-  ( c e. ( TopOn ` B ) -> c e. Top )
71 eqid 
 |-  U. c = U. c
72 71 topopn 
 |-  ( c e. Top -> U. c e. c )
73 67 70 72 3syl 
 |-  ( ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) /\ c e. b ) -> U. c e. c )
74 69 73 eqeltrd 
 |-  ( ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) /\ c e. b ) -> B e. c )
75 74 ralrimiva 
 |-  ( ( b C_ ( TopOn ` B ) /\ b =/= (/) ) -> A. c e. b B e. c )
76 75 3adant1 
 |-  ( ( B e. V /\ b C_ ( TopOn ` B ) /\ b =/= (/) ) -> A. c e. b B e. c )
77 elintg 
 |-  ( B e. V -> ( B e. |^| b <-> A. c e. b B e. c ) )
78 77 3ad2ant1 
 |-  ( ( B e. V /\ b C_ ( TopOn ` B ) /\ b =/= (/) ) -> ( B e. |^| b <-> A. c e. b B e. c ) )
79 76 78 mpbird 
 |-  ( ( B e. V /\ b C_ ( TopOn ` B ) /\ b =/= (/) ) -> B e. |^| b )
80 unissel 
 |-  ( ( U. |^| b C_ B /\ B e. |^| b ) -> U. |^| b = B )
81 66 79 80 syl2anc 
 |-  ( ( B e. V /\ b C_ ( TopOn ` B ) /\ b =/= (/) ) -> U. |^| b = B )
82 81 eqcomd 
 |-  ( ( B e. V /\ b C_ ( TopOn ` B ) /\ b =/= (/) ) -> B = U. |^| b )
83 istopon 
 |-  ( |^| b e. ( TopOn ` B ) <-> ( |^| b e. Top /\ B = U. |^| b ) )
84 47 82 83 sylanbrc 
 |-  ( ( B e. V /\ b C_ ( TopOn ` B ) /\ b =/= (/) ) -> |^| b e. ( TopOn ` B ) )
85 2 3 84 ismred 
 |-  ( B e. V -> ( TopOn ` B ) e. ( Moore ` ~P B ) )