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 φ J = topGen B
elcls3.2 φ X = J
elcls3.3 φ B TopBases
elcls3.4 φ S X
elcls3.5 φ P X
Assertion elcls3 φ P cls J S x B P x x S

Proof

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