Metamath Proof Explorer

Theorem symggen

Description: The span of the transpositions is the subgroup that moves finitely many points. (Contributed by Stefan O'Rear, 28-Aug-2015)

Ref Expression
Hypotheses symgtrf.t 
|- T = ran ( pmTrsp ` D )
symgtrf.g 
|- G = ( SymGrp ` D )
symgtrf.b 
|- B = ( Base ` G )
symggen.k 
|- K = ( mrCls ` ( SubMnd ` G ) )
Assertion symggen 
|- ( D e. V -> ( K ` T ) = { x e. B | dom ( x \ _I ) e. Fin } )

Proof

Step Hyp Ref Expression
1 symgtrf.t 
 |-  T = ran ( pmTrsp ` D )
2 symgtrf.g 
 |-  G = ( SymGrp ` D )
3 symgtrf.b 
 |-  B = ( Base ` G )
4 symggen.k 
 |-  K = ( mrCls ` ( SubMnd ` G ) )
5 elex 
 |-  ( D e. V -> D e. _V )
6 2 symggrp 
 |-  ( D e. _V -> G e. Grp )
7 6 grpmndd 
 |-  ( D e. _V -> G e. Mnd )
8 3 submacs 
 |-  ( G e. Mnd -> ( SubMnd ` G ) e. ( ACS ` B ) )
9 acsmre 
 |-  ( ( SubMnd ` G ) e. ( ACS ` B ) -> ( SubMnd ` G ) e. ( Moore ` B ) )
10 7 8 9 3syl 
 |-  ( D e. _V -> ( SubMnd ` G ) e. ( Moore ` B ) )
11 5 10 syl 
 |-  ( D e. V -> ( SubMnd ` G ) e. ( Moore ` B ) )
12 1 2 3 symgtrf 
 |-  T C_ B
13 12 a1i 
 |-  ( D e. V -> T C_ B )
14 2onn 
 |-  2o e. _om
15 nnfi 
 |-  ( 2o e. _om -> 2o e. Fin )
16 14 15 ax-mp 
 |-  2o e. Fin
17 eqid 
 |-  ( pmTrsp ` D ) = ( pmTrsp ` D )
18 17 1 pmtrfb 
 |-  ( x e. T <-> ( D e. _V /\ x : D -1-1-onto-> D /\ dom ( x \ _I ) ~~ 2o ) )
19 18 simp3bi 
 |-  ( x e. T -> dom ( x \ _I ) ~~ 2o )
20 enfi 
 |-  ( dom ( x \ _I ) ~~ 2o -> ( dom ( x \ _I ) e. Fin <-> 2o e. Fin ) )
21 19 20 syl 
 |-  ( x e. T -> ( dom ( x \ _I ) e. Fin <-> 2o e. Fin ) )
22 21 adantl 
 |-  ( ( D e. V /\ x e. T ) -> ( dom ( x \ _I ) e. Fin <-> 2o e. Fin ) )
23 16 22 mpbiri 
 |-  ( ( D e. V /\ x e. T ) -> dom ( x \ _I ) e. Fin )
24 13 23 ssrabdv 
 |-  ( D e. V -> T C_ { x e. B | dom ( x \ _I ) e. Fin } )
25 2 3 symgfisg 
 |-  ( D e. V -> { x e. B | dom ( x \ _I ) e. Fin } e. ( SubGrp ` G ) )
26 subgsubm 
 |-  ( { x e. B | dom ( x \ _I ) e. Fin } e. ( SubGrp ` G ) -> { x e. B | dom ( x \ _I ) e. Fin } e. ( SubMnd ` G ) )
27 25 26 syl 
 |-  ( D e. V -> { x e. B | dom ( x \ _I ) e. Fin } e. ( SubMnd ` G ) )
28 4 mrcsscl 
 |-  ( ( ( SubMnd ` G ) e. ( Moore ` B ) /\ T C_ { x e. B | dom ( x \ _I ) e. Fin } /\ { x e. B | dom ( x \ _I ) e. Fin } e. ( SubMnd ` G ) ) -> ( K ` T ) C_ { x e. B | dom ( x \ _I ) e. Fin } )
29 11 24 27 28 syl3anc 
 |-  ( D e. V -> ( K ` T ) C_ { x e. B | dom ( x \ _I ) e. Fin } )
