Metamath Proof Explorer

Theorem elcls3

Description: Membership in a closure in terms of the members of a basis. Theorem 6.5(b) of Munkres p. 95. (Contributed by NM, 26-Feb-2007) (Revised by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypotheses elcls3.1 
|- ( ph -> J = ( topGen ` B ) )
elcls3.2 
|- ( ph -> X = U. J )
elcls3.3 
|- ( ph -> B e. TopBases )
elcls3.4 
|- ( ph -> S C_ X )
elcls3.5 
|- ( ph -> P e. X )
Assertion elcls3 
|- ( ph -> ( P e. ( ( cls ` J ) ` S ) <-> A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) ) )

Proof

Step Hyp Ref Expression
1 elcls3.1 
 |-  ( ph -> J = ( topGen ` B ) )
2 elcls3.2 
 |-  ( ph -> X = U. J )
3 elcls3.3 
 |-  ( ph -> B e. TopBases )
4 elcls3.4 
 |-  ( ph -> S C_ X )
5 elcls3.5 
 |-  ( ph -> P e. X )
6 tgcl 
 |-  ( B e. TopBases -> ( topGen ` B ) e. Top )
7 3 6 syl 
 |-  ( ph -> ( topGen ` B ) e. Top )
8 1 7 eqeltrd 
 |-  ( ph -> J e. Top )
9 4 2 sseqtrd 
 |-  ( ph -> S C_ U. J )
10 5 2 eleqtrd 
 |-  ( ph -> P e. U. J )
11 eqid 
 |-  U. J = U. J
12 11 elcls 
 |-  ( ( J e. Top /\ S C_ U. J /\ P e. U. J ) -> ( P e. ( ( cls ` J ) ` S ) <-> A. y e. J ( P e. y -> ( y i^i S ) =/= (/) ) ) )
13 8 9 10 12 syl3anc 
 |-  ( ph -> ( P e. ( ( cls ` J ) ` S ) <-> A. y e. J ( P e. y -> ( y i^i S ) =/= (/) ) ) )
14 bastg 
 |-  ( B e. TopBases -> B C_ ( topGen ` B ) )
15 3 14 syl 
 |-  ( ph -> B C_ ( topGen ` B ) )
16 15 1 sseqtrrd 
 |-  ( ph -> B C_ J )
17 16 sseld 
 |-  ( ph -> ( y e. B -> y e. J ) )
18 17 imim1d 
 |-  ( ph -> ( ( y e. J -> ( P e. y -> ( y i^i S ) =/= (/) ) ) -> ( y e. B -> ( P e. y -> ( y i^i S ) =/= (/) ) ) ) )
19 18 ralimdv2 
 |-  ( ph -> ( A. y e. J ( P e. y -> ( y i^i S ) =/= (/) ) -> A. y e. B ( P e. y -> ( y i^i S ) =/= (/) ) ) )
20 eleq2w 
 |-  ( y = x -> ( P e. y <-> P e. x ) )
21 ineq1 
 |-  ( y = x -> ( y i^i S ) = ( x i^i S ) )
22 21 neeq1d 
 |-  ( y = x -> ( ( y i^i S ) =/= (/) <-> ( x i^i S ) =/= (/) ) )
23 20 22 imbi12d 
 |-  ( y = x -> ( ( P e. y -> ( y i^i S ) =/= (/) ) <-> ( P e. x -> ( x i^i S ) =/= (/) ) ) )
24 23 cbvralvw 
 |-  ( A. y e. B ( P e. y -> ( y i^i S ) =/= (/) ) <-> A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) )
25 19 24 imbitrdi 
 |-  ( ph -> ( A. y e. J ( P e. y -> ( y i^i S ) =/= (/) ) -> A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) ) )
26 simprl 
 |-  ( ( ( ph /\ A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) ) /\ ( y e. J /\ P e. y ) ) -> y e. J )
