Theorem mapenlem2 5584

Description: Lemma for mapen 5585.

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		dff1o5 4646	. 2 |- (H:(A ^m C)-1-1-onto->(B ^m D) <-> (H:(A ^m C)-1-1->(B ^m D) /\ ran H = (B ^m D)))
2		dff13 4850	. . 3 |- (H:(A ^m C)-1-1->(B ^m D) <-> (H:(A ^m C)-->(B ^m D) /\ A.z e. (A ^m C)A.w e. (A ^m C)((H` z) = (H` w) -> z = w)))
3		fco 4573	. . . . . . . . . 10 |- (((f o. x):C-->B /\ `'g:D-->C) -> ((f o. x) o. `'g):D-->B)
4		fco 4573	. . . . . . . . . . 11 |- ((f:A-->B /\ x:C-->A) -> (f o. x):C-->B)
5		f1of 4635	. . . . . . . . . . 11 |- (f:A-1-1-onto->B -> f:A-->B)
6	4, 5	sylan 497	. . . . . . . . . 10 |- ((f:A-1-1-onto->B /\ x:C-->A) -> (f o. x):C-->B)
7		f1ocnv 4651	. . . . . . . . . . 11 |- (g:C-1-1-onto->D -> `'g:D-1-1-onto->C)
8		f1of 4635	. . . . . . . . . . 11 |- (`'g:D-1-1-onto->C -> `'g:D-->C)
9	7, 8	syl 12	. . . . . . . . . 10 |- (g:C-1-1-onto->D -> `'g:D-->C)
10	3, 6, 9	syl2an 503	. . . . . . . . 9 |- (((f:A-1-1-onto->B /\ x:C-->A) /\ g:C-1-1-onto->D) -> ((f o. x) o. `'g):D-->B)
11	10	exp31 407	. . . . . . . 8 |- (f:A-1-1-onto->B -> (x:C-->A -> (g:C-1-1-onto->D -> ((f o. x) o. `'g):D-->B)))
12	11	com23 36	. . . . . . 7 |- (f:A-1-1-onto->B -> (g:C-1-1-onto->D -> (x:C-->A -> ((f o. x) o. `'g):D-->B)))
13	12	imp 377	. . . . . 6 |- ((f:A-1-1-onto->B /\ g:C-1-1-onto->D) -> (x:C-->A -> ((f o. x) o. `'g):D-->B))
14		mapenlem.1	. . . . . . 7 |- A e. _V
15		mapenlem.3	. . . . . . 7 |- C e. _V
16	14, 15	elmap 5393	. . . . . 6 |- (x e. (A ^m C) <-> x:C-->A)
17		mapenlem.2	. . . . . . 7 |- B e. _V
18		mapenlem.4	. . . . . . 7 |- D e. _V
19	17, 18	elmap 5393	. . . . . 6 |- (((f o. x) o. `'g) e. (B ^m D) <-> ((f o. x) o. `'g):D-->B)
20	13, 16, 19	3imtr4g 612	. . . . 5 |- ((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)))
21	20	r19.21aiv 2175	. . . 4 |- ((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))
22		mapenlem.5	. . . . 5 |- H = {<.x, y>. | (x e. (A ^m C) /\ y = ((f o. x) o. `'g))}
23	22	fopab2 4796	. . . 4 |- (A.x e. (A ^m C)((f o. x) o. `'g) e. (B ^m D) <-> H:(A ^m C)-->(B ^m D))
24	21, 23	sylib 215	. . 3 |- ((f:A-1-1-onto->B /\ g:C-1-1-onto->D) -> H:(A ^m C)-->(B ^m D))
25		fveq1 4680	. . . . . . . . . . . . . 14 |- ((H` z) = (H` w) -> ((H` z)` (g` v)) = ((H` w)` (g` v)))
26	25	adantl 424	. . . . . . . . . . . . 13 |- (((z:C-->A /\ w:C-->A) /\ (H` z) = (H` w)) -> ((H` z)` (g` v)) = ((H` w)` (g` v)))
27	26	ad2antlr 441	. . . . . . . . . . . 12 |- ((((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)))
28	14, 17, 15, 18, 22	mapenlem1 5583	. . . . . . . . . . . . . . . 16 |- ((((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)))
29	28	adantrl 430	. . . . . . . . . . . . . . 15 |- ((((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)))
30	29	exp43 415	. . . . . . . . . . . . . 14 |- ((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))))))
31	30	adantrd 427	. . . . . . . . . . . . 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 -> ((H` z)` (g` v)) = (f` (z` v))))))
32	31	imp42 396	. . . . . . . . . . . 12 |- ((((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)))
33	14, 17, 15, 18, 22	mapenlem1 5583	. . . . . . . . . . . . . . . 16 |- ((((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)))
34	33	adantrl 430	. . . . . . . . . . . . . . 15 |- ((((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)))
35	34	exp43 415	. . . . . . . . . . . . . 14 |- ((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))))))
36	35	adantld 426	. . . . . . . . . . . . 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 -> ((H` w)` (g` v)) = (f` (w` v))))))
37	36	imp42 396	. . . . . . . . . . . 12 |- ((((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)))
38	27, 32, 37	3eqtr3d 1934	. . . . . . . . . . 11 |- ((((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)))
39		f1fveq 4852	. . . . . . . . . . . . . 14 |- ((f:A-1-1->B /\ ((z` v) e. A /\ (w` v) e. A)) -> ((f` (z` v)) = (f` (w` v)) <-> (z` v) = (w` v)))
40		f1of1 4634	. . . . . . . . . . . . . 14 |- (f:A-1-1-onto->B -> f:A-1-1->B)
41		ffvelrn 4787	. . . . . . . . . . . . . . . . 17 |- ((z:C-->A /\ v e. C) -> (z` v) e. A)
42	41	adantlr 429	. . . . . . . . . . . . . . . 16 |- (((z:C-->A /\ w:C-->A) /\ v e. C) -> (z` v) e. A)
43		ffvelrn 4787	. . . . . . . . . . . . . . . . 17 |- ((w:C-->A /\ v e. C) -> (w` v) e. A)
44	43	adantll 428	. . . . . . . . . . . . . . . 16 |- (((z:C-->A /\ w:C-->A) /\ v e. C) -> (w` v) e. A)
45	42, 44	jca 310	. . . . . . . . . . . . . . 15 |- (((z:C-->A /\ w:C-->A) /\ v e. C) -> ((z` v) e. A /\ (w` v) e. A))
46	45	adantlr 429	. . . . . . . . . . . . . 14 |- ((((z:C-->A /\ w:C-->A) /\ (H` z) = (H` w)) /\ v e. C) -> ((z` v) e. A /\ (w` v) e. A))
47	39, 40, 46	syl2an 503	. . . . . . . . . . . . 13 |- ((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)))
48	47	adantlr 429	. . . . . . . . . . . 12 |- (((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)))
49	48	anassrs 489	. . . . . . . . . . 11 |- ((((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)))
50	38, 49	mpbid 212	. . . . . . . . . 10 |- ((((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) -> (z` v) = (w` v))
51	50	r19.21aiva 2176	. . . . . . . . 9 |- (((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ ((z:C-->A /\ w:C-->A) /\ (H` z) = (H` w))) -> A.v e. C (z` v) = (w` v))
52		eqfnfv2 4767	. . . . . . . . . . 11 |- ((z Fn C /\ w Fn C) -> (z = w <-> A.v e. C (z` v) = (w` v)))
53		ffn 4562	. . . . . . . . . . 11 |- (z:C-->A -> z Fn C)
54		ffn 4562	. . . . . . . . . . 11 |- (w:C-->A -> w Fn C)
55	52, 53, 54	syl2an 503	. . . . . . . . . 10 |- ((z:C-->A /\ w:C-->A) -> (z = w <-> A.v e. C (z` v) = (w` v)))
56	55	ad2antrl 442	. . . . . . . . 9 |- (((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ ((z:C-->A /\ w:C-->A) /\ (H` z) = (H` w))) -> (z = w <-> A.v e. C (z` v) = (w` v)))
57	51, 56	mpbird 213	. . . . . . . 8 |- (((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ ((z:C-->A /\ w:C-->A) /\ (H` z) = (H` w))) -> z = w)
58	57	exp32 408	. . . . . . 7 |- ((f:A-1-1-onto->B /\ g:C-1-1-onto->D) -> ((z:C-->A /\ w:C-->A) -> ((H` z) = (H` w) -> z = w)))
59	14, 15	elmap 5393	. . . . . . . 8 |- (z e. (A ^m C) <-> z:C-->A)
60	14, 15	elmap 5393	. . . . . . . 8 |- (w e. (A ^m C) <-> w:C-->A)
61	59, 60	anbi12i 540	. . . . . . 7 |- ((z e. (A ^m C) /\ w e. (A ^m C)) <-> (z:C-->A /\ w:C-->A))
62	58, 61	syl5ib 223	. . . . . 6 |- ((f:A-1-1-onto->B /\ g:C-1-1-onto->D) -> ((z e. (A ^m C) /\ w e. (A ^m C)) -> ((H` z) = (H` w) -> z = w)))
63	62	exp3a 405	. . . . 5 |- ((f:A-1-1-onto->B /\ g:C-1-1-onto->D) -> (z e. (A ^m C) -> (w e. (A ^m C) -> ((H` z) = (H` w) -> z = w))))
64	63	r19.21adv 2181	. . . 4 |- ((f:A-1-1-onto->B /\ g:C-1-1-onto->D) -> (z e. (A ^m C) -> A.w e. (A ^m C)((H` z) = (H` w) -> z = w)))
65	64	r19.21aiv 2175	. . 3 |- ((f:A-1-1-onto->B /\ g:C-1-1-onto->D) -> A.z e. (A ^m C)A.w e. (A ^m C)((H` z) = (H` w) -> z = w))
66	2, 24, 65	sylanbrc 527	. 2 |- ((f:A-1-1-onto->B /\ g:C-1-1-onto->D) -> H:(A ^m C)-1-1->(B ^m D))
67		frn 4569	. . . 4 |- (H:(A ^m C)-->(B ^m D) -> ran H C_ (B ^m D))
68	24, 67	syl 12	. . 3 |- ((f:A-1-1-onto->B /\ g:C-1-1-onto->D) -> ran H C_ (B ^m D))
69		fco 4573	. . . . . . . . . . . 12 |- (((`'f o. z):D-->A /\ g:C-->D) -> ((`'f o. z) o. g):C-->A)
70		fco 4573	. . . . . . . . . . . . 13 |- ((`'f:B-->A /\ z:D-->B) -> (`'f o. z):D-->A)
71		f1ocnv 4651	. . . . . . . . . . . . . 14 |- (f:A-1-1-onto->B -> `'f:B-1-1-onto->A)
72		f1of 4635	. . . . . . . . . . . . . 14 |- (`'f:B-1-1-onto->A -> `'f:B-->A)
73	71, 72	syl 12	. . . . . . . . . . . . 13 |- (f:A-1-1-onto->B -> `'f:B-->A)
74	70, 73	sylan 497	. . . . . . . . . . . 12 |- ((f:A-1-1-onto->B /\ z:D-->B) -> (`'f o. z):D-->A)
75		f1of 4635	. . . . . . . . . . . 12 |- (g:C-1-1-onto->D -> g:C-->D)
76	69, 74, 75	syl2an 503	. . . . . . . . . . 11 |- (((f:A-1-1-onto->B /\ z:D-->B) /\ g:C-1-1-onto->D) -> ((`'f o. z) o. g):C-->A)
77	76	an1rs 547	. . . . . . . . . 10 |- (((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ z:D-->B) -> ((`'f o. z) o. g):C-->A)
78	14, 15	elmap 5393	. . . . . . . . . 10 |- (((`'f o. z) o. g) e. (A ^m C) <-> ((`'f o. z) o. g):C-->A)
79	77, 78	sylibr 217	. . . . . . . . 9 |- (((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ z:D-->B) -> ((`'f o. z) o. g) e. (A ^m C))
80		coeq2 4124	. . . . . . . . . . . . 13 |- (x = ((`'f o. z) o. g) -> (f o. x) = (f o. ((`'f o. z) o. g)))
81	80	coeq1d 4127	. . . . . . . . . . . 12 |- (x = ((`'f o. z) o. g) -> ((f o. x) o. `'g) = ((f o. ((`'f o. z) o. g)) o. `'g))
82		visset 2295	. . . . . . . . . . . . . 14 |- f e. _V
83	82	cnvex 4425	. . . . . . . . . . . . . . . 16 |- `'f e. _V
84		visset 2295	. . . . . . . . . . . . . . . 16 |- z e. _V
85	83, 84	coex 4430	. . . . . . . . . . . . . . 15 |- (`'f o. z) e. _V
86		visset 2295	. . . . . . . . . . . . . . 15 |- g e. _V
87	85, 86	coex 4430	. . . . . . . . . . . . . 14 |- ((`'f o. z) o. g) e. _V
88	82, 87	coex 4430	. . . . . . . . . . . . 13 |- (f o. ((`'f o. z) o. g)) e. _V
89	86	cnvex 4425	. . . . . . . . . . . . 13 |- `'g e. _V
90	88, 89	coex 4430	. . . . . . . . . . . 12 |- ((f o. ((`'f o. z) o. g)) o. `'g) e. _V
91	81, 22, 90	fvopab4 4743	. . . . . . . . . . 11 |- (((`'f o. z) o. g) e. (A ^m C) -> (H` ((`'f o. z) o. g)) = ((f o. ((`'f o. z) o. g)) o. `'g))
92	79, 91	syl 12	. . . . . . . . . 10 |- (((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ z:D-->B) -> (H` ((`'f o. z) o. g)) = ((f o. ((`'f o. z) o. g)) o. `'g))
93		f1ococnv2 4662	. . . . . . . . . . . . . . . 16 |- (f:A-1-1-onto->B -> (f o. `'f) = ( _I |` B))
94	93	coeq1d 4127	. . . . . . . . . . . . . . 15 |- (f:A-1-1-onto->B -> ((f o. `'f) o. z) = (( _I |` B) o. z))
95		fcoi2 4586	. . . . . . . . . . . . . . 15 |- (z:D-->B -> (( _I |` B) o. z) = z)
96	94, 95	sylan9eq 1948	. . . . . . . . . . . . . 14 |- ((f:A-1-1-onto->B /\ z:D-->B) -> ((f o. `'f) o. z) = z)
97	96	coeq1d 4127	. . . . . . . . . . . . 13 |- ((f:A-1-1-onto->B /\ z:D-->B) -> (((f o. `'f) o. z) o. (g o. `'g)) = (z o. (g o. `'g)))
98	97	adantlr 429	. . . . . . . . . . . 12 |- (((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ z:D-->B) -> (((f o. `'f) o. z) o. (g o. `'g)) = (z o. (g o. `'g)))
99		f1ococnv2 4662	. . . . . . . . . . . . . . 15 |- (g:C-1-1-onto->D -> (g o. `'g) = ( _I |` D))
100	99	coeq2d 4128	. . . . . . . . . . . . . 14 |- (g:C-1-1-onto->D -> (z o. (g o. `'g)) = (z o. ( _I |` D)))
101		fcoi1 4584	. . . . . . . . . . . . . 14 |- (z:D-->B -> (z o. ( _I |` D)) = z)
102	100, 101	sylan9eq 1948	. . . . . . . . . . . . 13 |- ((g:C-1-1-onto->D /\ z:D-->B) -> (z o. (g o. `'g)) = z)
103	102	adantll 428	. . . . . . . . . . . 12 |- (((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ z:D-->B) -> (z o. (g o. `'g)) = z)
104	98, 103	eqtrd 1925	. . . . . . . . . . 11 |- (((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ z:D-->B) -> (((f o. `'f) o. z) o. (g o. `'g)) = z)
105		coass 4415	. . . . . . . . . . . 12 |- ((f o. ((`'f o. z) o. g)) o. `'g) = (f o. (((`'f o. z) o. g) o. `'g))
106		coass 4415	. . . . . . . . . . . . 13 |- (((`'f o. z) o. g) o. `'g) = ((`'f o. z) o. (g o. `'g))
107	106	coeq2i 4126	. . . . . . . . . . . 12 |- (f o. (((`'f o. z) o. g) o. `'g)) = (f o. ((`'f o. z) o. (g o. `'g)))
108		coass 4415	. . . . . . . . . . . . . 14 |- ((f o. `'f) o. z) = (f o. (`'f o. z))
109	108	coeq1i 4125	. . . . . . . . . . . . 13 |- (((f o. `'f) o. z) o. (g o. `'g)) = ((f o. (`'f o. z)) o. (g o. `'g))
110		coass 4415	. . . . . . . . . . . . 13 |- ((f o. (`'f o. z)) o. (g o. `'g)) = (f o. ((`'f o. z) o. (g o. `'g)))
111	109, 110	eqtr2i 1909	. . . . . . . . . . . 12 |- (f o. ((`'f o. z) o. (g o. `'g))) = (((f o. `'f) o. z) o. (g o. `'g))
112	105, 107, 111	3eqtri 1912	. . . . . . . . . . 11 |- ((f o. ((`'f o. z) o. g)) o. `'g) = (((f o. `'f) o. z) o. (g o. `'g))
113	104, 112	syl5eq 1940	. . . . . . . . . 10 |- (((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ z:D-->B) -> ((f o. ((`'f o. z) o. g)) o. `'g) = z)
114	92, 113	eqtrd 1925	. . . . . . . . 9 |- (((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ z:D-->B) -> (H` ((`'f o. z) o. g)) = z)
115	79, 114	jca 310	. . . . . . . 8 |- (((f:A-1-1-onto->B /\ g:C-1-1-onto->D) /\ z:D-->B) -> (((`'f o. z) o. g) e. (A ^m C) /\ (H` ((`'f o. z) o. g)) = z))
116	115	ex 402	. . . . . . 7 |- ((f:A-1-1-onto->B /\ g:C-1-1-onto->D) -> (z:D-->B -> (((`'f o. z) o. g) e. (A ^m C) /\ (H` ((`'f o. z) o. g)) = z)))
117	17, 18	elmap 5393	. . . . . . 7 |- (z e. (B ^m D) <-> z:D-->B)
118	116, 117	syl5ib 223	. . . . . 6 |- ((f:A-1-1-onto->B /\ g:C-1-1-onto->D) -> (z e. (B ^m D) -> (((`'f o. z) o. g) e. (A ^m C) /\ (H` ((`'f o. z) o. g)) = z)))
119		fveq2 4681	. . . . . . . 8 |- (w = ((`'f o. z) o. g) -> (H` w) = (H` ((`'f o. z) o. g)))
120	119	eqeq1d 1892	. . . . . . 7 |- (w = ((`'f o. z) o. g) -> ((H` w) = z <-> (H` ((`'f o. z) o. g)) = z))
121	120	rcla4ev 2381	. . . . . 6 |- ((((`'f o. z) o. g) e. (A ^m C) /\ (H` ((`'f o. z) o. g)) = z) -> E.w e. (A ^m C)(H` w) = z)
122	118, 121	syl6 25	. . . . 5 |- ((f:A-1-1-onto->B /\ g:C-1-1-onto->D) -> (z e. (B ^m D) -> E.w e. (A ^m C)(H` w) = z))
123		ffn 4562	. . . . . 6 |- (H:(A ^m C)-->(B ^m D) -> H Fn (A ^m C))
124		fvelrnb 4719	. . . . . 6 |- (H Fn (A ^m C) -> (z e. ran H <-> E.w e. (A ^m C)(H` w) = z))
125	24, 123, 124	3syl 24	. . . . 5 |- ((f:A-1-1-onto->B /\ g:C-1-1-onto->D) -> (z e. ran H <-> E.w e. (A ^m C)(H` w) = z))
126	122, 125	sylibrd 221	. . . 4 |- ((f:A-1-1-onto->B /\ g:C-1-1-onto->D) -> (z e. (B ^m D) -> z e. ran H))
127	126	ssrdv 2622	. . 3 |- ((f:A-1-1-onto->B /\ g:C-1-1-onto->D) -> (B ^m D) C_ ran H)
128	68, 127	eqssd 2633	. 2 |- ((f:A-1-1-onto->B /\ g:C-1-1-onto->D) -> ran H = (B ^m D))
129	1, 66, 128	sylanbrc 527	1 |- ((f:A-1-1-onto->B /\ g:C-1-1-onto->D) -> H:(A ^m C)-1-1-onto->(B ^m D))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300  A.wral 2105  E.wrex 2106  _Vcvv 2292   C_ wss 2593  {copab 3395   _I cid 3582  `'ccnv 3985  ran crn 3987   |` cres 3988   o. ccom 3990   Fn wfn 3993  -->wf 3994  -1-1->wf1 3995  -1-1-onto->wf1o 3997  ` cfv 3998  (class class class)co 4884   ^m cmap 5381

This theorem is referenced by:  mapen 5585

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-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-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-map 5383

Copyright terms: Public domain