Theorem mapenlem2 3385

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
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 group(s):   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 2760	. . . . . . . . . . . 12 |- (((f o. x):C-->B /\ `'g:D-->C) -> ((f o. x) o. `'g):D-->B)
2		fco 2760	. . . . . . . . . . . . 13 |- ((f:A-->B /\ x:C-->A) -> (f o. x):C-->B)
3		f1of 2800	. . . . . . . . . . . . 13 |- (f:A-1-1-onto->B -> f:A-->B)
4	2, 3	sylan 343	. . . . . . . . . . . 12 |- ((f:A-1-1-onto->B /\ x:C-->A) -> (f o. x):C-->B)
5		f1ocnv 2811	. . . . . . . . . . . . 13 |- (g:C-1-1-onto->D -> `'g:D-1-1-onto->C)
6		f1of 2800	. . . . . . . . . . . . 13 |- (`'g:D-1-1-onto->C -> `'g:D-->C)
7	5, 6	syl 12	. . . . . . . . . . . 12 |- (g:C-1-1-onto->D -> `'g:D-->C)
8	1, 4, 7	syl2an 349	. . . . . . . . . . 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 293	. . . . . . . . . 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 277	. . . . . . . 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 3265	. . . . . . . 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 3265	. . . . . . . 8 |- (((f o. x) o. `'g) e. (B ^m D) <-> ((f o. x) o. `'g):D-->B)
18	11, 14, 17	3imtr4g 426	. . . . . . 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 1259	. . . . . 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 2891	. . . . . 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 173	. . . . 5 |- ((f:A-1-1-onto->B /\ g:C-1-1-onto->D) -> H:(A ^m C)-->(B ^m D))
23		fveq1 2831	. . . . . . . . . . . . . . . . 17 |- ((H` z) = (H` w) -> ((H` z)` (g` v)) = ((H` w)` (g` v)))
24	23	adantl 305	. . . . . . . . . . . . . . . 16 |- (((z:C-->A /\ w:C-->A) /\ (H` z) = (H` w)) -> ((H` z)` (g` v)) = ((H` w)` (g` v)))
25	24	ad2antlr 321	. . . . . . . . . . . . . . 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)) = ((H` w)` (g` v)))
26	12, 15, 13, 16, 20	mapenlem1 3384	. . . . . . . . . . . . . . . . . . 19 |- ((((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 311	. . . . . . . . . . . . . . . . . 18 |- ((((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 301	. . . . . . . . . . . . . . . . 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))))))
29	28	adantrd 308	. . . . . . . . . . . . . . . 16 |- ((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 287	. . . . . . . . . . . . . . 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)))
31	12, 15, 13, 16, 20	mapenlem1 3384	. . . . . . . . . . . . . . . . . . 19 |- ((((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 311	. . . . . . . . . . . . . . . . . 18 |- ((((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 301	. . . . . . . . . . . . . . . . 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))))))
34	33	adantld 307	. . . . . . . . . . . . . . . 16 |- ((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 287	. . . . . . . . . . . . . . 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)))
36	25, 30, 35	3eqtr3d 1133	. . . . . . . . . . . . . 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)))
37		f1fveq 2918	. . . . . . . . . . . . . . . . 17 |- ((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 2799	. . . . . . . . . . . . . . . . 17 |- (f:A-1-1-onto->B -> f:A-1-1->B)
39		ffvrn 2890	. . . . . . . . . . . . . . . . . . . 20 |- ((z:C-->A /\ v e. C) -> (z` v) e. A)
40	39	adantlr 310	. . . . . . . . . . . . . . . . . . 19 |- (((z:C-->A /\ w:C-->A) /\ v e. C) -> (z` v) e. A)
41		ffvrn 2890	. . . . . . . . . . . . . . . . . . . 20 |- ((w:C-->A /\ v e. C) -> (w` v) e. A)
42	41	adantll 309	. . . . . . . . . . . . . . . . . . 19 |- (((z:C-->A /\ w:C-->A) /\ v e. C) -> (w` v) e. A)
43	40, 42	jca 236	. . . . . . . . . . . . . . . . . 18 |- (((z:C-->A /\ w:C-->A) /\ v e. C) -> ((z` v) e. A /\ (w` v) e. A))
44	43	adantlr 310	. . . . . . . . . . . . . . . . 17 |- ((((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 349	. . . . . . . . . . . . . . . 16 |- ((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 310	. . . . . . . . . . . . . . 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)) -> ((f` (z` v)) = (f` (w` v)) <-> (z` v) = (w` v)))
47	46	anassrs 338	. . . . . . . . . . . . . 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) -> ((