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 syl6ib
 |-  ( 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 ) =/= (/) ) ) )