Theorem gapm 9462

Description: The action of a particular group element is a permutation of the base set. (Contributed by Jeff Hankins, 11-Aug-2009.)

Hypotheses

Ref	Expression
gapm.1	|- X = ran G
gapm.2	|- Y = ran M
gapm.3	|- F = (M o. `'(2nd |` ({A} X. _V)))

Assertion

Ref	Expression
gapm	|- ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> F:Y-1-1-onto->Y)

Proof of Theorem gapm

Step	Hyp	Ref	Expression
1		dff1o4 4644	. 2 |- (F:Y-1-1-onto->Y <-> (F Fn Y /\ `'F Fn Y))
2		gapm.1	. . . . . 6 |- X = ran G
3		gapm.2	. . . . . 6 |- Y = ran M
4	2, 3	gaf 9457	. . . . 5 |- ((M e. B /\ <.G, M>. e. GrpAct) -> M:(X X. Y)-->Y)
5	4	3adant3 896	. . . 4 |- ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> M:(X X. Y)-->Y)
6		simp3 878	. . . 4 |- ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> A e. X)
7		gapm.3	. . . . 5 |- F = (M o. `'(2nd |` ({A} X. _V)))
8	7	curry1f 5076	. . . 4 |- ((M:(X X. Y)-->Y /\ A e. X) -> F:Y-->Y)
9	5, 6, 8	syl11anc 524	. . 3 |- ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> F:Y-->Y)
10		ffn 4562	. . 3 |- (F:Y-->Y -> F Fn Y)
11	9, 10	syl 12	. 2 |- ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> F Fn Y)
12		frel 4566	. . . . . . . . . . . 12 |- (M:(X X. Y)-->Y -> Rel M)
13	5, 12	syl 12	. . . . . . . . . . 11 |- ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> Rel M)
14		dfrel2 4358	. . . . . . . . . . 11 |- (Rel M <-> `'`'M = M)
15	13, 14	sylib 215	. . . . . . . . . 10 |- ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> `'`'M = M)
16	15	imaeq1d 4263	. . . . . . . . 9 |- ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> (`'`'M"({A} X. _V)) = (M"({A} X. _V)))
17		imassrn 4278	. . . . . . . . . . . 12 |- (M"({A} X. _V)) C_ ran M
18	17, 3	sseqtr4i 2650	. . . . . . . . . . 11 |- (M"({A} X. _V)) C_ Y
19	18	a1i 8	. . . . . . . . . 10 |- ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> (M"({A} X. _V)) C_ Y)
20		opelxpi 4040	. . . . . . . . . . . . . . 15 |- ((A e. {A} /\ (((inv` G)` A)Mt) e. _V) -> <.A, (((inv` G)` A)Mt)>. e. ({A} X. _V))
21		snidg 3067	. . . . . . . . . . . . . . . . 17 |- (A e. X -> A e. {A})
22	21	3ad2ant3 899	. . . . . . . . . . . . . . . 16 |- ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> A e. {A})
23	22	adantr 425	. . . . . . . . . . . . . . 15 |- (((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) /\ t e. Y) -> A e. {A})
24		oprex 4907	. . . . . . . . . . . . . . 15 |- (((inv` G)` A)Mt) e. _V
25	20, 23, 24	sylancl 525	. . . . . . . . . . . . . 14 |- (((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) /\ t e. Y) -> <.A, (((inv` G)` A)Mt)>. e. ({A} X. _V))
26		eqid 1884	. . . . . . . . . . . . . . . . 17 |- (((inv` G)` A)Mt) = (((inv` G)` A)Mt)
27		simpl1 879	. . . . . . . . . . . . . . . . . 18 |- (((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) /\ t e. Y) -> M e. B)
28		simpl2 880	. . . . . . . . . . . . . . . . . 18 |- (((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) /\ t e. Y) -> <.G, M>. e. GrpAct)
29		simpl3 881	. . . . . . . . . . . . . . . . . 18 |- (((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) /\ t e. Y) -> A e. X)
30	5	adantr 425	. . . . . . . . . . . . . . . . . . 19 |- (((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) /\ t e. Y) -> M:(X X. Y)-->Y)
31		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . 23 |- (inv` G) = (inv` G)
32	2, 31	grpinvcl 9352	. . . . . . . . . . . . . . . . . . . . . 22 |- ((G e. Grp /\ A e. X) -> ((inv` G)` A) e. X)
33		gagrp 9456	. . . . . . . . . . . . . . . . . . . . . 22 |- ((M e. B /\ <.G, M>. e. GrpAct) -> G e. Grp)
34	32, 33	sylan 497	. . . . . . . . . . . . . . . . . . . . 21 |- (((M e. B /\ <.G, M>. e. GrpAct) /\ A e. X) -> ((inv` G)` A) e. X)
35	34	3impa 1062	. . . . . . . . . . . . . . . . . . . 20 |- ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> ((inv` G)` A) e. X)
36	35	adantr 425	. . . . . . . . . . . . . . . . . . 19 |- (((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) /\ t e. Y) -> ((inv` G)` A) e. X)
37		simpr 350	. . . . . . . . . . . . . . . . . . 19 |- (((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) /\ t e. Y) -> t e. Y)
38		foprrn 4965	. . . . . . . . . . . . . . . . . . 19 |- ((M:(X X. Y)-->Y /\ ((inv` G)` A) e. X /\ t e. Y) -> (((inv` G)` A)Mt) e. Y)
39	30, 36, 37, 38	syl111anc 1100	. . . . . . . . . . . . . . . . . 18 |- (((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) /\ t e. Y) -> (((inv` G)` A)Mt) e. Y)
40	2, 3, 31	gacan 9460	. . . . . . . . . . . . . . . . . 18 |- ((M e. B /\ <.G, M>. e. GrpAct /\ (A e. X /\ (((inv` G)` A)Mt) e. Y /\ t e. Y)) -> ((AM(((inv` G)` A)Mt)) = t <-> (((inv` G)` A)Mt) = (((inv` G)` A)Mt)))
41	27, 28, 29, 39, 37, 40	syl113anc 1112	. . . . . . . . . . . . . . . . 17 |- (((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) /\ t e. Y) -> ((AM(((inv` G)` A)Mt)) = t <-> (((inv` G)` A)Mt) = (((inv` G)` A)Mt)))
42	26, 41	mpbiri 211	. . . . . . . . . . . . . . . 16 |- (((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) /\ t e. Y) -> (AM(((inv` G)` A)Mt)) = t)
43		df-opr 4886	. . . . . . . . . . . . . . . 16 |- (AM(((inv` G)` A)Mt)) = (M` <.A, (((inv` G)` A)Mt)>.)
44	42, 43	syl5eqr 1942	. . . . . . . . . . . . . . 15 |- (((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) /\ t e. Y) -> (M` <.A, (((inv` G)` A)Mt)>.) = t)
45		ffn 4562	. . . . . . . . . . . . . . . . . . 19 |- (M:(X X. Y)-->Y -> M Fn (X X. Y))
46	4, 45	syl 12	. . . . . . . . . . . . . . . . . 18 |- ((M e. B /\ <.G, M>. e. GrpAct) -> M Fn (X X. Y))
47	46	3adant3 896	. . . . . . . . . . . . . . . . 17 |- ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> M Fn (X X. Y))
48	47	adantr 425	. . . . . . . . . . . . . . . 16 |- (((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) /\ t e. Y) -> M Fn (X X. Y))
49		opelxpi 4040	. . . . . . . . . . . . . . . . 17 |- ((A e. X /\ (((inv` G)` A)Mt) e. Y) -> <.A, (((inv` G)` A)Mt)>. e. (X X. Y))
50	29, 39, 49	syl11anc 524	. . . . . . . . . . . . . . . 16 |- (((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) /\ t e. Y) -> <.A, (((inv` G)` A)Mt)>. e. (X X. Y))
51		visset 2295	. . . . . . . . . . . . . . . . 17 |- t e. _V
52	51	fnopfvb 4713	. . . . . . . . . . . . . . . 16 |- ((M Fn (X X. Y) /\ <.A, (((inv` G)` A)Mt)>. e. (X X. Y)) -> ((M` <.A, (((inv` G)` A)Mt)>.) = t <-> <.<.A, (((inv` G)` A)Mt)>., t>. e. M))
53	48, 50, 52	syl11anc 524	. . . . . . . . . . . . . . 15 |- (((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) /\ t e. Y) -> ((M` <.A, (((inv` G)` A)Mt)>.) = t <-> <.<.A, (((inv` G)` A)Mt)>., t>. e. M))
54	44, 53	mpbid 212	. . . . . . . . . . . . . 14 |- (((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) /\ t e. Y) -> <.<.A, (((inv` G)` A)Mt)>., t>. e. M)
55		opex 3527	. . . . . . . . . . . . . . 15 |- <.A, (((inv` G)` A)Mt)>. e. _V
56		eleq1 1957	. . . . . . . . . . . . . . . 16 |- (x = <.A, (((inv` G)` A)Mt)>. -> (x e. ({A} X. _V) <-> <.A, (((inv` G)` A)Mt)>. e. ({A} X. _V)))
57		opeq1 3158	. . . . . . . . . . . . . . . . 17 |- (x = <.A, (((inv` G)` A)Mt)>. -> <.x, t>. = <.<.A, (((inv` G)` A)Mt)>., t>.)
58	57	eleq1d 1963	. . . . . . . . . . . . . . . 16 |- (x = <.A, (((inv` G)` A)Mt)>. -> (<.x, t>. e. M <-> <.<.A, (((inv` G)` A)Mt)>., t>. e. M))
59	56, 58	anbi12d 690	. . . . . . . . . . . . . . 15 |- (x = <.A, (((inv` G)` A)Mt)>. -> ((x e. ({A} X. _V) /\ <.x, t>. e. M) <-> (<.A, (((inv` G)` A)Mt)>. e. ({A} X. _V) /\ <.<.A, (((inv` G)` A)Mt)>., t>. e. M)))
60	55, 59	cla4ev 2371	. . . . . . . . . . . . . 14 |- ((<.A, (((inv` G)` A)Mt)>. e. ({A} X. _V) /\ <.<.A, (((inv` G)` A)Mt)>., t>. e. M) -> E.x(x e. ({A} X. _V) /\ <.x, t>. e. M))
61	25, 54, 60	syl11anc 524	. . . . . . . . . . . . 13 |- (((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) /\ t e. Y) -> E.x(x e. ({A} X. _V) /\ <.x, t>. e. M))
62	61	ex 402	. . . . . . . . . . . 12 |- ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> (t e. Y -> E.x(x e. ({A} X. _V) /\ <.x, t>. e. M)))
63	51	elima3 4272	. . . . . . . . . . . 12 |- (t e. (M"({A} X. _V)) <-> E.x(x e. ({A} X. _V) /\ <.x, t>. e. M))
64	62, 63	syl6ibr 230	. . . . . . . . . . 11 |- ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> (t e. Y -> t e. (M"({A} X. _V))))
65	64	ssrdv 2622	. . . . . . . . . 10 |- ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> Y C_ (M"({A} X. _V)))
66	19, 65	eqssd 2633	. . . . . . . . 9 |- ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> (M"({A} X. _V)) = Y)
67	16, 66	eqtrd 1925	. . . . . . . 8 |- ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> (`'`'M"({A} X. _V)) = Y)
68		dmres 4234	. . . . . . . . . 10 |- dom (2nd |` ({A} X. _V)) = (({A} X. _V) i^i dom 2nd)
69		ssv 2636	. . . . . . . . . . . 12 |- ({A} X. _V) C_ _V
70		fo2nd 5033	. . . . . . . . . . . . 13 |- 2nd:_V-onto->_V
71		fofn 4619	. . . . . . . . . . . . . 14 |- (2nd:_V-onto->_V -> 2nd Fn _V)
72		fndm 4512	. . . . . . . . . . . . . 14 |- (2nd Fn _V -> dom 2nd = _V)
73	71, 72	syl 12	. . . . . . . . . . . . 13 |- (2nd:_V-onto->_V -> dom 2nd = _V)
74	70, 73	ax-mp 7	. . . . . . . . . . . 12 |- dom 2nd = _V
75	69, 74	sseqtr4i 2650	. . . . . . . . . . 11 |- ({A} X. _V) C_ dom 2nd
76		df-ss 2605	. . . . . . . . . . 11 |- (({A} X. _V) C_ dom 2nd <-> (({A} X. _V) i^i dom 2nd) = ({A} X. _V))
77	75, 76	mpbi 206	. . . . . . . . . 10 |- (({A} X. _V) i^i dom 2nd) = ({A} X. _V)
78	68, 77	eqtri 1908	. . . . . . . . 9 |- dom (2nd |` ({A} X. _V)) = ({A} X. _V)
79	78	imaeq2i 4262	. . . . . . . 8 |- (`'`'M"dom (2nd |` ({A} X. _V))) = (`'`'M"({A} X. _V))
80	67, 79	syl5eq 1940	. . . . . . 7 |- ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> (`'`'M"dom (2nd |` ({A} X. _V))) = Y)
81		dmco 4406	. . . . . . 7 |- dom ((2nd |` ({A} X. _V)) o. `'M) = (`'`'M"dom (2nd |` ({A} X. _V)))
82	80, 81	syl5eq 1940	. . . . . 6 |- ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> dom ((2nd |` ({A} X. _V)) o. `'M) = Y)
83		relco 4392	. . . . . . . . 9 |- Rel ((2nd |` ({A} X. _V)) o. `'M)
84	83	a1i12 9	. . . . . . . 8 |- ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> (dom ((2nd |` ({A} X. _V)) o. `'M) = Y -> Rel ((2nd |` ({A} X. _V)) o. `'M)))
85		raleq 2266	. . . . . . . . 9 |- (dom ((2nd |` ({A} X. _V)) o. `'M) = Y -> (A.t e. dom ((2nd |` ({A} X. _V)) o. `'M)E*x t((2nd |` ({A} X. _V)) o. `'M)x <-> A.t e. Y E*x t((2nd |` ({A} X. _V)) o. `'M)x))
86	2, 3, 31	gapmlem 9461	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) /\ t e. Y) /\ (zMt /\ z(2nd |` ({A} X. _V))x)) -> (((inv` G)` A)Mt) = x)
87	86	ex 402	. . . . . . . . . . . . . . . . . . . . . 22 |- (((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) /\ t e. Y) -> ((zMt /\ z(2nd |` ({A} X. _V))x) -> (((inv` G)` A)Mt) = x))
88	2, 3, 31	gapmlem 9461	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) /\ t e. Y) /\ (wMt /\ w(2nd |` ({A} X. _V))y)) -> (((inv` G)` A)Mt) = y)
89	88	ex 402	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) /\ t e. Y) -> ((wMt /\ w(2nd |` ({A} X. _V))y) -> (((inv` G)` A)Mt) = y))
90		eqtr 1904	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((x = (((inv` G)` A)Mt) /\ (((inv` G)` A)Mt) = y) -> x = y)
91	90	ex 402	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (x = (((inv` G)` A)Mt) -> ((((inv` G)` A)Mt) = y -> x = y))
92	91	eqcoms 1887	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((inv` G)` A)Mt) = x -> ((((inv` G)` A)Mt) = y -> x = y))
93	89, 92	syl9 71	. . . . . . . . . . . . . . . . . . . . . 22 |- (((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) /\ t e. Y) -> ((((inv` G)` A)Mt) = x -> ((wMt /\ w(2nd |` ({A} X. _V))y) -> x = y)))
94	87, 93	syld 30	. . . . . . . . . . . . . . . . . . . . 21 |- (((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) /\ t e. Y) -> ((zMt /\ z(2nd |` ({A} X. _V))x) -> ((wMt /\ w(2nd |` ({A} X. _V))y) -> x = y)))
95	94	expcom 403	. . . . . . . . . . . . . . . . . . . 20 |- (t e. Y -> ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> ((zMt /\ z(2nd |` ({A} X. _V))x) -> ((wMt /\ w(2nd |` ({A} X. _V))y) -> x = y))))
96	95	com4t 44	. . . . . . . . . . . . . . . . . . 19 |- ((zMt /\ z(2nd |` ({A} X. _V))x) -> ((wMt /\ w(2nd |` ({A} X. _V))y) -> (t e. Y -> ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> x = y))))
97	96	19.23adv 1584	. . . . . . . . . . . . . . . . . 18 |- ((zMt /\ z(2nd |` ({A} X. _V))x) -> (E.w(wMt /\ w(2nd |` ({A} X. _V))y) -> (t e. Y -> ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> x = y))))
98	97	19.23aiv 1674	. . . . . . . . . . . . . . . . 17 |- (E.z(zMt /\ z(2nd |` ({A} X. _V))x) -> (E.w(wMt /\ w(2nd |` ({A} X. _V))y) -> (t e. Y -> ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> x = y))))
99	98	imp 377	. . . . . . . . . . . . . . . 16 |- ((E.z(zMt /\ z(2nd |` ({A} X. _V))x) /\ E.w(wMt /\ w(2nd |` ({A} X. _V))y)) -> (t e. Y -> ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> x = y)))
100	99	com13 37	. . . . . . . . . . . . . . 15 |- ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> (t e. Y -> ((E.z(zMt /\ z(2nd |` ({A} X. _V))x) /\ E.w(wMt /\ w(2nd |` ({A} X. _V))y)) -> x = y)))
101		visset 2295	. . . . . . . . . . . . . . . . . . 19 |- x e. _V
102	51, 101	brco 4132	. . . . . . . . . . . . . . . . . 18 |- (t((2nd |` ({A} X. _V)) o. `'M)x <-> E.z(t`'Mz /\ z(2nd |` ({A} X. _V))x))
103		visset 2295	. . . . . . . . . . . . . . . . . . . . 21 |- z e. _V
104	51, 103	brcnv 4144	. . . . . . . . . . . . . . . . . . . 20 |- (t`'Mz <-> zMt)
105	104	anbi1i 539	. . . . . . . . . . . . . . . . . . 19 |- ((t`'Mz /\ z(2nd |` ({A} X. _V))x) <-> (zMt /\ z(2nd |` ({A} X. _V))x))
106	105	exbii 1398	. . . . . . . . . . . . . . . . . 18 |- (E.z(t`'Mz /\ z(2nd |` ({A} X. _V))x) <-> E.z(zMt /\ z(2nd |` ({A} X. _V))x))
107	102, 106	bitr2i 191	. . . . . . . . . . . . . . . . 17 |- (E.z(zMt /\ z(2nd |` ({A} X. _V))x) <-> t((2nd |` ({A} X. _V)) o. `'M)x)
108		visset 2295	. . . . . . . . . . . . . . . . . . 19 |- y e. _V
109	51, 108	brco 4132	. . . . . . . . . . . . . . . . . 18 |- (t((2nd |` ({A} X. _V)) o. `'M)y <-> E.w(t`'Mw /\ w(2nd |` ({A} X. _V))y))
110		visset 2295	. . . . . . . . . . . . . . . . . . . . 21 |- w e. _V
111	51, 110	brcnv 4144	. . . . . . . . . . . . . . . . . . . 20 |- (t`'Mw <-> wMt)
112	111	anbi1i 539	. . . . . . . . . . . . . . . . . . 19 |- ((t`'Mw /\ w(2nd |` ({A} X. _V))y) <-> (wMt /\ w(2nd |` ({A} X. _V))y))
113	112	exbii 1398	. . . . . . . . . . . . . . . . . 18 |- (E.w(t`'Mw /\ w(2nd |` ({A} X. _V))y) <-> E.w(wMt /\ w(2nd |` ({A} X. _V))y))
114	109, 113	bitr2i 191	. . . . . . . . . . . . . . . . 17 |- (E.w(wMt /\ w(2nd |` ({A} X. _V))y) <-> t((2nd |` ({A} X. _V)) o. `'M)y)
115	107, 114	anbi12i 540	. . . . . . . . . . . . . . . 16 |- ((E.z(zMt /\ z(2nd |` ({A} X. _V))x) /\ E.w(wMt /\ w(2nd |` ({A} X. _V))y)) <-> (t((2nd |` ({A} X. _V)) o. `'M)x /\ t((2nd |` ({A} X. _V)) o. `'M)y))
116	115	imbi1i 203	. . . . . . . . . . . . . . 15 |- (((E.z(zMt /\ z(2nd |` ({A} X. _V))x) /\ E.w(wMt /\ w(2nd |` ({A} X. _V))y)) -> x = y) <-> ((t((2nd |` ({A} X. _V)) o. `'M)x /\ t((2nd |` ({A} X. _V)) o. `'M)y) -> x = y))
117	100, 116	syl6ib 229	. . . . . . . . . . . . . 14 |- ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> (t e. Y -> ((t((2nd |` ({A} X. _V)) o. `'M)x /\ t((2nd |` ({A} X. _V)) o. `'M)y) -> x = y)))
118		breq2 3342	. . . . . . . . . . . . . . . 16 |- (x = y -> (t((2nd |` ({A} X. _V)) o. `'M)x <-> t((2nd |` ({A} X. _V)) o. `'M)y))
119	108, 118	sbcie 2485	. . . . . . . . . . . . . . 15 |- ([y / x]t((2nd |` ({A} X. _V)) o. `'M)x <-> t((2nd |` ({A} X. _V)) o. `'M)y)
120	119	anbi2i 538	. . . . . . . . . . . . . 14 |- ((t((2nd |` ({A} X. _V)) o. `'M)x /\ [y / x]t((2nd |` ({A} X. _V)) o. `'M)x) <-> (t((2nd |` ({A} X. _V)) o. `'M)x /\ t((2nd |` ({A} X. _V)) o. `'M)y))
121	117, 120	syl7ib 233	. . . . . . . . . . . . 13 |- ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> (t e. Y -> ((t((2nd |` ({A} X. _V)) o. `'M)x /\ [y / x]t((2nd |` ({A} X. _V)) o. `'M)x) -> x = y)))
122	121	19.21adv 1666	. . . . . . . . . . . 12 |- ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> (t e. Y -> A.y((t((2nd |` ({A} X. _V)) o. `'M)x /\ [y / x]t((2nd |` ({A} X. _V)) o. `'M)x) -> x = y)))
123	122	19.21adv 1666	. . . . . . . . . . 11 |- ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> (t e. Y -> A.xA.y((t((2nd |` ({A} X. _V)) o. `'M)x /\ [y / x]t((2nd |` ({A} X. _V)) o. `'M)x) -> x = y)))
124		ax-17 1317	. . . . . . . . . . . 12 |- (t((2nd |` ({A} X. _V)) o. `'M)x -> A.y t((2nd |` ({A} X. _V)) o. `'M)x)
125	124	mo3 1797	. . . . . . . . . . 11 |- (E*x t((2nd |` ({A} X. _V)) o. `'M)x <-> A.xA.y((t((2nd |` ({A} X. _V)) o. `'M)x /\ [y / x]t((2nd |` ({A} X. _V)) o. `'M)x) -> x = y))
126	123, 125	syl6ibr 230	. . . . . . . . . 10 |- ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> (t e. Y -> E*x t((2nd |` ({A} X. _V)) o. `'M)x))
127	126	r19.21aiv 2175	. . . . . . . . 9 |- ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> A.t e. Y E*x t((2nd |` ({A} X. _V)) o. `'M)x)
128	85, 127	syl5cbir 228	. . . . . . . 8 |- ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> (dom ((2nd |` ({A} X. _V)) o. `'M) = Y -> A.t e. dom ((2nd |` ({A} X. _V)) o. `'M)E*x t((2nd |` ({A} X. _V)) o. `'M)x))
129	84, 128	jcad 661	. . . . . . 7 |- ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> (dom ((2nd |` ({A} X. _V)) o. `'M) = Y -> (Rel ((2nd |` ({A} X. _V)) o. `'M) /\ A.t e. dom ((2nd |` ({A} X. _V)) o. `'M)E*x t((2nd |` ({A} X. _V)) o. `'M)x)))
130		dffun7 4447	. . . . . . 7 |- (Fun ((2nd |` ({A} X. _V)) o. `'M) <-> (Rel ((2nd |` ({A} X. _V)) o. `'M) /\ A.t e. dom ((2nd |` ({A} X. _V)) o. `'M)E*x t((2nd |` ({A} X. _V)) o. `'M)x))
131	129, 130	syl6ibr 230	. . . . . 6 |- ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> (dom ((2nd |` ({A} X. _V)) o. `'M) = Y -> Fun ((2nd |` ({A} X. _V)) o. `'M)))
132	82, 131	jcai 313	. . . . 5 |- ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> (dom ((2nd |` ({A} X. _V)) o. `'M) = Y /\ Fun ((2nd |` ({A} X. _V)) o. `'M)))
133	132	ancomd 483	. . . 4 |- ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> (Fun ((2nd |` ({A} X. _V)) o. `'M) /\ dom ((2nd |` ({A} X. _V)) o. `'M) = Y))
134		df-fn 4009	. . . 4 |- (((2nd |` ({A} X. _V)) o. `'M) Fn Y <-> (Fun ((2nd |` ({A} X. _V)) o. `'M) /\ dom ((2nd |` ({A} X. _V)) o. `'M) = Y))
135	133, 134	sylibr 217	. . 3 |- ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> ((2nd |` ({A} X. _V)) o. `'M) Fn Y)
136	7	cnveqi 4136	. . . . 5 |- `'F = `'(M o. `'(2nd |` ({A} X. _V)))
137		cnvco 4145	. . . . 5 |- `'(M o. `'(2nd |` ({A} X. _V))) = (`'`'(2nd |` ({A} X. _V)) o. `'M)
138		cocnvcnv1 4408	. . . . 5 |- (`'`'(2nd |` ({A} X. _V)) o. `'M) = ((2nd |` ({A} X. _V)) o. `'M)
139	136, 137, 138	3eqtri 1912	. . . 4 |- `'F = ((2nd |` ({A} X. _V)) o. `'M)
140	139	fneq1i 4507	. . 3 |- (`'F Fn Y <-> ((2nd |` ({A} X. _V)) o. `'M) Fn Y)
141	135, 140	sylibr 217	. 2 |- ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> `'F Fn Y)
142	1, 11, 141	sylanbrc 527	1 |- ((M e. B /\ <.G, M>. e. GrpAct /\ A e. X) -> F:Y-1-1-onto->Y)

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326  [wsbc 1534  E*wmo 1772  A.wral 2105  _Vcvv 2292   i^i cin 2592   C_ wss 2593  {csn 3044  <.cop 3046   class class class wbr 3338   X. cxp 3984  `'ccnv 3985  dom cdm 3986  ran crn 3987   |` cres 3988  "cima 3989   o. ccom 3990  Rel wrel 3991  Fun wfun 3992   Fn wfn 3993  -->wf 3994  -onto->wfo 3996  -1-1-onto->wf1o 3997  ` cfv 3998  (class class class)co 4884  2ndc2nd 5019  Grpcgr 9311  invcgn 9313  GrpActcga 9447

This theorem is referenced by:  gaplc 14731  gapm2 14732

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-reu 2111  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-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-1st 5020  df-2nd 5021  df-grp 9316  df-gid 9317  df-ginv 9318  df-ga 9448

Copyright terms: Public domain