30 vex 
 |-  x e. _V
31 30 a1i 
 |-  ( dom ( x \ _I ) e. Fin -> x e. _V )
32 finnum 
 |-  ( dom ( x \ _I ) e. Fin -> dom ( x \ _I ) e. dom card )
33 domfi 
 |-  ( ( dom ( x \ _I ) e. Fin /\ dom ( y \ _I ) ~<_ dom ( x \ _I ) ) -> dom ( y \ _I ) e. Fin )
34 2 3 symgbasf1o 
 |-  ( y e. B -> y : D -1-1-onto-> D )
35 34 adantl 
 |-  ( ( dom ( y \ _I ) e. Fin /\ y e. B ) -> y : D -1-1-onto-> D )
36 f1ofn 
 |-  ( y : D -1-1-onto-> D -> y Fn D )
37 fnnfpeq0 
 |-  ( y Fn D -> ( dom ( y \ _I ) = (/) <-> y = ( _I |` D ) ) )
38 35 36 37 3syl 
 |-  ( ( dom ( y \ _I ) e. Fin /\ y e. B ) -> ( dom ( y \ _I ) = (/) <-> y = ( _I |` D ) ) )
39 2 3 elbasfv 
 |-  ( y e. B -> D e. _V )
40 39 adantl 
 |-  ( ( dom ( y \ _I ) e. Fin /\ y e. B ) -> D e. _V )
41 2 symgid 
 |-  ( D e. _V -> ( _I |` D ) = ( 0g ` G ) )
42 40 41 syl 
 |-  ( ( dom ( y \ _I ) e. Fin /\ y e. B ) -> ( _I |` D ) = ( 0g ` G ) )
43 40 10 syl 
 |-  ( ( dom ( y \ _I ) e. Fin /\ y e. B ) -> ( SubMnd ` G ) e. ( Moore ` B ) )
44 4 mrccl 
 |-  ( ( ( SubMnd ` G ) e. ( Moore ` B ) /\ T C_ B ) -> ( K ` T ) e. ( SubMnd ` G ) )
45 43 12 44 sylancl 
 |-  ( ( dom ( y \ _I ) e. Fin /\ y e. B ) -> ( K ` T ) e. ( SubMnd ` G ) )
46 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
47 46 subm0cl 
 |-  ( ( K ` T ) e. ( SubMnd ` G ) -> ( 0g ` G ) e. ( K ` T ) )
48 45 47 syl 
 |-  ( ( dom ( y \ _I ) e. Fin /\ y e. B ) -> ( 0g ` G ) e. ( K ` T ) )
49 42 48 eqeltrd 
 |-  ( ( dom ( y \ _I ) e. Fin /\ y e. B ) -> ( _I |` D ) e. ( K ` T ) )
50 eleq1a 
 |-  ( ( _I |` D ) e. ( K ` T ) -> ( y = ( _I |` D ) -> y e. ( K ` T ) ) )
51 49 50 syl 
 |-  ( ( dom ( y \ _I ) e. Fin /\ y e. B ) -> ( y = ( _I |` D ) -> y e. ( K ` T ) ) )
52 38 51 sylbid 
 |-  ( ( dom ( y \ _I ) e. Fin /\ y e. B ) -> ( dom ( y \ _I ) = (/) -> y e. ( K ` T ) ) )
53 52 adantr 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ A. z ( dom ( z \ _I ) ~< dom ( y \ _I ) -> ( z e. B -> z e. ( K ` T ) ) ) ) -> ( dom ( y \ _I ) = (/) -> y e. ( K ` T ) ) )
54 n0 
 |-  ( dom ( y \ _I ) =/= (/) <-> E. u u e. dom ( y \ _I ) )
55 40 adantr 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> D e. _V )
56 simpr 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> u e. dom ( y \ _I ) )
57 f1omvdmvd 
 |-  ( ( y : D -1-1-onto-> D /\ u e. dom ( y \ _I ) ) -> ( y ` u ) e. ( dom ( y \ _I ) \ { u } ) )
