Theorem mapenlem2 4490

Description: Lemma for mapen 4491.

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
mapenlem2	|- ((f:A-1-1-onto->B /\ g:C-1-1-onto->D) -> H:(A ^m C)-1-1-onto->(B ^m D))

Distinct variable groups:   f,g,x,y,A   B,f,g,x,y   C,f,g,x,y   D,f,g,x,y

Proof of Theorem mapenlem2

Step	Hyp	Ref	Expression
1		fco 3636	. . . . . . . . . . . 12 |- (((f o. x):C-->B /\ `'g:D-->C) -> ((f o. x) o. `'g):D-->B)
2		fco 3636	. . . . . . . . . . . . 13 |- ((f:A-->B /\ x:C-->A) -> (f o. x):C-->B)
3		f1of 3689	. . . . . . . . . . . . 13 |- (f:A-1-1-onto->B -> f:A-->B)
4	2, 3	sylan 448	. . . . . . . . . . . 12 |- ((f:A-1-1-onto->B /\ x:C-->A) -> (f o. x):C-->B)
5		f1ocnv 3701	. . . . . . . . . . . . 13 |- (g:C-1-1-onto->D -> `'g:D-1-1-onto->C)
6		f1of 3689	. . . . . . . . . . . . 13 |- (`'g:D-1-1-onto->C -> `'g:D-->C)
7	5, 6	syl 10	. . . . . . . . . . . 12 |- (g:C-1-1-onto->D -> `'g:D-->C)
8	1, 4, 7	syl2an 454	. . . . . . . . . . 11 |- (((f:A-1-1-onto->B /\ x:C-->A) /\ g:C-1-1-onto->D) -> ((f o. x) o. `'g):D-->B)
9	8	exp31 376	. . . . . . . . . 10 |- (f:A-1-1-onto->B -> (x:C-->A -> (g:C-1-1-onto->D -> ((f o. x) o. `'g):D-->B)))
10	9	com23 32	. . . . . . . . 9 |- (f:A-1-1-onto->B -> (g:C-1-1-onto->D -> (x:C-->A -> ((f o. x) o. `'g):D-->B)))
11	10	imp 350	. . . . . . . 8 |- ((f:A-1-1-onto->B /\ g:C-1-1-onto->D) -> (x:C-->A -> ((f o. x) o. `'g):D-->B))
12		mapenlem.1	. . . . . . . . 9 |- A e. V
13		mapenlem.3	. . . . . . . . 9 |- C e. V
14	12, 13	elmap 4334	. . . . . . . 8 |- (x e. (A ^m C) <-> x:C-->A)
15		mapenlem.2	. . . . . . . . 9 |- B e. V
16		mapenlem.4	. . . . . . . . 9 |- D e. V
17	15, 16	elmap 4334	. . . . . . . 8 |- (((f o. x) o. `'g) e. (B ^m D) <-> ((f o. x) o. `'g):D-->B)
18	11, 14, 17	3imtr4g 553	. . . . . . 7 |- ((f:A-1-1-onto->B /\ g:C-1-1-onto->D) -> (x e. (A ^m C) -> ((f o. x) o. `'g) e. (B ^m D)))
19	18	r19.21aiv 1713	. . . . . 6 |- ((f:A-1-1-onto->B /\ g:C-1-1-onto->D) -> A.x e. (A ^m C)((f o. x) o. `'g) e. (B ^m D))
20		mapenlem.5	. . . . . . 7 |- H = {<.x, y>. | (x e. (A ^m C) /\ y = ((f o. x) o. `'g))}
21	20	fopab2 3823	. . . . . 6 |- (A.x e. (A ^m C)((f o. x) o. `'g) e. (B ^m D) <-> H:(A ^m C)-->(B ^m D))
22	19, 21	sylib 198	. . . . 5 |- ((f:A-1-1-onto->B /\ g:C-1-1-onto->D) -> H:(A ^m C)-->(B ^m D))
23		fveq1 3723	. . . . . . . . . . . . . . . 16 |- ((H` z) = (H` w) -> ((H` z)` (g` v)) = ((H` w)` (g` v)))
24	23	adantl 388	. . . . . . . . . . . . . . 15 |- (((z:C-->A /\ w:C-->A) /\ (H` z) = (H` w)) -> ((H` z)` (g` v)) = ((H` w)` (g` v)))
25	24	ad2antlr 405	. . . . . . . . . . . . . 14 |- ((((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ ((z:C-->A /\ w:C-->A) /\ (H` z) = (H` w))) /\ v e. C) -> ((H` z)` (g` v)) = ((H` w)` (g` v)))
26	12, 15, 13, 16, 20	mapenlem1 4489	. . . . . . . . . . . . . . . . . 18 |- ((((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)))
27	26	adantrl 394	. . . . . . . . . . . . . . . . 17 |- ((((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ z:C-->A) /\ ((H` z) = (H` w) /\ v e. C)) -> ((H` z)` (g` v)) = (f` (z` v)))
28	27	exp43 384	. . . . . . . . . . . . . . . 16 |- ((f:A-1-1-onto->B /\ g:C-1-1-onto->D) -> (z:C-->A -> ((H` z) = (H` w) -> (v e. C -> ((H` z)` (g` v)) = (f` (z` v))))))
29	28	adantrd 391	. . . . . . . . . . . . . . 15 |- ((f:A-1-1-onto->B /\ g:C-1-1-onto->D) -> ((z:C-->A /\ w:C-->A) -> ((H` z) = (H` w) -> (v e. C -> ((H` z)` (g` v)) = (f` (z` v))))))
30	29	imp42 369	. . . . . . . . . . . . . 14 |- ((((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ ((z:C-->A /\ w:C-->A) /\ (H` z) = (H` w))) /\ v e. C) -> ((H` z)` (g` v)) = (f` (z` v)))
31	12, 15, 13, 16, 20	mapenlem1 4489	. . . . . . . . . . . . . . . . . 18 |- ((((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ w:C-->A) /\ v e. C) -> ((H` w)` (g` v)) = (f` (w` v)))
32	31	adantrl 394	. . . . . . . . . . . . . . . . 17 |- ((((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ w:C-->A) /\ ((H` z) = (H` w) /\ v e. C)) -> ((H` w)` (g` v)) = (f` (w` v)))
33	32	exp43 384	. . . . . . . . . . . . . . . 16 |- ((f:A-1-1-onto->B /\ g:C-1-1-onto->D) -> (w:C-->A -> ((H` z) = (H` w) -> (v e. C -> ((H` w)` (g` v)) = (f` (w` v))))))
34	33	adantld 390	. . . . . . . . . . . . . . 15 |- ((f:A-1-1-onto->B /\ g:C-1-1-onto->D) -> ((z:C-->A /\ w:C-->A) -> ((H` z) = (H` w) -> (v e. C -> ((H` w)` (g` v)) = (f` (w` v))))))
35	34	imp42 369	. . . . . . . . . . . . . 14 |- ((((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ ((z:C-->A /\ w:C-->A) /\ (H` z) = (H` w))) /\ v e. C) -> ((H` w)` (g` v)) = (f` (w` v)))
36	25, 30, 35	3eqtr3d 1515	. . . . . . . . . . . . 13 |- ((((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ ((z:C-->A /\ w:C-->A) /\ (H` z) = (H` w))) /\ v e. C) -> (f` (z` v)) = (f` (w` v)))
37		f1fveq 3876	. . . . . . . . . . . . . . . 16 |- ((f:A-1-1->B /\ ((z` v) e. A /\ (w` v) e. A)) -> ((f` (z` v)) = (f` (w` v)) <-> (z` v) = (w` v)))
38		f1of1 3688	. . . . . . . . . . . . . . . 16 |- (f:A-1-1-onto->B -> f:A-1-1->B)
39		ffvelrn 3814	. . . . . . . . . . . . . . . . . . 19 |- ((z:C-->A /\ v e. C) -> (z` v) e. A)
40	39	adantlr 393	. . . . . . . . . . . . . . . . . 18 |- (((z:C-->A /\ w:C-->A) /\ v e. C) -> (z` v) e. A)
41		ffvelrn 3814	. . . . . . . . . . . . . . . . . . 19 |- ((w:C-->A /\ v e. C) -> (w` v) e. A)
42	41	adantll 392	. . . . . . . . . . . . . . . . . 18 |- (((z:C-->A /\ w:C-->A) /\ v e. C) -> (w` v) e. A)
43	40, 42	jca 288	. . . . . . . . . . . . . . . . 17 |- (((z:C-->A /\ w:C-->A) /\ v e. C) -> ((z` v) e. A /\ (w` v) e. A))
44	43	adantlr 393	. . . . . . . . . . . . . . . 16 |- ((((z:C-->A /\ w:C-->A) /\ (H` z) = (H` w)) /\ v e. C) -> ((z` v) e. A /\ (w` v) e. A))
45	37, 38, 44	syl2an 454	. . . . . . . . . . . . . . 15 |- ((f:A-1-1-onto->B /\ (((z:C-->A /\ w:C-->A) /\ (H` z) = (H` w)) /\ v e. C)) -> ((f` (z` v)) = (f` (w` v)) <-> (z` v) = (w` v)))
46	45	adantlr 393	. . . . . . . . . . . . . 14 |- (((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ (((z:C-->A /\ w:C-->A) /\ (H` z) = (H` w)) /\ v e. C)) -> ((f` (z` v)) = (f` (w` v)) <-> (z` v) = (w` v)))
47	46	anassrs 441	. . . . . . . . . . . . 13 |- ((((f:A-1-1-onto->B /\ g:C