Theorem tgss2t 7587

Description: A criterion for determining whether one topology is finer than another, based on a comparison of their bases. Lemma 2.2 of [Munkres] p. 80.

Assertion

Ref	Expression
tgss2t	|- ((B e. Bases /\ C e. Bases /\ U.B = U.C) -> ((topGen` B) (_ (topGen` C) <-> A.x e. U.BA.y e. B (x e. y -> E.z e. C (x e. z /\ z (_ y))))

Distinct variable groups:   x,y,z,B   x,C,y,z

Proof of Theorem tgss2t

Step	Hyp	Ref	Expression
1		tg2t 7571	. . . . . 6 |- ((C e. Bases /\ y e. (topGen` C) /\ x e. y) -> E.z e. C (x e. z /\ z (_ y))
2		pm3.27 323	. . . . . . 7 |- ((B e. Bases /\ C e. Bases) -> C e. Bases)
3	2	ad2antrr 404	. . . . . 6 |- ((((B e. Bases /\ C e. Bases) /\ (topGen` B) (_ (topGen` C)) /\ ((x e. U.B /\ y e. B) /\ x e. y)) -> C e. Bases)
4		sstr 2068	. . . . . . . . . . . 12 |- ((B (_ (topGen` B) /\ (topGen` B) (_ (topGen` C)) -> B (_ (topGen` C))
5		bastgt 7572	. . . . . . . . . . . 12 |- (B e. Bases -> B (_ (topGen` B))
6	4, 5	sylan 448	. . . . . . . . . . 11 |- ((B e. Bases /\ (topGen` B) (_ (topGen` C)) -> B (_ (topGen` C))
7	6	sseld 2063	. . . . . . . . . 10 |- ((B e. Bases /\ (topGen` B) (_ (topGen` C)) -> (y e. B -> y e. (topGen` C)))
8	7	imp 350	. . . . . . . . 9 |- (((B e. Bases /\ (topGen` B) (_ (topGen` C)) /\ y e. B) -> y e. (topGen` C))
9	8	adantllr 397	. . . . . . . 8 |- ((((B e. Bases /\ C e. Bases) /\ (topGen` B) (_ (topGen` C)) /\ y e. B) -> y e. (topGen` C))
10	9	adantrl 394	. . . . . . 7 |- ((((B e. Bases /\ C e. Bases) /\ (topGen` B) (_ (topGen` C)) /\ (x e. U.B /\ y e. B)) -> y e. (topGen` C))
11	10	adantrr 395	. . . . . 6 |- ((((B e. Bases /\ C e. Bases) /\ (topGen` B) (_ (topGen` C)) /\ ((x e. U.B /\ y e. B) /\ x e. y)) -> y e. (topGen` C))
12		simprr 415	. . . . . 6 |- ((((B e. Bases /\ C e. Bases) /\ (topGen` B) (_ (topGen` C)) /\ ((x e. U.B /\ y e. B) /\ x e. y)) -> x e. y)
13	1, 3, 11, 12	syl3anc 857	. . . . 5 |- ((((B e. Bases /\ C e. Bases) /\ (topGen` B) (_ (topGen` C)) /\ ((x e. U.B /\ y e. B) /\ x e. y)) -> E.z e. C (x e. z /\ z (_ y))
14	13	exp43 384	. . . 4 |- ((B e. Bases /\ C e. Bases) -> ((topGen` B) (_ (topGen` C) -> ((x e. U.B /\ y e. B) -> (x e. y -> E.z e. C (x e. z /\ z (_ y)))))
15	14	r19.21advv 1718	. . 3 |- ((B e. Bases /\ C e. Bases) -> ((topGen` B) (_ (topGen` C) -> A.x e. U.BA.y e. B (x e. y -> E.z e. C (x e. z /\ z (_ y))))
16	15	3adant3 798	. 2 |- ((B e. Bases /\ C e. Bases /\ U.B = U.C) -> ((topGen` B) (_ (topGen` C) -> A.x e. U.BA.y e. B (x e. y -> E.z e. C (x e. z /\ z (_ y))))
17		eltg2t 7569	. . . . . . . . . 10 |- (C e. Bases -> (u e. (topGen` C) <-> (u (_ U.C /\ A.w e. u E.z e. C (w e. z /\ z (_ u))))
18		tg1t 7570	. . . . . . . . . . . . . 14 |- ((B e. Bases /\ u e. (topGen` B)) -> u (_ U.B)
19	18	adantll 392	. . . . . . . . . . . . 13 |- (((U.B = U.C /\ B e. Bases) /\ u e. (topGen` B)) -> u (_ U.B)
20		simpll 412	. . . . . . . . . . . . 13 |- (((U.B = U.C /\ B e. Bases) /\ u e. (topGen` B)) -> U.B = U.C)
21	19, 20	sseqtrd 2093	. . . . . . . . . . . 12 |- (((U.B = U.C /\ B e. Bases) /\ u e. (topGen` B)) -> u (_ U.C)
22	21	adantrl 394	. . . . . . . . . . 11 |- (((U.B = U.C /\ B e. Bases) /\ (A.x e. U.BA.y e. B (x e. y -> E.z e. C (x e. z /\ z (_ y)) /\ u e. (topGen` B))) -> u (_ U.C)
23		elssuni 2521	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (v e. B -> v (_ U.B)
24	23	sseld 2063	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (v e. B -> (w e. v -> w e. U.B))
25	24	imp 350	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((v e. B /\ w e. v) -> w e. U.B)
26	25	adantrr 395	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((v e. B /\ (w e. v /\ v (_ u)) -> w e. U.B)
27	26	adantrl 394	. . . . . . . . . . . . . . . . . . . . . 22 |- ((v e. B /\ (A.x e. U.BA.y e. B (x e. y -> E.z e. C (x e. z /\ z (_ y)) /\ (w e. v /\ v (_ u))) -> w e. U.B)
28		elequ1 1134	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x = w -> (x e. y <-> w e. y))
29		elequ1 1134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (x = w -> (x e. z <-> w e. z))
30	29	anbi1d 616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (x = w -> ((x e. z /\ z (_ y) <-> (w e. z /\ z (_ y)))
31	30	rexbidv 1661	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x = w -> (E.z e. C (x e. z /\ z (_ y) <-> E.z e. C (w e. z /\ z (_ y)))
32	28, 31	imbi12d 625	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x = w -> ((x e. y -> E.z e. C (x e. z /\ z (_ y)) <-> (w e. y -> E.z e. C (w e. z /\ z (_ y))))
33		elequ2 1135	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (y = v -> (w e. y <-> w e. v))
34		sseq2 2079	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (y = v -> (z (_ y <-> z (_ v))
35	34	anbi2d 615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (y = v -> ((w e. z /\ z (_ y) <-> (w e. z /\ z (_ v)))
36	35	rexbidv 1661	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (y = v -> (E.z e. C (w e. z /\ z (_ y) <-> E.z e. C (w e. z /\ z (_ v)))
37	33, 36	imbi12d 625	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (y = v -> ((w e. y -> E.z e. C (w e. z /\ z (_ y)) <-> (w e. v -> E.z e. C (w e. z /\ z (_ v))))
38	32, 37	rcla42v 1876	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((w e. U.B /\ v e. B) -> (A.x e. U.BA.y e. B (x e. y -> E.z e. C (x e. z /\ z (_ y)) -> (w e. v -> E.z e. C (w e. z /\ z (_ v))))
39	38	ex 373	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (w e. U.B -> (v e. B -> (A.x e. U.BA.y e. B (x e. y -> E.z e. C (x e. z /\ z (_ y)) -> (w e. v -> E.z e. C (w e. z /\ z (_ v)))))
40	39	com4l 39	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (v e. B -> (A.x e. U.BA.y e. B (x e. y -> E.z e. C (x e. z /\ z (_ y)) -> (w e. v -> (w e. U.B -> E.z e. C (w e. z /\ z (_ v)))))
41	40	imp32 363	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((v e. B /\ (A.x e. U.BA.y e. B (x e. y -> E.z e. C (x e. z /\ z (_ y)) /\ w e. v)) -> (w e. U.B -> E.z e. C (w e. z /\ z (_ v)))
42	41	adantrrr 403	. . . . . . . . . . . . . . . . . . . . . 22 |- ((v e. B /\ (A.x e. U.BA.y e. B (x e. y -> E.z e. C (x e. z /\ z (_ y)) /\ (w e. v /\ v (_ u))) -> (w e. U.B -> E.z e. C (w e. z /\ z (_ v)))
43	27, 42	mpd 26	. . . . . . . . . . . . . . . . . . . . 21 |- ((v e. B /\ (A.x e. U.BA.y e. B (x e. y -> E.z e. C (x e. z /\ z (_ y)) /\ (w e. v /\ v (_ u))) -> E.z e. C (w e. z /\ z (_ v))
44	43	an1s 486	. . . . . . . . . . . . . . . . . . . 20 |- ((A.x e. U.BA.y e. B (x e. y -> E.z e. C (x e. z /\ z (_ y)) /\ (v e. B /\ (w e. v /\ v (_ u))) -> E.z e. C (w e. z /\ z (_ v))
45		sstr2 2067	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (z (_ v -> (v (_ u -> z (_ u))
46	45	com12 11	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (v (_ u -> (z (_ v -> z (_ u))
47	46	anim2d 560	. . . . . . . . . . . . . . . . . . . . . . 23 |- (v (_ u -> ((w e. z /\ z (_ v) -> (w e. z /\ z (_ u)))
48	47	r19.22sdv 1735	. . . . . . . . . . . . . . . . . . . . . 22 |- (v (_ u -> (E.z e. C (w e. z /\ z (_ v) -> E.z e. C (w e. z /\ z (_ u)))
49	48	adantl 388	. . . . . . . . . . . . . . . . . . . . 21 |- ((w e. v /\ v (_ u) -> (E.z e. C (w e. z /\ z (_ v) -> E.z e. C (w e. z /\ z (_ u)))
50	49	ad2antll 407	. . . . . . . . . . . . . . . . . . . 20 |- ((A.x e. U.BA.y e. B (x e. y -> E.z e. C (x e. z /\ z (_ y)) /\ (v e. B /\ (w e. v /\ v (_ u))) -> (E.z e. C (w e. z /\ z (_ v) -> E.z e. C (w e. z /\ z (_ u)))
51	44, 50	mpd 26	. . . . . . . . . . . . . . . . . . 19 |- ((A.x e. U.BA.y e. B (x e. y -> E.z e. C (x e. z /\ z (_ y)) /\ (v e. B /\ (w e. v /\ v (_ u))) -> E.z e. C (w e. z /\ z (_ u))
52	51	exp32 377	. . . . . . . . . . . . . . . . . 18 |- (A.