27 1 ad2antrr 
 |-  ( ( ( ph /\ A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) ) /\ ( y e. J /\ P e. y ) ) -> J = ( topGen ` B ) )
28 26 27 eleqtrd 
 |-  ( ( ( ph /\ A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) ) /\ ( y e. J /\ P e. y ) ) -> y e. ( topGen ` B ) )
29 simprr 
 |-  ( ( ( ph /\ A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) ) /\ ( y e. J /\ P e. y ) ) -> P e. y )
30 tg2 
 |-  ( ( y e. ( topGen ` B ) /\ P e. y ) -> E. z e. B ( P e. z /\ z C_ y ) )
31 28 29 30 syl2anc 
 |-  ( ( ( ph /\ A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) ) /\ ( y e. J /\ P e. y ) ) -> E. z e. B ( P e. z /\ z C_ y ) )
32 eleq2w 
 |-  ( x = z -> ( P e. x <-> P e. z ) )
33 ineq1 
 |-  ( x = z -> ( x i^i S ) = ( z i^i S ) )
34 33 neeq1d 
 |-  ( x = z -> ( ( x i^i S ) =/= (/) <-> ( z i^i S ) =/= (/) ) )
35 32 34 imbi12d 
 |-  ( x = z -> ( ( P e. x -> ( x i^i S ) =/= (/) ) <-> ( P e. z -> ( z i^i S ) =/= (/) ) ) )
36 35 rspccva 
 |-  ( ( A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) /\ z e. B ) -> ( P e. z -> ( z i^i S ) =/= (/) ) )
37 36 imp 
 |-  ( ( ( A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) /\ z e. B ) /\ P e. z ) -> ( z i^i S ) =/= (/) )
38 ssdisj 
 |-  ( ( z C_ y /\ ( y i^i S ) = (/) ) -> ( z i^i S ) = (/) )
39 38 ex 
 |-  ( z C_ y -> ( ( y i^i S ) = (/) -> ( z i^i S ) = (/) ) )
40 39 necon3d 
 |-  ( z C_ y -> ( ( z i^i S ) =/= (/) -> ( y i^i S ) =/= (/) ) )
41 37 40 syl5com 
 |-  ( ( ( A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) /\ z e. B ) /\ P e. z ) -> ( z C_ y -> ( y i^i S ) =/= (/) ) )
42 41 exp31 
 |-  ( A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) -> ( z e. B -> ( P e. z -> ( z C_ y -> ( y i^i S ) =/= (/) ) ) ) )
43 42 imp4a 
 |-  ( A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) -> ( z e. B -> ( ( P e. z /\ z C_ y ) -> ( y i^i S ) =/= (/) ) ) )
44 43 rexlimdv 
 |-  ( A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) -> ( E. z e. B ( P e. z /\ z C_ y ) -> ( y i^i S ) =/= (/) ) )
45 44 ad2antlr 
 |-  ( ( ( ph /\ A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) ) /\ ( y e. J /\ P e. y ) ) -> ( E. z e. B ( P e. z /\ z C_ y ) -> ( y i^i S ) =/= (/) ) )
46 31 45 mpd 
 |-  ( ( ( ph /\ A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) ) /\ ( y e. J /\ P e. y ) ) -> ( y i^i S ) =/= (/) )
47 46 exp43 
 |-  ( ph -> ( A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) -> ( y e. J -> ( P e. y -> ( y i^i S ) =/= (/) ) ) ) )
48 47 ralrimdv 
 |-  ( ph -> ( A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) -> A. y e. J ( P e. y -> ( y i^i S ) =/= (/) ) ) )
49 25 48 impbid 
 |-  ( ph -> ( A. y e. J ( P e. y -> ( y i^i S ) =/= (/) ) <-> A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) ) )
50 13 49 bitrd 
 |-  ( ph -> ( P e. ( ( cls ` J ) ` S ) <-> A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) ) )