58 35 57 sylan 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> ( y ` u ) e. ( dom ( y \ _I ) \ { u } ) )
59 58 eldifad 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> ( y ` u ) e. dom ( y \ _I ) )
60 56 59 prssd 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> { u , ( y ` u ) } C_ dom ( y \ _I ) )
61 difss 
 |-  ( y \ _I ) C_ y
62 dmss 
 |-  ( ( y \ _I ) C_ y -> dom ( y \ _I ) C_ dom y )
63 61 62 ax-mp 
 |-  dom ( y \ _I ) C_ dom y
64 f1odm 
 |-  ( y : D -1-1-onto-> D -> dom y = D )
65 35 64 syl 
 |-  ( ( dom ( y \ _I ) e. Fin /\ y e. B ) -> dom y = D )
66 63 65 sseqtrid 
 |-  ( ( dom ( y \ _I ) e. Fin /\ y e. B ) -> dom ( y \ _I ) C_ D )
67 66 adantr 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> dom ( y \ _I ) C_ D )
68 60 67 sstrd 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> { u , ( y ` u ) } C_ D )
69 vex 
 |-  u e. _V
70 fvex 
 |-  ( y ` u ) e. _V
71 35 adantr 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> y : D -1-1-onto-> D )
72 71 36 syl 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> y Fn D )
73 66 sselda 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> u e. D )
74 fnelnfp 
 |-  ( ( y Fn D /\ u e. D ) -> ( u e. dom ( y \ _I ) <-> ( y ` u ) =/= u ) )
75 72 73 74 syl2anc 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> ( u e. dom ( y \ _I ) <-> ( y ` u ) =/= u ) )
76 56 75 mpbid 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> ( y ` u ) =/= u )
77 76 necomd 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> u =/= ( y ` u ) )
78 pr2nelem 
 |-  ( ( u e. _V /\ ( y ` u ) e. _V /\ u =/= ( y ` u ) ) -> { u , ( y ` u ) } ~~ 2o )
79 69 70 77 78 mp3an12i 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> { u , ( y ` u ) } ~~ 2o )
80 17 1 pmtrrn 
 |-  ( ( D e. _V /\ { u , ( y ` u ) } C_ D /\ { u , ( y ` u ) } ~~ 2o ) -> ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) e. T )
81 55 68 79 80 syl3anc 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) e. T )
82 12 81 sselid 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) e. B )
83 simplr 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> y e. B )
84 eqid 
 |-  ( +g ` G ) = ( +g ` G )
85 2 3 84 symgov 
 |-  ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) e. B /\ y e. B ) -> ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) = ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) )
86 82 83 85 syl2anc 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) = ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) )
87 86 oveq2d 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) ) = ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) ) )
88 40 6 syl 
 |-  ( ( dom ( y \ _I ) e. Fin /\ y e. B ) -> G e. Grp )
89 88 adantr 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> G e. Grp )
90 3 84 grpcl 
 |-  ( ( G e. Grp /\ ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) e. B /\ y e. B ) -> ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) e. B )
91 89 82 83 90 syl3anc 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) e. B )
92 86 91 eqeltrrd 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) e. B )
93 2 3 84 symgov 
 |-  ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) e. B /\ ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) e. B ) -> ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) ) = ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) ) )
94 82 92 93 syl2anc 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) ) = ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) ) )
95 coass 
 |-  ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ) o. y ) = ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) )
96 17 1 pmtrfinv 
 |-  ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) e. T -> ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ) = ( _I |` D ) )
97 81 96 syl 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ) = ( _I |` D ) )
98 97 coeq1d 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ) o. y ) = ( ( _I |` D ) o. y ) )
99 f1of 
 |-  ( y : D -1-1-onto-> D -> y : D --> D )
100 fcoi2 
 |-  ( y : D --> D -> ( ( _I |` D ) o. y ) = y )
101 71 99 100 3syl 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> ( ( _I |` D ) o. y ) = y )
102 98 101 eqtrd 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ) o. y ) = y )
103 95 102 eqtr3id 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) ) = y )
104 87 94 103 3eqtrd 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) ) = y )
105 104 adantlr 
 |-  ( ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ A. z ( dom ( z \ _I ) ~< dom ( y \ _I ) -> ( z e. B -> z e. ( K ` T ) ) ) ) /\ u e. dom ( y \ _I ) ) -> ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) ) = y )
106 45 ad2antrr 
 |-  ( ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ A. z ( dom ( z \ _I ) ~< dom ( y \ _I ) -> ( z e. B -> z e. ( K ` T ) ) ) ) /\ u e. dom ( y \ _I ) ) -> ( K ` T ) e. ( SubMnd ` G ) )
