Theorem tgcn 12219

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.)

Hypotheses

Ref	Expression
tgcn.1	|- ( ph -> J e. (TopOn ` X ) )
tgcn.3	|- ( ph -> K = ( topGen ` B ) )
tgcn.4	|- ( ph -> K e. (TopOn ` Y ) )

Assertion

Ref	Expression
tgcn	|- ( ph -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. B ( `' F " y ) e. J ) ) )

Distinct variable groups:   y, B   y, F   y, J   y, K   y, X   y, Y

Allowed substitution hint:   ph( y)

Proof of Theorem tgcn

Dummy variables x z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		tgcn.1	. . 3 |- ( ph -> J e. (TopOn ` X ) )
2		tgcn.4	. . 3 |- ( ph -> K e. (TopOn ` Y ) )
3		iscn 12208	. . 3 |- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. K ( `' F " y ) e. J ) ) )
4	1, 2, 3	syl2anc 406	. 2 |- ( ph -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. K ( `' F " y ) e. J ) ) )
5		tgcn.3	. . . . . . . . 9 |- ( ph -> K = ( topGen ` B ) )
6		topontop 12024	. . . . . . . . . 10 |- ( K e. (TopOn ` Y ) -> K e. Top )
7	2, 6	syl 14	. . . . . . . . 9 |- ( ph -> K e. Top )
8	5, 7	eqeltrrd 2192	. . . . . . . 8 |- ( ph -> ( topGen ` B ) e. Top )
9		tgclb 12077	. . . . . . . 8 |- ( B e. TopBases <-> ( topGen ` B ) e. Top )
10	8, 9	sylibr 133	. . . . . . 7 |- ( ph -> B e. TopBases )
11		bastg 12073	. . . . . . 7 |- ( B e. TopBases -> B C_ ( topGen ` B ) )
12	10, 11	syl 14	. . . . . 6 |- ( ph -> B C_ ( topGen ` B ) )
13	12, 5	sseqtr4d 3102	. . . . 5 |- ( ph -> B C_ K )
14		ssralv 3127	. . . . 5 |- ( B C_ K -> ( A. y e. K ( `' F " y ) e. J -> A. y e. B ( `' F " y ) e. J ) )
15	13, 14	syl 14	. . . 4 |- ( ph -> ( A. y e. K ( `' F " y ) e. J -> A. y e. B ( `' F " y ) e. J ) )
16	5	eleq2d 2184	. . . . . . . . 9 |- ( ph -> ( x e. K <-> x e. ( topGen ` B ) ) )
17		eltg3 12069	. . . . . . . . . 10 |- ( B e. TopBases -> ( x e. ( topGen ` B ) <-> E. z ( z C_ B /\ x = U. z ) ) )
18	10, 17	syl 14	. . . . . . . . 9 |- ( ph -> ( x e. ( topGen ` B ) <-> E. z ( z C_ B /\ x = U. z ) ) )
19	16, 18	bitrd 187	. . . . . . . 8 |- ( ph -> ( x e. K <-> E. z ( z C_ B /\ x = U. z ) ) )
20		ssralv 3127	. . . . . . . . . . . 12 |- ( z C_ B -> ( A. y e. B ( `' F " y ) e. J -> A. y e. z ( `' F " y ) e. J ) )
21		topontop 12024	. . . . . . . . . . . . . 14 |- ( J e. (TopOn ` X ) -> J e. Top )
22	1, 21	syl 14	. . . . . . . . . . . . 13 |- ( ph -> J e. Top )
23		iunopn 12012	. . . . . . . . . . . . . 14 |- ( ( J e. Top /\ A. y e. z ( `' F " y ) e. J ) -> U_ y e. z ( `' F " y ) e. J )
24	23	ex 114	. . . . . . . . . . . . 13 |- ( J e. Top -> ( A. y e. z ( `' F " y ) e. J -> U_ y e. z ( `' F " y ) e. J ) )
25	22, 24	syl 14	. . . . . . . . . . . 12 |- ( ph -> ( A. y e. z ( `' F " y ) e. J -> U_ y e. z ( `' F " y ) e. J ) )
26	20, 25	sylan9r 405	. . . . . . . . . . 11 |- ( ( ph /\ z C_ B ) -> ( A. y e. B ( `' F " y ) e. J -> U_ y e. z ( `' F " y ) e. J ) )
27		imaeq2 4835	. . . . . . . . . . . . . 14 |- ( x = U. z -> ( `' F " x ) = ( `' F " U. z ) )
28		imauni 5616	. . . . . . . . . . . . . 14 |- ( `' F " U. z ) = U_ y e. z ( `' F " y )
29	27, 28	syl6eq 2163	. . . . . . . . . . . . 13 |- ( x = U. z -> ( `' F " x ) = U_ y e. z ( `' F " y ) )
30	29	eleq1d 2183	. . . . . . . . . . . 12 |- ( x = U. z -> ( ( `' F " x ) e. J <-> U_ y e. z ( `' F " y ) e. J ) )
31	30	imbi2d 229	. . . . . . . . . . 11 |- ( 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 156	. . . . . . . . . 10 |- ( ( ph /\ z C_ B ) -> ( x = U. z -> ( A. y e. B ( `' F " y ) e. J -> ( `' F " x ) e. J ) ) )
33	32	expimpd 358	. . . . . . . . 9 |- ( ph -> ( ( z C_ B /\ x = U. z ) -> ( A. y e. B ( `' F " y ) e. J -> ( `' F " x ) e. J ) ) )
34	33	exlimdv 1773	. . . . . . . 8 |- ( 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 149	. . . . . . 7 |- ( ph -> ( x e. K -> ( A. y e. B ( `' F " y ) e. J -> ( `' F " x ) e. J ) ) )
36	35	imp 123	. . . . . 6 |- ( ( ph /\ x e. K ) -> ( A. y e. B ( `' F " y ) e. J -> ( `' F " x ) e. J ) )
37	36	ralrimdva 2486	. . . . 5 |- ( ph -> ( A. y e. B ( `' F " y ) e. J -> A. x e. K ( `' F " x ) e. J ) )
38		imaeq2 4835	. . . . . . 7 |- ( x = y -> ( `' F " x ) = ( `' F " y ) )
39	38	eleq1d 2183	. . . . . 6 |- ( x = y -> ( ( `' F " x ) e. J <-> ( `' F " y ) e. J ) )
40	39	cbvralv 2628	. . . . 5 |- ( A. x e. K ( `' F " x ) e. J <-> A. y e. K ( `' F " y ) e. J )
41	37, 40	syl6ib 160	. . . 4 |- ( ph -> ( A. y e. B ( `' F " y ) e. J -> A. y e. K ( `' F " y ) e. J ) )
42	15, 41	impbid 128	. . 3 |- ( ph -> ( A. y e. K ( `' F " y ) e. J <-> A. y e. B ( `' F " y ) e. J ) )
43	42	anbi2d 457	. 2 |- ( ph -> ( ( F : X --> Y /\ A. y e. K ( `' F " y ) e. J ) <-> ( F : X --> Y /\ A. y e. B ( `' F " y ) e. J ) ) )
44	4, 43	bitrd 187	1 |- ( ph -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. B ( `' F " y ) e. J ) ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   = wceq 1314   E.wex 1451   e. wcel 1463   A.wral 2390   C_ wss 3037   U.cuni 3702   U_ciun 3779   `'ccnv 4498   "cima 4502   -->wf 5077   ` cfv 5081  (class class class)co 5728   topGenctg 11978   Topctop 12007  TopOnctopon 12020   TopBasesctb 12052   Cn ccn 12197

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4006  ax-pow 4058  ax-pr 4091  ax-un 4315  ax-setind 4412

This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-fal 1320  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2244  df-ne 2283  df-ral 2395  df-rex 2396  df-rab 2399  df-v 2659  df-sbc 2879  df-csb 2972  df-dif 3039  df-un 3041  df-in 3043  df-ss 3050  df-nul 3330  df-pw 3478  df-sn 3499  df-pr 3500  df-op 3502  df-uni 3703  df-iun 3781  df-br 3896  df-opab 3950  df-mpt 3951  df-id 4175  df-xp 4505  df-rel 4506  df-cnv 4507  df-co 4508  df-dm 4509  df-rn 4510  df-res 4511  df-ima 4512  df-iota 5046  df-fun 5083  df-fn 5084  df-f 5085  df-fv 5089  df-ov 5731  df-oprab 5732  df-mpo 5733  df-1st 5992  df-2nd 5993  df-map 6498  df-topgen 11984  df-top 12008  df-topon 12021  df-bases 12053  df-cn 12200

This theorem is referenced by:  txcnmpt  12284