Theorem cnconst 7780

Description: A constant function is continuous. (Contributed by FL, 25-Jan-2007.)

Hypotheses

Ref	Expression
cnconst.1	|- X = U.J
cnconst.2	|- Y = U.K

Assertion

Ref	Expression
cnconst	|- (((J e. Top /\ K e. Top) /\ (B e. Y /\ F:X-->{B})) -> F e. (J Cn K))

Proof of Theorem cnconst

Step	Hyp	Ref	Expression
1		fss 3635	. . . . 5 |- ((F:X-->{B} /\ {B} (_ Y) -> F:X-->Y)
2		simprr 415	. . . . 5 |- ((J e. Top /\ (B e. Y /\ F:X-->{B})) -> F:X-->{B})
3		snssi 2466	. . . . . 6 |- (B e. Y -> {B} (_ Y)
4	3	ad2antrl 406	. . . . 5 |- ((J e. Top /\ (B e. Y /\ F:X-->{B})) -> {B} (_ Y)
5	1, 2, 4	sylanc 471	. . . 4 |- ((J e. Top /\ (B e. Y /\ F:X-->{B})) -> F:X-->Y)
6		eleq1 1534	. . . . . . . . . . . . . . . . . 18 |- ((/) = (`'F"x) -> ((/) e. J <-> (`'F"x) e. J))
7		0opnt 7601	. . . . . . . . . . . . . . . . . 18 |- (J e. Top -> (/) e. J)
8	6, 7	syl5cbi 209	. . . . . . . . . . . . . . . . 17 |- (J e. Top -> ((/) = (`'F"x) -> (`'F"x) e. J))
9		eqcom 1477	. . . . . . . . . . . . . . . . 17 |- ((`'F"x) = (/) <-> (/) = (`'F"x))
10	8, 9	syl5ib 206	. . . . . . . . . . . . . . . 16 |- (J e. Top -> ((`'F"x) = (/) -> (`'F"x) e. J))
11		0ima 3421	. . . . . . . . . . . . . . . . 17 |- ((/)"x) = (/)
12		eqtrt 1492	. . . . . . . . . . . . . . . . 17 |- (((`'F"x) = ((/)"x) /\ ((/)"x) = (/)) -> (`'F"x) = (/))
13	11, 12	mpan2 696	. . . . . . . . . . . . . . . 16 |- ((`'F"x) = ((/)"x) -> (`'F"x) = (/))
14	10, 13	syl5 21	. . . . . . . . . . . . . . 15 |- (J e. Top -> ((`'F"x) = ((/)"x) -> (`'F"x) e. J))
15		imaeq1 3401	. . . . . . . . . . . . . . 15 |- (`'F = (/) -> (`'F"x) = ((/)"x))
16	14, 15	syl5 21	. . . . . . . . . . . . . 14 |- (J e. Top -> (`'F = (/) -> (`'F"x) e. J))
17		cnv0 3446	. . . . . . . . . . . . . . 15 |- `'(/) = (/)
18		eqtrt 1492	. . . . . . . . . . . . . . 15 |- ((`'F = `'(/) /\ `'(/) = (/)) -> `'F = (/))
19	17, 18	mpan2 696	. . . . . . . . . . . . . 14 |- (`'F = `'(/) -> `'F = (/))
20	16, 19	syl5 21	. . . . . . . . . . . . 13 |- (J e. Top -> (`'F = `'(/) -> (`'F"x) e. J))
21		cnveq 3292	. . . . . . . . . . . . 13 |- (F = (/) -> `'F = `'(/))
22	20, 21	syl5 21	. . . . . . . . . . . 12 |- (J e. Top -> (F = (/) -> (`'F"x) e. J))
23	22	3ad2ant1 800	. . . . . . . . . . 11 |- ((J e. Top /\ F:X-->{B} /\ B e. x) -> (F = (/) -> (`'F"x) e. J))
24		imassrn 3415	. . . . . . . . . . . . . . . . . . . 20 |- (`'F"x) (_ ran `' F
25	24	a1i 8	. . . . . . . . . . . . . . . . . . 19 |- (F:X-->{B} -> (`'F"x) (_ ran `' F)
26		fdm 3631	. . . . . . . . . . . . . . . . . . . 20 |- (F:X-->{B} -> dom F = X)
27		dfdm4 3305	. . . . . . . . . . . . . . . . . . . 20 |- dom F = ran `' F
28	26, 27	syl5eqr 1521	. . . . . . . . . . . . . . . . . . 19 |- (F:X-->{B} -> ran `' F = X)
29	25, 28	sseqtrd 2097	. . . . . . . . . . . . . . . . . 18 |- (F:X-->{B} -> (`'F"x) (_ X)
30	29	3ad2ant1 800	. . . . . . . . . . . . . . . . 17 |- ((F:X-->{B} /\ B e. x /\ -. F = (/)) -> (`'F"x) (_ X)
31	26	eqcomd 1480	. . . . . . . . . . . . . . . . . . . . 21 |- (F:X-->{B} -> X = dom F)
32	31	adantr 389	. . . . . . . . . . . . . . . . . . . 20 |- ((F:X-->{B} /\ -. F = (/)) -> X = dom F)
33		imadmrn 3414	. . . . . . . . . . . . . . . . . . . . . 22 |- (`'F"dom `' F) = ran `' F
34	27, 33	eqtr4 1498	. . . . . . . . . . . . . . . . . . . . 21 |- dom F = (`'F"dom `' F)
35	34	a1i 8	. . . . . . . . . . . . . . . . . . . 20 |- ((F:X-->{B} /\ -. F = (/)) -> dom F = (`'F"dom `' F))
36		foconst 3683	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((F:X-->{B} /\ F =/= (/)) -> F:X-onto->{B})
37		df-ne 1587	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (F =/= (/) <-> -. F = (/))
38	36, 37	sylan2br 453	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((F:X-->{B} /\ -. F = (/)) -> F:X-onto->{B})
39		forn 3674	. . . . . . . . . . . . . . . . . . . . . . 23 |- (F:X-onto->{B} -> ran F = {B})
40	38, 39	syl 10	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F:X-->{B} /\ -. F = (/)) -> ran F = {B})
41		df-rn 3189	. . . . . . . . . . . . . . . . . . . . . 22 |- ran F = dom `' F
42	40, 41	syl5eqr 1521	. . . . . . . . . . . . . . . . . . . . 21 |- ((F:X-->{B} /\ -. F = (/)) -> dom `' F = {B})
43	42	imaeq2d 3404	. . . . . . . . . . . . . . . . . . . 20 |- ((F:X-->{B} /\ -. F = (/)) -> (`'F"dom `' F) = (`'F"{B}))
44	32, 35, 43	3eqtrd 1511	. . . . . . . . . . . . . . . . . . 19 |- ((F:X-->{B} /\ -. F = (/)) -> X = (`'F"{B}))
45	44	3adant2 798	. . . . . . . . . . . . . . . . . 18 |- ((F:X-->{B} /\ B e. x /\ -. F = (/)) -> X = (`'F"{B}))
46		snssi 2466	. . . . . . . . . . . . . . . . . . . 20 |- (B e. x -> {B} (_ x)
47		imass2 3433	. . . . . . . . . . . . . . . . . . . 20 |- ({B} (_ x -> (`'F"{B}) (_ (`'F"x))
48	46, 47	syl 10	. . . . . . . . . . . . . . . . . . 19 |- (B e. x -> (`'F"{B}) (_ (`'F"x))
49	48	3ad2ant2 801	. . . . . . . . . . . . . . . . . 18 |- ((F:X-->{B} /\ B e. x /\ -. F = (/)) -> (`'F"{B}) (_ (`'F"x))
50	45, 49	eqsstrd 2095	. . . . . . . . . . . . . . . . 17 |- ((F:X-->{B} /\ B e. x /\ -. F = (/)) -> X (_ (`'F"x))
51	30, 50	eqssd 2079	. . . . . . . . . . . . . . . 16 |- ((F:X-->{B} /\ B e. x /\ -. F = (/)) -> (`'F"x) = X)
52	51	3exp 832	. . . . . . . . . . . . . . 15 |- (F:X-->{B} -> (B e. x -> (-. F = (/) -> (`'F"x) = X)))
53	52	a1i 8	. . . . . . . . . . . . . 14 |- (J e. Top -> (F:X-->{B} -> (B e. x -> (-. F = (/) -> (`'F"x) = X))))
54	53	3imp1 846	. . . . . . . . . . . . 13 |- (((J e. Top /\ F:X-->{B} /\ B e. x) /\ -. F = (/)) -> (`'F"x) = X)
55		cnconst.1	. . . . . . . . . . . . . . . 16 |- X = U.J
56	55	topopn 7602	. . . . . . . . . . . . . . 15 |- (J e. Top -> X e. J)
57	56	3ad2ant1 800	. . . . . . . . . . . . . 14 |- ((J e. Top /\ F:X-->{B} /\ B e. x) -> X e. J)
58	57	adantr 389	. . . . . . . . . . . . 13 |- (((J e. Top /\ F:X-->{B} /\ B e. x) /\ -. F = (/)) -> X e. J)
59	54, 58	eqeltrd 1548	. . . . . . . . . . . 12 |- (((J e. Top /\ F:X-->{B} /\ B e. x) /\ -. F = (/)) -> (`'F"x) e. J)
60	59	ex 373	. . . . . . . . . . 11 |- ((J e. Top /\ F:X-->{B} /\ B e. x) -> (-. F = (/) -> (`'F"x) e. J))
61	23, 60	pm2.61d 127	. . . . . . . . . 10 |- ((J e. Top /\ F:X-->{B} /\ B e. x) -> (`'F"x) e. J)
62	61	3exp 832	. . . . . . . . 9 |- (J e. Top -> (F:X-->{B} -> (B e. x -> (`'F"x) e. J)))
63	62	a1d 12	. . . . . . . 8 |- (J e. Top -> (B e. Y -> (F:X-->{B} -> (B e. x -> (`'F"x) e. J))))
64	63	imp32 363	. . . . . . 7 |- ((J e. Top /\ (B e. Y /\ F:X-->{B})) -> (B e. x -> (`'F"x) e. J))
65		fimacnvdisj 3649	. . . . . . . . . . 11 |- ((F:X-->{B} /\ ({B} i^i x) = (/)) -> (`'F"x) = (/))
66		pm3.27 323	. . . . . . . . . . 11 |- ((B e. Y /\ F:X-->{B}) -> F:X-->{B})
67		disjsn 2441	. . . . . . . . . . . . 13 |- ((x i^i {B}) = (/) <-> -. B e. x)
68	67	biimpr 152	. . . . . . . . . . . 12 |- (-. B e. x -> (x i^i {B}) = (/))
69		incom 2208	. . . . . . . . . . . 12 |- ({B} i^i x) = (x i^i {B})
70	68, 69	syl5eq 1519	. . . . . . . . . . 11 |- (-. B e. x -> ({B} i^i x) = (/))
71	65, 66, 70	syl2an 454	. . . . . . . . . 10 |- (((B e. Y /\ F:X-->{B}) /\ -. B e. x) -> (`'F"x) = (/))
72	71	adantll 392	. . . . . . . . 9 |- (((J e. Top /\ (B e. Y /\ F:X-->{B})) /\ -. B e. x) -> (`'F"x) = (/))
73	7	ad2antrr 404	. . . . . . . . 9 |- (((J e. Top /\ (B e. Y /\ F:X-->{B})) /\ -. B e. x) -> (/) e. J)
74	72, 73	eqeltrd 1548	. . . . . . . 8 |- (((J e. Top /\ (B e. Y /\ F:X-->{B})) /\ -. B e. x) -> (`'F"x) e. J)
75	74	ex 373	. . . . . . 7 |- ((J e. Top /\ (B e. Y /\ F:X-->{B})) -> (-. B e. x -> (`'F"x) e. J))
76	64, 75	pm2.61d 127	. . . . . 6 |- ((J e. Top /\ (B e. Y /\ F:X-->{B})) -> (`'F"x) e. J)
77	76	a1d 12	. . . . 5 |- ((J e. Top /\ (B e. Y /\ F:X-->{B})) -> (x e. K -> (`'F"x) e. J))
78	77	r19.21aiv 1713	. . . 4 |- ((J e. Top /\ (B e. Y /\ F:X-->