107 4 mrcssid 
 |-  ( ( ( SubMnd ` G ) e. ( Moore ` B ) /\ T C_ B ) -> T C_ ( K ` T ) )
108 43 12 107 sylancl 
 |-  ( ( dom ( y \ _I ) e. Fin /\ y e. B ) -> T C_ ( K ` T ) )
109 108 adantr 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> T C_ ( K ` T ) )
110 109 81 sseldd 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) e. ( K ` T ) )
111 110 adantlr 
 |-  ( ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ A. z ( dom ( z \ _I ) ~< dom ( y \ _I ) -> ( z e. B -> z e. ( K ` T ) ) ) ) /\ u e. dom ( y \ _I ) ) -> ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) e. ( K ` T ) )
112 86 difeq1d 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) \ _I ) = ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) \ _I ) )
113 112 dmeqd 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> dom ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) \ _I ) = dom ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) \ _I ) )
114 simpll 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> dom ( y \ _I ) e. Fin )
115 mvdco 
 |-  dom ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) \ _I ) C_ ( dom ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) \ _I ) u. dom ( y \ _I ) )
116 17 pmtrmvd 
 |-  ( ( D e. _V /\ { u , ( y ` u ) } C_ D /\ { u , ( y ` u ) } ~~ 2o ) -> dom ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) \ _I ) = { u , ( y ` u ) } )
117 55 68 79 116 syl3anc 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> dom ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) \ _I ) = { u , ( y ` u ) } )
118 117 60 eqsstrd 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> dom ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) \ _I ) C_ dom ( y \ _I ) )
119 ssidd 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> dom ( y \ _I ) C_ dom ( y \ _I ) )
120 118 119 unssd 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> ( dom ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) \ _I ) u. dom ( y \ _I ) ) C_ dom ( y \ _I ) )
121 115 120 sstrid 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> dom ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) \ _I ) C_ dom ( y \ _I ) )
122 fvco2 
 |-  ( ( y Fn D /\ u e. D ) -> ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) ` u ) = ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ` ( y ` u ) ) )
123 72 73 122 syl2anc 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) ` u ) = ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ` ( y ` u ) ) )
124 prcom 
 |-  { u , ( y ` u ) } = { ( y ` u ) , u }
125 124 fveq2i 
 |-  ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) = ( ( pmTrsp ` D ) ` { ( y ` u ) , u } )
126 125 fveq1i 
 |-  ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ` ( y ` u ) ) = ( ( ( pmTrsp ` D ) ` { ( y ` u ) , u } ) ` ( y ` u ) )
127 67 59 sseldd 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> ( y ` u ) e. D )
128 17 pmtrprfv 
 |-  ( ( D e. _V /\ ( ( y ` u ) e. D /\ u e. D /\ ( y ` u ) =/= u ) ) -> ( ( ( pmTrsp ` D ) ` { ( y ` u ) , u } ) ` ( y ` u ) ) = u )
129 55 127 73 76 128 syl13anc 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> ( ( ( pmTrsp ` D ) ` { ( y ` u ) , u } ) ` ( y ` u ) ) = u )
130 126 129 eqtrid 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ` ( y ` u ) ) = u )
131 123 130 eqtrd 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) ` u ) = u )
132 2 3 symgbasf1o 
 |-  ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) e. B -> ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) : D -1-1-onto-> D )
133 f1ofn 
 |-  ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) : D -1-1-onto-> D -> ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) Fn D )
134 92 132 133 3syl 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) Fn D )
135 fnelnfp 
 |-  ( ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) Fn D /\ u e. D ) -> ( u e. dom ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) \ _I ) <-> ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) ` u ) =/= u ) )
136 135 necon2bbid 
 |-  ( ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) Fn D /\ u e. D ) -> ( ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) ` u ) = u <-> -. u e. dom ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) \ _I ) ) )
