Theorem mapenlem1 3384

Description: Lemma for mapen 3386.

Hypotheses

Ref	Expression
mapenlem.1	|- A e. V
mapenlem.2	|- B e. V
mapenlem.3	|- C e. V
mapenlem.4	|- D e. V
mapenlem.5	|- H = {<.x, y>. | (x e. (A ^m C) /\ y = ((f o. x) o. `'g))}

Assertion

Ref	Expression
mapenlem1	|- ((((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ z:C-->A) /\ v e. C) -> ((H` z)` (g` v)) = (f` (z` v)))

Distinct variable group(s):   f,g,x,y,z,v,A   B,f,g,x,y,z,v   C,f,g,x,y,z,v   D,f,g,x,y,z,v   z,H,v

Proof of Theorem mapenlem1

Step	Hyp	Ref	Expression
1		mapenlem.1	. . . . . 6 |- A e. V
2		mapenlem.3	. . . . . 6 |- C e. V
3	1, 2	elmap 3265	. . . . 5 |- (z e. (A ^m C) <-> z:C-->A)
4		coeq2 2503	. . . . . . 7 |- (x = z -> (f o. x) = (f o. z))
5	4	coeq1d 2506	. . . . . 6 |- (x = z -> ((f o. x) o. `'g) = ((f o. z) o. `'g))
6		mapenlem.5	. . . . . 6 |- H = {<.x, y>. | (x e. (A ^m C) /\ y = ((f o. x) o. `'g))}
7		visset 1350	. . . . . . . 8 |- f e. V
8		visset 1350	. . . . . . . 8 |- z e. V
9	7, 8	coex 2672	. . . . . . 7 |- (f o. z) e. V
10		visset 1350	. . . . . . . 8 |- g e. V
11	10	cnvex 2670	. . . . . . 7 |- `'g e. V
12	9, 11	coex 2672	. . . . . 6 |- ((f o. z) o. `'g) e. V
13	5, 6, 12	fvopab4 2871	. . . . 5 |- (z e. (A ^m C) -> (H` z) = ((f o. z) o. `'g))
14	3, 13	sylbir 176	. . . 4 |- (z:C-->A -> (H` z) = ((f o. z) o. `'g))
15	14	fveq1d 2834	. . 3 |- (z:C-->A -> ((H` z)` (g` v)) = (((f o. z) o. `'g)` (g` v)))
16	15	ad2antlr 321	. 2 |- ((((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ z:C-->A) /\ v e. C) -> ((H` z)` (g` v)) = (((f o. z) o. `'g)` (g` v)))
17		f1ococnv1 2818	. . . . . . . . . 10 |- (g:C-1-1-onto->D -> (`'g o. g) = (I |` C))
18	17	coeq2d 2507	. . . . . . . . 9 |- (g:C-1-1-onto->D -> ((f o. z) o. (`'g o. g)) = ((f o. z) o. (I |` C)))
19		fcoi1 2765	. . . . . . . . 9 |- ((f o. z):C-->B -> ((f o. z) o. (I |` C)) = (f o. z))
20	18, 19	sylan9eqr 1145	. . . . . . . 8 |- (((f o. z):C-->B /\ g:C-1-1-onto->D) -> ((f o. z) o. (`'g o. g)) = (f o. z))
21		fco 2760	. . . . . . . . 9 |- ((f:A-->B /\ z:C-->A) -> (f o. z):C-->B)
22		f1of 2800	. . . . . . . . 9 |- (f:A-1-1-onto->B -> f:A-->B)
23	21, 22	sylan 343	. . . . . . . 8 |- ((f:A-1-1-onto->B /\ z:C-->A) -> (f o. z):C-->B)
24	20, 23	sylan 343	. . . . . . 7 |- (((f:A-1-1-onto->B /\ z:C-->A) /\ g:C-1-1-onto->D) -> ((f o. z) o. (`'g o. g)) = (f o. z))
25	24	an1rs 373	. . . . . 6 |- (((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ z:C-->A) -> ((f o. z) o. (`'g o. g)) = (f o. z))
26		coass 2667	. . . . . 6 |- (((f o. z) o. `'g) o. g) = ((f o. z) o. (`'g o. g))
27	25, 26	syl5eq 1136	. . . . 5 |- (((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ z:C-->A) -> (((f o. z) o. `'g) o. g) = (f o. z))
28	27	fveq1d 2834	. . . 4 |- (((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ z:C-->A) -> ((((f o. z) o. `'g) o. g)` v) = ((f o. z)` v))
29	28	adantr 306	. . 3 |- ((((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ z:C-->A) /\ v e. C) -> ((((f o. z) o. `'g) o. g)` v) = ((f o. z)` v))
30		fvco3 2867	. . . . . . . . . 10 |- (((Fun ((f o. z) o. `'g) /\ g:C-->D) /\ v e. C) -> ((((f o. z) o. `'g) o. g)` v) = (((f o. z) o. `'g)` (g` v)))
31	30	exp 291	. . . . . . . . 9 |- ((Fun ((f o. z) o. `'g) /\ g:C-->D) -> (v e. C -> ((((f o. z) o. `'g) o. g)` v) = (((f o. z) o. `'g)` (g` v))))
32		funco 2696	. . . . . . . . . 10 |- ((Fun (f o. z) /\ Fun `'g) -> Fun ((f o. z) o. `'g))
33		funco 2696	. . . . . . . . . . 11 |- ((Fun f /\ Fun z) -> Fun (f o. z))
34		f1ofun 2802	. . . . . . . . . . 11 |- (f:A-1-1-onto->B -> Fun f)
35		ffun 2754	. . . . . . . . . . 11 |- (z:C-->A -> Fun z)
36	33, 34, 35	syl2an 349	. . . . . . . . . 10 |- ((f:A-1-1-onto->B /\ z:C-->A) -> Fun (f o. z))
37		f1o3 2805	. . . . . . . . . . 11 |- (g:C-1-1-onto->D <-> (g:C-onto->D /\ Fun `'g))
38	37	pm3.27bd 263	. . . . . . . . . 10 |- (g:C-1-1-onto->D -> Fun `'g)
39	32, 36, 38	syl2an 349	. . . . . . . . 9 |- (((f:A-1-1-onto->B /\ z:C-->A) /\ g:C-1-1-onto->D) -> Fun ((f o. z) o. `'g))
40		f1of 2800	. . . . . . . . 9 |- (g:C-1-1-onto->D -> g:C-->D)
41	31, 39, 40	syl2an 349	. . . . . . . 8 |- ((((f:A-1-1-onto->B /\ z:C-->A) /\ g:C-1-1-onto->D) /\ g:C-1-1-onto->D) -> (v e. C -> ((((f o. z) o. `'g) o. g)` v) = (((f o. z) o. `'g)` (g` v))))
42	41	exp31 293	. . . . . . 7 |- ((f:A-1-1-onto->B /\ z:C-->A) -> (g:C-1-1-onto->D -> (g:C-1-1-onto->D -> (v e. C -> ((((f o. z) o. `'g) o. g)` v) = (((f o. z) o. `'g)` (g` v))))))
43	42	pm2.43d 59	. . . . . 6 |- ((f:A-1-1-onto->B /\ z:C-->A) -> (g:C-1-1-onto->D -> (v e. C -> ((((f o. z) o. `'g) o. g)` v) = (((f o. z) o. `'g)` (g` v)))))
44	43	exp 291	. . . . 5 |- (f:A-1-1-onto->B -> (z:C-->A -> (g:C-1-1-onto->D -> (v e. C -> ((((f o. z) o. `'g) o. g)` v) = (((f o. z) o. `'g)` (g` v))))))
45	44	com23 32	. . . 4 |- (f:A-1-1-onto->B -> (g:C-1-1-onto->D -> (z:C-->A -> (v e. C -> ((((f o. z) o. `'g) o. g)` v) = (((f o. z) o. `'g)` (g` v))))))
46	45	imp41 286	. . 3 |- ((((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ z:C-->A) /\ v e. C) -> ((((f o. z) o. `'g) o. g)` v) = (((f o. z) o. `'g)` (g` v)))
47		fvco3 2867	. . . . . . 7 |- (((Fun f /\ z:C-->A) /\ v e. C) -> ((f o. z)` v) = (f` (z` v)))
48	47	anasss 337	. . . . . 6 |- ((Fun f /\ (z:C-->A /\ v e. C)) -> ((f o. z)` v) = (f` (z` v)))
49	48, 34	sylan 343	. . . . 5 |- ((f:A-1-1-onto->B /\ (z:C-->A /\ v e. C)) -> ((f o. z)` v) = (f` (z` v)))
50	49	adantlr 310	. . . 4 |- (((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ (z:C-->A /\ v e. C)) -> ((f o. z)` v) = (f` (z` v)))
51	50	anassrs 338	. . 3 |- ((((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ z:C-->A) /\ v e. C) -> ((f o. z)` v) = (f` (z` v)))
52	29, 46, 51	3eqtr3d 1133	. 2 |- ((((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ z:C-->A) /\ v e. C) -> (((f o. z) o. `'g)` (g` v)) = (f` (z` v)))
53	16, 52	eqtrd 1128	1 |- ((((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ z:C-->A) /\ v e. C) -> ((H` z)` (g` v)) = (f` (z` v)))

Syntax hints:   -> wi 2   /\ wa 196   = weq 797   = wceq 1091   e. wcel 1092  Vcvv 1348  {copab 2055  Icid 2057  `'ccnv 2409   |` cres 2412   o. ccom 2414  Fun wfun 2416  -->wf 2418  -onto->wfo 2420  -1-1-onto->wf1o 2421  ` cfv 2422  (class class class)co 3001   ^m cm 3258

This theorem is referenced by:  mapenlem2 3385

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799