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 𝑇 = ran ( pmTrsp ‘ 𝐷 )
symgtrf.g 𝐺 = ( SymGrp ‘ 𝐷 )
symgtrf.b 𝐵 = ( Base ‘ 𝐺 )
symggen.k 𝐾 = ( mrCls ‘ ( SubMnd ‘ 𝐺 ) )
Assertion symggen ( 𝐷𝑉 → ( 𝐾𝑇 ) = { 𝑥𝐵 ∣ dom ( 𝑥 ∖ I ) ∈ Fin } )

Proof

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