137 134 73 136 syl2anc 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> ( ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) ` u ) = u <-> -. u e. dom ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) \ _I ) ) )
138 131 137 mpbid 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> -. u e. dom ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) \ _I ) )
139 121 56 138 ssnelpssd 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> dom ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) \ _I ) C. dom ( y \ _I ) )
140 php3 
 |-  ( ( dom ( y \ _I ) e. Fin /\ dom ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) \ _I ) C. dom ( y \ _I ) ) -> dom ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) \ _I ) ~< dom ( y \ _I ) )
141 114 139 140 syl2anc 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> dom ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) o. y ) \ _I ) ~< dom ( y \ _I ) )
142 113 141 eqbrtrd 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ u e. dom ( y \ _I ) ) -> dom ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) \ _I ) ~< dom ( y \ _I ) )
143 142 adantlr 
 |-  ( ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ A. z ( dom ( z \ _I ) ~< dom ( y \ _I ) -> ( z e. B -> z e. ( K ` T ) ) ) ) /\ u e. dom ( y \ _I ) ) -> dom ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) \ _I ) ~< dom ( y \ _I ) )
144 91 adantlr 
 |-  ( ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ A. z ( dom ( z \ _I ) ~< dom ( y \ _I ) -> ( z e. B -> z e. ( K ` T ) ) ) ) /\ u e. dom ( y \ _I ) ) -> ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) e. B )
145 ovex 
 |-  ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) e. _V
146 difeq1 
 |-  ( z = ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) -> ( z \ _I ) = ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) \ _I ) )
147 146 dmeqd 
 |-  ( z = ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) -> dom ( z \ _I ) = dom ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) \ _I ) )
148 147 breq1d 
 |-  ( z = ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) -> ( dom ( z \ _I ) ~< dom ( y \ _I ) <-> dom ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) \ _I ) ~< dom ( y \ _I ) ) )
149 eleq1 
 |-  ( z = ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) -> ( z e. B <-> ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) e. B ) )
150 eleq1 
 |-  ( z = ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) -> ( z e. ( K ` T ) <-> ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) e. ( K ` T ) ) )
151 149 150 imbi12d 
 |-  ( z = ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) -> ( ( z e. B -> z e. ( K ` T ) ) <-> ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) e. B -> ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) e. ( K ` T ) ) ) )
152 148 151 imbi12d 
 |-  ( z = ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) -> ( ( dom ( z \ _I ) ~< dom ( y \ _I ) -> ( z e. B -> z e. ( K ` T ) ) ) <-> ( dom ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) \ _I ) ~< dom ( y \ _I ) -> ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) e. B -> ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) e. ( K ` T ) ) ) ) )
153 145 152 spcv 
 |-  ( A. z ( dom ( z \ _I ) ~< dom ( y \ _I ) -> ( z e. B -> z e. ( K ` T ) ) ) -> ( dom ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) \ _I ) ~< dom ( y \ _I ) -> ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) e. B -> ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) e. ( K ` T ) ) ) )
154 153 ad2antlr 
 |-  ( ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ A. z ( dom ( z \ _I ) ~< dom ( y \ _I ) -> ( z e. B -> z e. ( K ` T ) ) ) ) /\ u e. dom ( y \ _I ) ) -> ( dom ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) \ _I ) ~< dom ( y \ _I ) -> ( ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) e. B -> ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) e. ( K ` T ) ) ) )
155 143 144 154 mp2d 
 |-  ( ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ A. z ( dom ( z \ _I ) ~< dom ( y \ _I ) -> ( z e. B -> z e. ( K ` T ) ) ) ) /\ u e. dom ( y \ _I ) ) -> ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) e. ( K ` T ) )
156 84 submcl 
 |-  ( ( ( K ` T ) e. ( SubMnd ` G ) /\ ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) e. ( K ` T ) /\ ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) e. ( K ` T ) ) -> ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) ) e. ( K ` T ) )
157 106 111 155 156 syl3anc 
 |-  ( ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ A. z ( dom ( z \ _I ) ~< dom ( y \ _I ) -> ( z e. B -> z e. ( K ` T ) ) ) ) /\ u e. dom ( y \ _I ) ) -> ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) ( ( ( pmTrsp ` D ) ` { u , ( y ` u ) } ) ( +g ` G ) y ) ) e. ( K ` T ) )
