Theorem cnconst 9057

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		simprr 451	. . . . 5 |- ((J e. Top /\ (B e. Y /\ F:X-->{B})) -> F:X-->{B})
2		snssi 3129	. . . . . 6 |- (B e. Y -> {B} C_ Y)
3	2	ad2antrl 442	. . . . 5 |- ((J e. Top /\ (B e. Y /\ F:X-->{B})) -> {B} C_ Y)
4		fss 4571	. . . . 5 |- ((F:X-->{B} /\ {B} C_ Y) -> F:X-->Y)
5	1, 3, 4	syl11anc 524	. . . 4 |- ((J e. Top /\ (B e. Y /\ F:X-->{B})) -> F:X-->Y)
6		eleq1 1957	. . . . . . . . . . . . . . . . . 18 |- ((/) = (`'F"x) -> ((/) e. J <-> (`'F"x) e. J))
7		0opn 8870	. . . . . . . . . . . . . . . . . 18 |- (J e. Top -> (/) e. J)
8	6, 7	syl5cbi 226	. . . . . . . . . . . . . . . . 17 |- (J e. Top -> ((/) = (`'F"x) -> (`'F"x) e. J))
9		eqcom 1886	. . . . . . . . . . . . . . . . 17 |- ((`'F"x) = (/) <-> (/) = (`'F"x))
10	8, 9	syl5ib 223	. . . . . . . . . . . . . . . 16 |- (J e. Top -> ((`'F"x) = (/) -> (`'F"x) e. J))
11		0ima 4284	. . . . . . . . . . . . . . . . 17 |- ((/)"x) = (/)
12		eqtr 1904	. . . . . . . . . . . . . . . . 17 |- (((`'F"x) = ((/)"x) /\ ((/)"x) = (/)) -> (`'F"x) = (/))
13	11, 12	mpan2 760	. . . . . . . . . . . . . . . 16 |- ((`'F"x) = ((/)"x) -> (`'F"x) = (/))
14	10, 13	syl5 20	. . . . . . . . . . . . . . 15 |- (J e. Top -> ((`'F"x) = ((/)"x) -> (`'F"x) e. J))
15		imaeq1 4259	. . . . . . . . . . . . . . 15 |- (`'F = (/) -> (`'F"x) = ((/)"x))
16	14, 15	syl5 20	. . . . . . . . . . . . . 14 |- (J e. Top -> (`'F = (/) -> (`'F"x) e. J))
17		cnv0 4319	. . . . . . . . . . . . . . 15 |- `'(/) = (/)
18		eqtr 1904	. . . . . . . . . . . . . . 15 |- ((`'F = `'(/) /\ `'(/) = (/)) -> `'F = (/))
19	17, 18	mpan2 760	. . . . . . . . . . . . . 14 |- (`'F = `'(/) -> `'F = (/))
20	16, 19	syl5 20	. . . . . . . . . . . . 13 |- (J e. Top -> (`'F = `'(/) -> (`'F"x) e. J))
21		cnveq 4135	. . . . . . . . . . . . 13 |- (F = (/) -> `'F = `'(/))
22	20, 21	syl5 20	. . . . . . . . . . . 12 |- (J e. Top -> (F = (/) -> (`'F"x) e. J))
23	22	3ad2ant1 897	. . . . . . . . . . 11 |- ((J e. Top /\ F:X-->{B} /\ B e. x) -> (F = (/) -> (`'F"x) e. J))
24		imassrn 4278	. . . . . . . . . . . . . . . . . . . 20 |- (`'F"x) C_ ran `' F
25	24	a1i 8	. . . . . . . . . . . . . . . . . . 19 |- (F:X-->{B} -> (`'F"x) C_ ran `' F)
26		fdm 4567	. . . . . . . . . . . . . . . . . . . 20 |- (F:X-->{B} -> dom F = X)
27		dfdm4 4151	. . . . . . . . . . . . . . . . . . . 20 |- dom F = ran `' F
28	26, 27	syl5eqr 1942	. . . . . . . . . . . . . . . . . . 19 |- (F:X-->{B} -> ran `' F = X)
29	25, 28	sseqtrd 2653	. . . . . . . . . . . . . . . . . 18 |- (F:X-->{B} -> (`'F"x) C_ X)
30	29	3ad2ant1 897	. . . . . . . . . . . . . . . . 17 |- ((F:X-->{B} /\ B e. x /\ -. F = (/)) -> (`'F"x) C_ X)
31	26	eqcomd 1889	. . . . . . . . . . . . . . . . . . . . 21 |- (F:X-->{B} -> X = dom F)
32	31	adantr 425	. . . . . . . . . . . . . . . . . . . 20 |- ((F:X-->{B} /\ -. F = (/)) -> X = dom F)
33		imadmrn 4277	. . . . . . . . . . . . . . . . . . . . . 22 |- (`'F"dom `' F) = ran `' F
34	27, 33	eqtr4i 1911	. . . . . . . . . . . . . . . . . . . . 21 |- dom F = (`'F"dom `' F)
35	34	a1i 8	. . . . . . . . . . . . . . . . . . . 20 |- ((F:X-->{B} /\ -. F = (/)) -> dom F = (`'F"dom `' F))
36		foconst 4629	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((F:X-->{B} /\ F =/= (/)) -> F:X-onto->{B})
37		df-ne 2019	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (F =/= (/) <-> -. F = (/))
38	36, 37	sylan2br 502	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((F:X-->{B} /\ -. F = (/)) -> F:X-onto->{B})
39		forn 4620	. . . . . . . . . . . . . . . . . . . . . . 23 |- (F:X-onto->{B} -> ran F = {B})
40	38, 39	syl 12	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F:X-->{B} /\ -. F = (/)) -> ran F = {B})
41		df-rn 4005	. . . . . . . . . . . . . . . . . . . . . 22 |- ran F = dom `' F
42	40, 41	syl5eqr 1942	. . . . . . . . . . . . . . . . . . . . 21 |- ((F:X-->{B} /\ -. F = (/)) -> dom `' F = {B})
43	42	imaeq2d 4264	. . . . . . . . . . . . . . . . . . . 20 |- ((F:X-->{B} /\ -. F = (/)) -> (`'F"dom `' F) = (`'F"{B}))
44	32, 35, 43	3eqtrd 1929	. . . . . . . . . . . . . . . . . . 19 |- ((F:X-->{B} /\ -. F = (/)) -> X = (`'F"{B}))
45	44	3adant2 895	. . . . . . . . . . . . . . . . . 18 |- ((F:X-->{B} /\ B e. x /\ -. F = (/)) -> X = (`'F"{B}))
46		snssi 3129	. . . . . . . . . . . . . . . . . . . 20 |- (B e. x -> {B} C_ x)
47		imass2 4299	. . . . . . . . . . . . . . . . . . . 20 |- ({B} C_ x -> (`'F"{B}) C_ (`'F"x))
48	46, 47	syl 12	. . . . . . . . . . . . . . . . . . 19 |- (B e. x -> (`'F"{B}) C_ (`'F"x))
49	48	3ad2ant2 898	. . . . . . . . . . . . . . . . . 18 |- ((F:X-->{B} /\ B e. x /\ -. F = (/)) -> (`'F"{B}) C_ (`'F"x))
50	45, 49	eqsstrd 2651	. . . . . . . . . . . . . . . . 17 |- ((F:X-->{B} /\ B e. x /\ -. F = (/)) -> X C_ (`'F"x))
51	30, 50	eqssd 2633	. . . . . . . . . . . . . . . 16 |- ((F:X-->{B} /\ B e. x /\ -. F = (/)) -> (`'F"x) = X)
52	51	3exp 1066	. . . . . . . . . . . . . . 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 1081	. . . . . . . . . . . . 13 |- (((J e. Top /\ F:X-->{B} /\ B e. x) /\ -. F = (/)) -> (`'F"x) = X)
55		cnconst.1	. . . . . . . . . . . . . . . 16 |- X = U.J
56	55	topopn 8871	. . . . . . . . . . . . . . 15 |- (J e. Top -> X e. J)
57	56	3ad2ant1 897	. . . . . . . . . . . . . 14 |- ((J e. Top /\ F:X-->{B} /\ B e. x) -> X e. J)
58	57	adantr 425	. . . . . . . . . . . . 13 |- (((J e. Top /\ F:X-->{B} /\ B e. x) /\ -. F = (/)) -> X e. J)
59	54, 58	eqeltrd 1971	. . . . . . . . . . . 12 |- (((J e. Top /\ F:X-->{B} /\ B e. x) /\ -. F = (/)) -> (`'F"x) e. J)
60	59	ex 402	. . . . . . . . . . 11 |- ((J e. Top /\ F:X-->{B} /\ B e. x) -> (-. F = (/) -> (`'F"x) e. J))
61	23, 60	pm2.61d 141	. . . . . . . . . 10 |- ((J e. Top /\ F:X-->{B} /\ B e. x) -> (`'F"x) e. J)
62	61	3exp 1066	. . . . . . . . 9 |- (J e. Top -> (F:X-->{B} -> (B e. x -> (`'F"x) e. J)))
63	62	a1d 15	. . . . . . . 8 |- (J e. Top -> (B e. Y -> (F:X-->{B} -> (B e. x -> (`'F"x) e. J))))
64	63	imp32 390	. . . . . . 7 |- ((J e. Top /\ (B e. Y /\ F:X-->{B})) -> (B e. x -> (`'F"x) e. J))
65		fimacnvdisj 4590	. . . . . . . . . . 11 |- ((F:X-->{B} /\ ({B} i^i x) = (/)) -> (`'F"x) = (/))
66		simpr 350	. . . . . . . . . . 11 |- ((B e. Y /\ F:X-->{B}) -> F:X-->{B})
67		disjsn 3089	. . . . . . . . . . . . 13 |- ((x i^i {B}) = (/) <-> -. B e. x)
68	67	biimpri 169	. . . . . . . . . . . 12 |- (-. B e. x -> (x i^i {B}) = (/))
69		incom 2787	. . . . . . . . . . . 12 |- ({B} i^i x) = (x i^i {B})
70	68, 69	syl5eq 1940	. . . . . . . . . . 11 |- (-. B e. x -> ({B} i^i x) = (/))
71	65, 66, 70	syl2an 503	. . . . . . . . . 10 |- (((B e. Y /\ F:X-->{B}) /\ -. B e. x) -> (`'F"x) = (/))
72	71	adantll 428	. . . . . . . . 9 |- (((J e. Top /\ (B e. Y /\ F:X-->{B})) /\ -. B e. x) -> (`'F"x) = (/))
73	7	ad2antrr 440	. . . . . . . . 9 |- (((J e. Top /\ (B e. Y /\ F:X-->{B})) /\ -. B e. x) -> (/) e. J)
74	72, 73	eqeltrd 1971	. . . . . . . 8 |- (((J e. Top /\ (B e. Y /\ F:X-->{B})) /\ -. B e. x) -> (`'F"x) e. J)
75	74	ex 402	. . . . . . 7 |- ((J e. Top /\ (B e. Y /\ F:X-->{B})) -> (-. B e. x -> (`'F"x) e. J))
76	64, 75	pm2.61d 141	. . . . . 6 |- ((J e. Top /\ (B e. Y /\ F:X-->{B})) -> (`'F"x) e. J)
77	76	a1d 15	. . . . 5 |- ((J e. Top /\ (B e. Y /\ F:X-->{B})) -> (x e. K -> (`'F"x) e. J))
78	77	r19.21aiv 2175	. . . 4 |- ((J e. Top /\ (B e. Y /\ F:X-->{B})) -> A.x e. K (`'F"x) e. J)
79	5, 78	jca 310	. . 3 |- ((J e. Top /\ (B e. Y /\ F:X-->{B})) -> (F:X-->Y /\ A.x e. K (`'F"x) e. J))
80	79	adantlr 429	. 2 |- (((J e. Top /\ K e. Top) /\ (B e. Y /\ F:X-->{B})) -> (F:X-->Y /\ A.x e. K (`'F"x) e. J))
81		cnconst.2	. . . 4 |- Y = U.K
82	55, 81	iscn 9034	. . 3 |- ((J e. Top /\ K e. Top) -> (F e. (J Cn K) <-> (F:X-->Y /\ A.x e. K (`'F"x) e. J)))
83	82	adantr 425	. 2 |- (((J e. Top /\ K e. Top) /\ (B e. Y /\ F:X-->{B})) -> (F e. (J Cn K) <-> (F:X-->Y /\ A.x e. K (`'F"x) e. J)))
84	80, 83	mpbird 213	1 |- (((J e. Top /\ K e. Top) /\ (B e. Y /\ F:X-->{B})) -> F e. (J Cn K))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300   =/= wne 2017  A.wral 2105   i^i cin 2592   C_ wss 2593  (/)c0 2875  {csn 3044  U.cuni 3177  `'ccnv 3985  dom cdm 3986  ran crn 3987  "cima 3989  -->wf 3994  -onto->wfo 3996  (class class class)co 4884  Topctop 8857   Cn ccn 9028

This theorem is referenced by:  metcnconst 9163  ttcn 14913  pcopt 16084  pcorev 16087  pi1gp 16095

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-fo 4012  df-fv 4014  df-opr 4886  df-oprab 4887  df-map 5383  df-top 8861  df-cn 9030

Copyright terms: Public domain