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