158 105 157 eqeltrrd 
 |-  ( ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ A. z ( dom ( z \ _I ) ~< dom ( y \ _I ) -> ( z e. B -> z e. ( K ` T ) ) ) ) /\ u e. dom ( y \ _I ) ) -> y e. ( K ` T ) )
159 158 ex 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ A. z ( dom ( z \ _I ) ~< dom ( y \ _I ) -> ( z e. B -> z e. ( K ` T ) ) ) ) -> ( u e. dom ( y \ _I ) -> y e. ( K ` T ) ) )
160 159 exlimdv 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ A. z ( dom ( z \ _I ) ~< dom ( y \ _I ) -> ( z e. B -> z e. ( K ` T ) ) ) ) -> ( E. u u e. dom ( y \ _I ) -> y e. ( K ` T ) ) )
161 54 160 syl5bi 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ A. z ( dom ( z \ _I ) ~< dom ( y \ _I ) -> ( z e. B -> z e. ( K ` T ) ) ) ) -> ( dom ( y \ _I ) =/= (/) -> y e. ( K ` T ) ) )
162 53 161 pm2.61dne 
 |-  ( ( ( dom ( y \ _I ) e. Fin /\ y e. B ) /\ A. z ( dom ( z \ _I ) ~< dom ( y \ _I ) -> ( z e. B -> z e. ( K ` T ) ) ) ) -> y e. ( K ` T ) )
163 162 exp31 
 |-  ( dom ( y \ _I ) e. Fin -> ( y e. B -> ( A. z ( dom ( z \ _I ) ~< dom ( y \ _I ) -> ( z e. B -> z e. ( K ` T ) ) ) -> y e. ( K ` T ) ) ) )
164 163 com23 
 |-  ( dom ( y \ _I ) e. Fin -> ( A. z ( dom ( z \ _I ) ~< dom ( y \ _I ) -> ( z e. B -> z e. ( K ` T ) ) ) -> ( y e. B -> y e. ( K ` T ) ) ) )
165 33 164 syl 
 |-  ( ( dom ( x \ _I ) e. Fin /\ dom ( y \ _I ) ~<_ dom ( x \ _I ) ) -> ( A. z ( dom ( z \ _I ) ~< dom ( y \ _I ) -> ( z e. B -> z e. ( K ` T ) ) ) -> ( y e. B -> y e. ( K ` T ) ) ) )
166 165 3impia 
 |-  ( ( dom ( x \ _I ) e. Fin /\ dom ( y \ _I ) ~<_ dom ( x \ _I ) /\ A. z ( dom ( z \ _I ) ~< dom ( y \ _I ) -> ( z e. B -> z e. ( K ` T ) ) ) ) -> ( y e. B -> y e. ( K ` T ) ) )
167 eleq1w 
 |-  ( y = z -> ( y e. B <-> z e. B ) )
168 eleq1w 
 |-  ( y = z -> ( y e. ( K ` T ) <-> z e. ( K ` T ) ) )
169 167 168 imbi12d 
 |-  ( y = z -> ( ( y e. B -> y e. ( K ` T ) ) <-> ( z e. B -> z e. ( K ` T ) ) ) )
170 eleq1w 
 |-  ( y = x -> ( y e. B <-> x e. B ) )
171 eleq1w 
 |-  ( y = x -> ( y e. ( K ` T ) <-> x e. ( K ` T ) ) )
172 170 171 imbi12d 
 |-  ( y = x -> ( ( y e. B -> y e. ( K ` T ) ) <-> ( x e. B -> x e. ( K ` T ) ) ) )
173 difeq1 
 |-  ( y = z -> ( y \ _I ) = ( z \ _I ) )
174 173 dmeqd 
 |-  ( y = z -> dom ( y \ _I ) = dom ( z \ _I ) )
175 difeq1 
 |-  ( y = x -> ( y \ _I ) = ( x \ _I ) )
176 175 dmeqd 
 |-  ( y = x -> dom ( y \ _I ) = dom ( x \ _I ) )
177 31 32 166 169 172 174 176 indcardi 
 |-  ( dom ( x \ _I ) e. Fin -> ( x e. B -> x e. ( K ` T ) ) )
178 177 impcom 
 |-  ( ( x e. B /\ dom ( x \ _I ) e. Fin ) -> x e. ( K ` T ) )
179 178 3adant1 
 |-  ( ( D e. V /\ x e. B /\ dom ( x \ _I ) e. Fin ) -> x e. ( K ` T ) )
180 179 rabssdv 
 |-  ( D e. V -> { x e. B | dom ( x \ _I ) e. Fin } C_ ( K ` T ) )
181 29 180 eqssd 
 |-  ( D e. V -> ( K ` T ) = { x e. B | dom ( x \ _I ) e. Fin } )