Theorem cnresima 15891

Description: A continuous function is continuous onto its image.

Assertion

Ref	Expression
cnresima	|- ((J e. Top /\ K e. Top /\ F e. (J Cn K)) -> F e. (J Cn (subSp` <.ran F, K>.)))

Proof of Theorem cnresima

Step	Hyp	Ref	Expression
1		eqid 1884	. . . . 5 |- U.J = U.J
2		eqid 1884	. . . . 5 |- U.K = U.K
3	1, 2	iscn 9034	. . . 4 |- ((J e. Top /\ K e. Top) -> (F e. (J Cn K) <-> (F:U.J-->U.K /\ A.x e. K (`'F"x) e. J)))
4	3	biimpa 460	. . 3 |- (((J e. Top /\ K e. Top) /\ F e. (J Cn K)) -> (F:U.J-->U.K /\ A.x e. K (`'F"x) e. J))
5		simpll 448	. . . . 5 |- (((J e. Top /\ K e. Top) /\ (F:U.J-->U.K /\ A.x e. K (`'F"x) e. J)) -> J e. Top)
6		stoig3 10253	. . . . . . 7 |- ((K e. Top /\ ran F C_ U.K) -> (subSp` <.ran F, K>.) e. Top)
7		frn 4569	. . . . . . 7 |- (F:U.J-->U.K -> ran F C_ U.K)
8	6, 7	sylan2 500	. . . . . 6 |- ((K e. Top /\ F:U.J-->U.K) -> (subSp` <.ran F, K>.) e. Top)
9	8	ad2ant2lr 446	. . . . 5 |- (((J e. Top /\ K e. Top) /\ (F:U.J-->U.K /\ A.x e. K (`'F"x) e. J)) -> (subSp` <.ran F, K>.) e. Top)
10		eqid 1884	. . . . . 6 |- U.(subSp` <.ran F, K>.) = U.(subSp` <.ran F, K>.)
11	1, 10	iscn 9034	. . . . 5 |- ((J e. Top /\ (subSp` <.ran F, K>.) e. Top) -> (F e. (J Cn (subSp` <.ran F, K>.)) <-> (F:U.J-->U.(subSp` <.ran F, K>.) /\ A.y e. (subSp` <.ran F, K>.)(`'F"y) e. J)))
12	5, 9, 11	syl11anc 524	. . . 4 |- (((J e. Top /\ K e. Top) /\ (F:U.J-->U.K /\ A.x e. K (`'F"x) e. J)) -> (F e. (J Cn (subSp` <.ran F, K>.)) <-> (F:U.J-->U.(subSp` <.ran F, K>.) /\ A.y e. (subSp` <.ran F, K>.)(`'F"y) e. J)))
13		ffn 4562	. . . . . . . 8 |- (F:U.J-->U.K -> F Fn U.J)
14		dffn3 4570	. . . . . . . 8 |- (F Fn U.J <-> F:U.J-->ran F)
15	13, 14	sylib 215	. . . . . . 7 |- (F:U.J-->U.K -> F:U.J-->ran F)
16	15	adantl 424	. . . . . 6 |- ((K e. Top /\ F:U.J-->U.K) -> F:U.J-->ran F)
17		stoig2 10252	. . . . . . . 8 |- ((K e. Top /\ ran F C_ U.K) -> U.(subSp` <.ran F, K>.) = ran F)
18	17, 7	sylan2 500	. . . . . . 7 |- ((K e. Top /\ F:U.J-->U.K) -> U.(subSp` <.ran F, K>.) = ran F)
19		feq3 4553	. . . . . . 7 |- (U.(subSp` <.ran F, K>.) = ran F -> (F:U.J-->U.(subSp` <.ran F, K>.) <-> F:U.J-->ran F))
20	18, 19	syl 12	. . . . . 6 |- ((K e. Top /\ F:U.J-->U.K) -> (F:U.J-->U.(subSp` <.ran F, K>.) <-> F:U.J-->ran F))
21	16, 20	mpbird 213	. . . . 5 |- ((K e. Top /\ F:U.J-->U.K) -> F:U.J-->U.(subSp` <.ran F, K>.))
22	21	ad2ant2lr 446	. . . 4 |- (((J e. Top /\ K e. Top) /\ (F:U.J-->U.K /\ A.x e. K (`'F"x) e. J)) -> F:U.J-->U.(subSp` <.ran F, K>.))
23		visset 2295	. . . . . . . . . . 11 |- y e. _V
24		issubspt 10247	. . . . . . . . . . 11 |- ((K e. Top /\ y e. _V /\ ran F e. _V) -> (y e. (subSp` <.ran F, K>.) <-> E.z e. K y = (z i^i ran F)))
25	23, 24	mp3an2 1179	. . . . . . . . . 10 |- ((K e. Top /\ ran F e. _V) -> (y e. (subSp` <.ran F, K>.) <-> E.z e. K y = (z i^i ran F)))
26		fex 4595	. . . . . . . . . . . . 13 |- ((F:U.J-->U.K /\ U.J e. _V) -> F e. _V)
27		uniexg 3795	. . . . . . . . . . . . 13 |- (J e. Top -> U.J e. _V)
28	26, 27	sylan2 500	. . . . . . . . . . . 12 |- ((F:U.J-->U.K /\ J e. Top) -> F e. _V)
29	28	ancoms 484	. . . . . . . . . . 11 |- ((J e. Top /\ F:U.J-->U.K) -> F e. _V)
30		rnexg 4207	. . . . . . . . . . 11 |- (F e. _V -> ran F e. _V)
31	29, 30	syl 12	. . . . . . . . . 10 |- ((J e. Top /\ F:U.J-->U.K) -> ran F e. _V)
32	25, 31	sylan2 500	. . . . . . . . 9 |- ((K e. Top /\ (J e. Top /\ F:U.J-->U.K)) -> (y e. (subSp` <.ran F, K>.) <-> E.z e. K y = (z i^i ran F)))
33	32	anassrs 489	. . . . . . . 8 |- (((K e. Top /\ J e. Top) /\ F:U.J-->U.K) -> (y e. (subSp` <.ran F, K>.) <-> E.z e. K y = (z i^i ran F)))
34	33	ancom1s 548	. . . . . . 7 |- (((J e. Top /\ K e. Top) /\ F:U.J-->U.K) -> (y e. (subSp` <.ran F, K>.) <-> E.z e. K y = (z i^i ran F)))
35	34	adantrr 431	. . . . . 6 |- (((J e. Top /\ K e. Top) /\ (F:U.J-->U.K /\ A.x e. K (`'F"x) e. J)) -> (y e. (subSp` <.ran F, K>.) <-> E.z e. K y = (z i^i ran F)))
36		imaeq2 4260	. . . . . . . . . . . 12 |- (y = (z i^i ran F) -> (`'F"y) = (`'F"(z i^i ran F)))
37	36	eleq1d 1963	. . . . . . . . . . 11 |- (y = (z i^i ran F) -> ((`'F"y) e. J <-> (`'F"(z i^i ran F)) e. J))
38		fnfvelrn 4786	. . . . . . . . . . . . . . . . . . . 20 |- ((F Fn U.J /\ x e. U.J) -> (F` x) e. ran F)
39		simpl 346	. . . . . . . . . . . . . . . . . . . . 21 |- (((F` x) e. z /\ (F` x) e. ran F) -> (F` x) e. z)
40		pm3.21 306	. . . . . . . . . . . . . . . . . . . . 21 |- ((F` x) e. ran F -> ((F` x) e. z -> ((F` x) e. z /\ (F` x) e. ran F)))
41	39, 40	impbid2 576	. . . . . . . . . . . . . . . . . . . 20 |- ((F` x) e. ran F -> (((F` x) e. z /\ (F` x) e. ran F) <-> (F` x) e. z))
42	38, 41	syl 12	. . . . . . . . . . . . . . . . . . 19 |- ((F Fn U.J /\ x e. U.J) -> (((F` x) e. z /\ (F` x) e. ran F) <-> (F` x) e. z))
43		elin 2786	. . . . . . . . . . . . . . . . . . 19 |- ((F` x) e. (z i^i ran F) <-> ((F` x) e. z /\ (F` x) e. ran F))
44	42, 43	syl5bb 591	. . . . . . . . . . . . . . . . . 18 |- ((F Fn U.J /\ x e. U.J) -> ((F` x) e. (z i^i ran F) <-> (F` x) e. z))
45	44	pm5.32da 711	. . . . . . . . . . . . . . . . 17 |- (F Fn U.J -> ((x e. U.J /\ (F` x) e. (z i^i ran F)) <-> (x e. U.J /\ (F` x) e. z)))
46		elpreima 10161	. . . . . . . . . . . . . . . . 17 |- (F Fn U.J -> (x e. (`'F"(z i^i ran F)) <-> (x e. U.J /\ (F` x) e. (z i^i ran F))))
47		elpreima 10161	. . . . . . . . . . . . . . . . 17 |- (F Fn U.J -> (x e. (`'F"z) <-> (x e. U.J /\ (F` x) e. z)))
48	45, 46, 47	3bitr4d 609	. . . . . . . . . . . . . . . 16 |- (F Fn U.J -> (x e. (`'F"(z i^i ran F)) <-> x e. (`'F"z)))
49	48	eqrdv 1882	. . . . . . . . . . . . . . 15 |- (F Fn U.J -> (`'F"(z i^i ran F)) = (`'F"z))
50	13, 49	syl 12	. . . . . . . . . . . . . 14 |- (F:U.J-->U.K -> (`'F"(z i^i ran F)) = (`'F"z))
51	50	adantl 424	. . . . . . . . . . . . 13 |- (((J e. Top /\ K e. Top) /\ F:U.J-->U.K) -> (`'F"(z i^i ran F)) = (`'F"z))
52	51	eleq1d 1963	. . . . . . . . . . . 12 |- (((J e. Top /\ K e. Top) /\ F:U.J-->U.K) -> ((`'F"(z i^i ran F)) e. J <-> (`'F"z) e. J))
53	52	biimpar 461	. . . . . . . . . . 11 |- ((((J e. Top /\ K e. Top) /\ F:U.J-->U.K) /\ (`'F"z) e. J) -> (`'F"(z i^i ran F)) e. J)
54	37, 53	syl5cbir 228	. . . . . . . . . 10 |- ((((J e. Top /\ K e. Top) /\ F:U.J-->U.K) /\ (`'F"z) e. J) -> (y = (z i^i ran F) -> (`'F"y) e. J))
55		imaeq2 4260	. . . . . . . . . . . 12 |- (x = z -> (`'F"x) = (`'F"z))
56	55	eleq1d 1963	. . . . . . . . . . 11 |- (x = z -> ((`'F"x) e. J <-> (`'F"z) e. J))
57	56	rcla4cva 2379	. . . . . . . . . 10 |- ((A.x e. K (`'F"x) e. J /\ z e. K) -> (`'F"z) e. J)
58	54, 57	sylan2 500	. . . . . . . . 9 |- ((((J e. Top /\ K e. Top) /\ F:U.J-->U.K) /\ (A.x e. K (`'F"x) e. J /\ z e. K)) -> (y = (z i^i ran F) -> (`'F"y) e. J))
59	58	anassrs 489	. . . . . . . 8 |- (((((J e. Top /\ K e. Top) /\ F:U.J-->U.K) /\ A.x e. K (`'F"x) e. J) /\ z e. K) -> (y = (z i^i ran F) -> (`'F"y) e. J))
60	59	r19.23adva 2216	. . . . . . 7 |- ((((J e. Top /\ K e. Top) /\ F:U.J-->U.K) /\ A.x e. K (`'F"x) e. J) -> (E.z e. K y = (z i^i ran F) -> (`'F"y) e. J))
61	60	anasss 488	. . . . . 6 |- (((J e. Top /\ K e. Top) /\ (F:U.J-->U.K /\ A.x e. K (`'F"x) e. J)) -> (E.z e. K y = (z i^i ran F) -> (`'F"y) e. J))
62	35, 61	sylbid 220	. . . . 5 |- (((J e. Top /\ K e. Top) /\ (F:U.J-->U.K /\ A.x e. K (`'F"x) e. J)) -> (y e. (subSp` <.ran F, K>.) -> (`'F"y) e. J))
63	62	r19.21aiv 2175	. . . 4 |- (((J e. Top /\ K e. Top) /\ (F:U.J-->U.K /\ A.x e. K (`'F"x) e. J)) -> A.y e. (subSp` <.ran F, K>.)(`'F"y) e. J)
64	12, 22, 63	mpbir2and 802	. . 3 |- (((J e. Top /\ K e. Top) /\ (F:U.J-->U.K /\ A.x e. K (`'F"x) e. J)) -> F e. (J Cn (subSp` <.ran F, K>.)))
65	4, 64	syldan 516	. 2 |- (((J e. Top /\ K e. Top) /\ F e. (J Cn K)) -> F e. (J Cn (subSp` <.ran F, K>.)))
66	65	3impa 1062	1 |- ((J e. Top /\ K e. Top /\ F e. (J Cn K)) -> F e. (J Cn (subSp` <.ran F, K>.)))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  E.wrex 2106  _Vcvv 2292   i^i cin 2592   C_ wss 2593  <.cop 3046  U.cuni 3177  `'ccnv 3985  ran crn 3987  "cima 3989   Fn wfn 3993  -->wf 3994  ` cfv 3998  (class class class)co 4884  Topctop 8857   Cn ccn 9028  subSpcsubsp 10242

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  ax-reg 5695

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-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-iun 3257  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-fv 4014  df-opr 4886  df-oprab 4887  df-map 5383  df-top 8861  df-topsp 8862  df-cn 9030  df-subsp 10243

Copyright terms: Public domain