Theorem cnconst 7777

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 3641	. . . . 5 |- ((F:X-->{B} /\ {B} (_ Y) -> F:X-->Y)
2		simprr 417	. . . . 5 |- ((J e. Top /\ (B e. Y /\ F:X-->{B})) -> F:X-->{B})
3		snssi 2470	. . . . . 6 |- (B e. Y -> {B} (_ Y)
4	3	ad2antrl 408	. . . . 5 |- ((J e. Top /\ (B e. Y /\ F:X-->{B})) -> {B} (_ Y)
5	1, 2, 4	sylanc 473	. . . 4 |- ((J e. Top /\ (B e. Y /\ F:X-->{B})) -> F:X-->Y)
6		eleq1 1537	. . . . . . . . . . . . . . . . . 18 |- ((/) = (`'F"x) -> ((/) e. J <-> (`'F"x) e. J))
7		0opnt 7602	. . . . . . . . . . . . . . . . . 18 |- (J e. Top -> (/) e. J)
8	6, 7	syl5cbi 209	. . . . . . . . . . . . . . . . 17 |- (J e. Top -> ((/) = (`'F"x) -> (`'F"x) e. J))
9		eqcom 1480	. . . . . . . . . . . . . . . . 17 |- ((`'F"x) = (/) <-> (/) = (`'F"x))
10	8, 9	syl5ib 206	. . . . . . . . . . . . . . . 16 |- (J e. Top -> ((`'F"x) = (/) -> (`'F"x) e. J))
11		0ima 3427	. . . . . . . . . . . . . . . . 17 |- ((/)"x) = (/)
12		eqtrt 1495	. . . . . . . . . . . . . . . . 17 |- (((`'F"x) = ((/)"x) /\ ((/)"x) = (/)) -> (`'F"x) = (/))
13	11, 12	mpan2 698	. . . . . . . . . . . . . . . 16 |- ((`'F"x) = ((/)"x) -> (`'F"x) = (/))
14	10, 13	syl5 21	. . . . . . . . . . . . . . 15 |- (J e. Top -> ((`'F"x) = ((/)"x) -> (`'F"x) e. J))
15		imaeq1 3407	. . . . . . . . . . . . . . 15 |- (`'F = (/) -> (`'F"x) = ((/)"x))
16	14, 15	syl5 21	. . . . . . . . . . . . . 14 |- (J e. Top -> (`'F = (/) -> (`'F"x) e. J))
17		cnv0 3452	. . . . . . . . . . . . . . 15 |- `'(/) = (/)
18		eqtrt 1495	. . . . . . . . . . . . . . 15 |- ((`'F = `'(/) /\ `'(/) = (/)) -> `'F = (/))
19	17, 18	mpan2 698	. . . . . . . . . . . . . 14 |- (`'F = `'(/) -> `'F = (/))
20	16, 19	syl5 21	. . . . . . . . . . . . 13 |- (J e. Top -> (`'F = `'(/) -> (`'F"x) e. J))
21		cnveq 3298	. . . . . . . . . . . . 13 |- (F = (/) -> `'F = `'(/))
22	20, 21	syl5 21	. . . . . . . . . . . 12 |- (J e. Top -> (F = (/) -> (`'F"x) e. J))
23	22	3ad2ant1 802	. . . . . . . . . . 11 |- ((J e. Top /\ F:X-->{B} /\ B e. x) -> (F = (/) -> (`'F"x) e. J))
24		imassrn 3421	. . . . . . . . . . . . . . . . . . . 20 |- (`'F"x) (_ ran `' F
25	24	a1i 8	. . . . . . . . . . . . . . . . . . 19 |- (F:X-->{B} -> (`'F"x) (_ ran `' F)
26		fdm 3637	. . . . . . . . . . . . . . . . . . . 20 |- (F:X-->{B} -> dom F = X)
27		dfdm4 3311	. . . . . . . . . . . . . . . . . . . 20 |- dom F = ran `' F
28	26, 27	syl5eqr 1524	. . . . . . . . . . . . . . . . . . 19 |- (F:X-->{B} -> ran `' F = X)
29	25, 28	sseqtrd 2100	. . . . . . . . . . . . . . . . . 18 |- (F:X-->{B} -> (`'F"x) (_ X)
30	29	3ad2ant1 802	. . . . . . . . . . . . . . . . 17 |- ((F:X-->{B} /\ B e. x /\ -. F = (/)) -> (`'F"x) (_ X)
31	26	eqcomd 1483	. . . . . . . . . . . . . . . . . . . . 21 |- (F:X-->{B} -> X = dom F)
32	31	adantr 391	. . . . . . . . . . . . . . . . . . . 20 |- ((F:X-->{B} /\ -. F = (/)) -> X = dom F)
33		imadmrn 3420	. . . . . . . . . . . . . . . . . . . . . 22 |- (`'F"dom `' F) = ran `' F
34	27, 33	eqtr4 1501	. . . . . . . . . . . . . . . . . . . . 21 |- dom F = (`'F"dom `' F)
35	34	a1i 8	. . . . . . . . . . . . . . . . . . . 20 |- ((F:X-->{B} /\ -. F = (/)) -> dom F = (`'F"dom `' F))
36		foconst 3689	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((F:X-->{B} /\ F =/= (/)) -> F:X-onto->{B})
37		df-ne 1590	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (F =/= (/) <-> -. F = (/))
38	36, 37	sylan2br 455	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((F:X-->{B} /\ -. F = (/)) -> F:X-onto->{B})
39		forn 3680	. . . . . . . . . . . . . . . . . . . . . . 23 |- (F:X-onto->{B} -> ran F = {B})
40	38, 39	syl 10	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F:X-->{B} /\ -. F = (/)) -> ran F = {B})
41		df-rn 3195	. . . . . . . . . . . . . . . . . . . . . 22 |- ran F = dom `' F
42	40, 41	syl5eqr 1524	. . . . . . . . . . . . . . . . . . . . 21 |- ((F:X-->{B} /\ -. F = (/)) -> dom `' F = {B})
43	42	imaeq2d 3410	. . . . . . . . . . . . . . . . . . . 20 |- ((F:X-->{B} /\ -. F = (/)) -> (`'F"dom `' F) = (`'F"{B}))
44	32, 35, 43	3eqtrd 1514	. . . . . . . . . . . . . . . . . . 19 |- ((F:X-->{B} /\ -. F = (/)) -> X = (`'F"{B}))
45	44	3adant2 800	. . . . . . . . . . . . . . . . . 18 |- ((F:X-->{B} /\ B e. x /\ -. F = (/)) -> X = (`'F"{B}))
46		snssi 2470	. . . . . . . . . . . . . . . . . . . 20 |- (B e. x -> {B} (_ x)
47		imass2 3439	. . . . . . . . . . . . . . . . . . . 20 |- ({B} (_ x -> (`'F"{B}) (_ (`'F"x))
48	46, 47	syl 10	. . . . . . . . . . . . . . . . . . 19 |- (B e. x -> (`'F"{B}) (_ (`'F"x))
49	48	3ad2ant2 803	. . . . . . . . . . . . . . . . . 18 |- ((F:X-->{B} /\ B e. x /\ -. F = (/)) -> (`'F"{B}) (_ (`'F"x))
50	45, 49	eqsstrd 2098	. . . . . . . . . . . . . . . . 17 |- ((F:X-->{B} /\ B e. x /\ -. F = (/)) -> X (_ (`'F"x))
51	30, 50	eqssd 2082	. . . . . . . . . . . . . . . 16 |- ((F:X-->{B} /\ B e. x /\ -. F = (/)) -> (`'F"x) = X)
52	51	3exp 834	. . . . . . . . . . . . . . 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 848	. . . . . . . . . . . . 13 |- (((J e. Top /\ F:X-->{B} /\ B e. x) /\ -. F = (/)) -> (`'F"x) = X)
55		cnconst.1	. . . . . . . . . . . . . . . 16 |- X = U.J
56	55	topopn 7603	. . . . . . . . . . . . . . 15 |- (J e. Top -> X e. J)
57	56	3ad2ant1 802	. . . . . . . . . . . . . 14 |- ((J e. Top /\ F:X-->{B} /\ B e. x) -> X e. J)
58	57	adantr 391	. . . . . . . . . . . . 13 |- (((J e. Top /\ F:X-->{B} /\ B e. x) /\ -. F = (/)) -> X e. J)
59	54, 58	eqeltrd 1551	. . . . . . . . . . . 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 834	. . . . . . . . 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 3655	. . . . . . . . . . 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 2445	. . . . . . . . . . . . 13 |- ((x i^i {B}) = (/) <-> -. B e. x)
68	67	biimpr 152	. . . . . . . . . . . 12 |- (-. B e. x -> (x i^i {B}) = (/))
69		incom 2211	. . . . . . . . . . . 12 |- ({B} i^i x) = (x i^i {B})
70	68, 69	syl5eq 1522	. . . . . . . . . . 11 |- (-. B e. x -> ({B} i^i x) = (/))
71	65, 66, 70	syl2an 456	. . . . . . . . . 10 |- (((B e. Y /\ F:X-->{B}) /\ -. B e. x) -> (`'F"x) = (/))
72	71	adantll 394	. . . . . . . . 9 |- (((J e. Top /\ (B e. Y /\ F:X-->{B})) /\ -. B e. x) -> (`'F"x) = (/))
73	7	ad2antrr 406	. . . . . . . . 9 |- (((J e. Top /\ (B e. Y /\ F:X-->{B})) /\ -. B e. x) -> (/) e. J)
74	72, 73	eqeltrd 1551	. . . . . . . 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 1716	. . . 4 |- ((J e. Top /\ (B e. Y /\ F:X-->