tgcn

Description: The continuity predicate when the range is given by a basis for a topology. (Contributed by Mario Carneiro, 7-Feb-2015) (Revised by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Hypotheses	tgcn.1	\|- ( ph -> J e. ( TopOn ` X ) )
	tgcn.3	\|- ( ph -> K = ( topGen ` B ) )
	tgcn.4	\|- ( ph -> K e. ( TopOn ` Y ) )
Assertion	tgcn	\|- ( ph -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. B ( `' F " y ) e. J ) ) )

Proof

Step	Hyp	Ref	Expression
1		tgcn.1	\|- ( ph -> J e. ( TopOn ` X ) )
2		tgcn.3	\|- ( ph -> K = ( topGen ` B ) )
3		tgcn.4	\|- ( ph -> K e. ( TopOn ` Y ) )
4		iscn	\|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. K ( `' F " y ) e. J ) ) )
5	1 3 4	syl2anc	\|- ( ph -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. K ( `' F " y ) e. J ) ) )
6		topontop	\|- ( K e. ( TopOn ` Y ) -> K e. Top )
7	3 6	syl	\|- ( ph -> K e. Top )
8	2 7	eqeltrrd	\|- ( ph -> ( topGen ` B ) e. Top )
9		tgclb	\|- ( B e. TopBases <-> ( topGen ` B ) e. Top )
10	8 9	sylibr	\|- ( ph -> B e. TopBases )
11		bastg	\|- ( B e. TopBases -> B C_ ( topGen ` B ) )
12	10 11	syl	\|- ( ph -> B C_ ( topGen ` B ) )
13	12 2	sseqtrrd	\|- ( ph -> B C_ K )
14		ssralv	\|- ( B C_ K -> ( A. y e. K ( `' F " y ) e. J -> A. y e. B ( `' F " y ) e. J ) )
15	13 14	syl	\|- ( ph -> ( A. y e. K ( `' F " y ) e. J -> A. y e. B ( `' F " y ) e. J ) )
16	2	eleq2d	\|- ( ph -> ( x e. K <-> x e. ( topGen ` B ) ) )
17		eltg3	\|- ( B e. TopBases -> ( x e. ( topGen ` B ) <-> E. z ( z C_ B /\ x = U. z ) ) )
18	10 17	syl	\|- ( ph -> ( x e. ( topGen ` B ) <-> E. z ( z C_ B /\ x = U. z ) ) )
19	16 18	bitrd	\|- ( ph -> ( x e. K <-> E. z ( z C_ B /\ x = U. z ) ) )
20		ssralv	\|- ( z C_ B -> ( A. y e. B ( `' F " y ) e. J -> A. y e. z ( `' F " y ) e. J ) )
21		topontop	\|- ( J e. ( TopOn ` X ) -> J e. Top )
22	1 21	syl	\|- ( ph -> J e. Top )
23		iunopn	\|- ( ( J e. Top /\ A. y e. z ( `' F " y ) e. J ) -> U_ y e. z ( `' F " y ) e. J )
24	23	ex	\|- ( J e. Top -> ( A. y e. z ( `' F " y ) e. J -> U_ y e. z ( `' F " y ) e. J ) )
25	22 24	syl	\|- ( ph -> ( A. y e. z ( `' F " y ) e. J -> U_ y e. z ( `' F " y ) e. J ) )
26	20 25	sylan9r	\|- ( ( ph /\ z C_ B ) -> ( A. y e. B ( `' F " y ) e. J -> U_ y e. z ( `' F " y ) e. J ) )
27		imaeq2	\|- ( x = U. z -> ( `' F " x ) = ( `' F " U. z ) )
28		imauni	\|- ( `' F " U. z ) = U_ y e. z ( `' F " y )
29	27 28	eqtrdi	\|- ( x = U. z -> ( `' F " x ) = U_ y e. z ( `' F " y ) )
30	29	eleq1d	\|- ( x = U. z -> ( ( `' F " x ) e. J <-> U_ y e. z ( `' F " y ) e. J ) )
31	30	imbi2d	\|- ( x = U. z -> ( ( A. y e. B ( `' F " y ) e. J -> ( `' F " x ) e. J ) <-> ( A. y e. B ( `' F " y ) e. J -> U_ y e. z ( `' F " y ) e. J ) ) )
32	26 31	syl5ibrcom	\|- ( ( ph /\ z C_ B ) -> ( x = U. z -> ( A. y e. B ( `' F " y ) e. J -> ( `' F " x ) e. J ) ) )
33	32	expimpd	\|- ( ph -> ( ( z C_ B /\ x = U. z ) -> ( A. y e. B ( `' F " y ) e. J -> ( `' F " x ) e. J ) ) )
34	33	exlimdv	\|- ( ph -> ( E. z ( z C_ B /\ x = U. z ) -> ( A. y e. B ( `' F " y ) e. J -> ( `' F " x ) e. J ) ) )
35	19 34	sylbid	\|- ( ph -> ( x e. K -> ( A. y e. B ( `' F " y ) e. J -> ( `' F " x ) e. J ) ) )
36	35	imp	\|- ( ( ph /\ x e. K ) -> ( A. y e. B ( `' F " y ) e. J -> ( `' F " x ) e. J ) )
37	36	ralrimdva	\|- ( ph -> ( A. y e. B ( `' F " y ) e. J -> A. x e. K ( `' F " x ) e. J ) )
38		imaeq2	\|- ( x = y -> ( `' F " x ) = ( `' F " y ) )
39	38	eleq1d	\|- ( x = y -> ( ( `' F " x ) e. J <-> ( `' F " y ) e. J ) )
40	39	cbvralvw	\|- ( A. x e. K ( `' F " x ) e. J <-> A. y e. K ( `' F " y ) e. J )
41	37 40	imbitrdi	\|- ( ph -> ( A. y e. B ( `' F " y ) e. J -> A. y e. K ( `' F " y ) e. J ) )
42	15 41	impbid	\|- ( ph -> ( A. y e. K ( `' F " y ) e. J <-> A. y e. B ( `' F " y ) e. J ) )
43	42	anbi2d	\|- ( ph -> ( ( F : X --> Y /\ A. y e. K ( `' F " y ) e. J ) <-> ( F : X --> Y /\ A. y e. B ( `' F " y ) e. J ) ) )
44	5 43	bitrd	\|- ( ph -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. B ( `' F " y ) e. J ) ) )

Metamath Proof Explorer

Theorem tgcn

Proof