This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 enpr2 ⊢ ( ( 𝑢 ∈ 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 eqtrid ⊢ ( ( ( 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 biimtrid ⊢ ( ( ( 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 } )