Metamath Proof Explorer


Theorem symgvalstruct

Description: The value of the symmetric group function at A represented as extensible structure with three slots. This corresponds to the former definition of SymGrp . (Contributed by Paul Chapman, 25-Feb-2008) (Revised by Mario Carneiro, 12-Jan-2015) (Revised by AV, 31-Mar-2024) (Proof shortened by AV, 6-Nov-2024)

Ref Expression
Hypotheses symgvalstruct.g 𝐺 = ( SymGrp ‘ 𝐴 )
symgvalstruct.b 𝐵 = { 𝑥𝑥 : 𝐴1-1-onto𝐴 }
symgvalstruct.m 𝑀 = ( 𝐴m 𝐴 )
symgvalstruct.p + = ( 𝑓𝑀 , 𝑔𝑀 ↦ ( 𝑓𝑔 ) )
symgvalstruct.j 𝐽 = ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) )
Assertion symgvalstruct ( 𝐴𝑉𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )

Proof

Step Hyp Ref Expression
1 symgvalstruct.g 𝐺 = ( SymGrp ‘ 𝐴 )
2 symgvalstruct.b 𝐵 = { 𝑥𝑥 : 𝐴1-1-onto𝐴 }
3 symgvalstruct.m 𝑀 = ( 𝐴m 𝐴 )
4 symgvalstruct.p + = ( 𝑓𝑀 , 𝑔𝑀 ↦ ( 𝑓𝑔 ) )
5 symgvalstruct.j 𝐽 = ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) )
6 hashv01gt1 ( 𝐴𝑉 → ( ( ♯ ‘ 𝐴 ) = 0 ∨ ( ♯ ‘ 𝐴 ) = 1 ∨ 1 < ( ♯ ‘ 𝐴 ) ) )
7 hasheq0 ( 𝐴𝑉 → ( ( ♯ ‘ 𝐴 ) = 0 ↔ 𝐴 = ∅ ) )
8 0symgefmndeq ( EndoFMnd ‘ ∅ ) = ( SymGrp ‘ ∅ )
9 8 eqcomi ( SymGrp ‘ ∅ ) = ( EndoFMnd ‘ ∅ )
10 fveq2 ( 𝐴 = ∅ → ( SymGrp ‘ 𝐴 ) = ( SymGrp ‘ ∅ ) )
11 1 10 eqtrid ( 𝐴 = ∅ → 𝐺 = ( SymGrp ‘ ∅ ) )
12 fveq2 ( 𝐴 = ∅ → ( EndoFMnd ‘ 𝐴 ) = ( EndoFMnd ‘ ∅ ) )
13 9 11 12 3eqtr4a ( 𝐴 = ∅ → 𝐺 = ( EndoFMnd ‘ 𝐴 ) )
14 13 adantl ( ( 𝐴𝑉𝐴 = ∅ ) → 𝐺 = ( EndoFMnd ‘ 𝐴 ) )
15 eqid ( EndoFMnd ‘ 𝐴 ) = ( EndoFMnd ‘ 𝐴 )
16 15 3 4 5 efmnd ( 𝐴𝑉 → ( EndoFMnd ‘ 𝐴 ) = { ⟨ ( Base ‘ ndx ) , 𝑀 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )
17 16 adantr ( ( 𝐴𝑉𝐴 = ∅ ) → ( EndoFMnd ‘ 𝐴 ) = { ⟨ ( Base ‘ ndx ) , 𝑀 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )
18 0map0sn0 ( ∅ ↑m ∅ ) = { ∅ }
19 id ( 𝐴 = ∅ → 𝐴 = ∅ )
20 19 19 oveq12d ( 𝐴 = ∅ → ( 𝐴m 𝐴 ) = ( ∅ ↑m ∅ ) )
21 11 fveq2d ( 𝐴 = ∅ → ( Base ‘ 𝐺 ) = ( Base ‘ ( SymGrp ‘ ∅ ) ) )
22 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
23 1 22 symgbas ( Base ‘ 𝐺 ) = { 𝑥𝑥 : 𝐴1-1-onto𝐴 }
24 symgbas0 ( Base ‘ ( SymGrp ‘ ∅ ) ) = { ∅ }
25 21 23 24 3eqtr3g ( 𝐴 = ∅ → { 𝑥𝑥 : 𝐴1-1-onto𝐴 } = { ∅ } )
26 2 25 eqtrid ( 𝐴 = ∅ → 𝐵 = { ∅ } )
27 18 20 26 3eqtr4a ( 𝐴 = ∅ → ( 𝐴m 𝐴 ) = 𝐵 )
28 27 adantl ( ( 𝐴𝑉𝐴 = ∅ ) → ( 𝐴m 𝐴 ) = 𝐵 )
29 3 28 eqtrid ( ( 𝐴𝑉𝐴 = ∅ ) → 𝑀 = 𝐵 )
30 29 opeq2d ( ( 𝐴𝑉𝐴 = ∅ ) → ⟨ ( Base ‘ ndx ) , 𝑀 ⟩ = ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ )
31 30 tpeq1d ( ( 𝐴𝑉𝐴 = ∅ ) → { ⟨ ( Base ‘ ndx ) , 𝑀 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )
32 14 17 31 3eqtrd ( ( 𝐴𝑉𝐴 = ∅ ) → 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )
33 32 ex ( 𝐴𝑉 → ( 𝐴 = ∅ → 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ) )
34 7 33 sylbid ( 𝐴𝑉 → ( ( ♯ ‘ 𝐴 ) = 0 → 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ) )
35 hash1snb ( 𝐴𝑉 → ( ( ♯ ‘ 𝐴 ) = 1 ↔ ∃ 𝑥 𝐴 = { 𝑥 } ) )
36 snex { 𝑥 } ∈ V
37 eleq1 ( 𝐴 = { 𝑥 } → ( 𝐴 ∈ V ↔ { 𝑥 } ∈ V ) )
38 36 37 mpbiri ( 𝐴 = { 𝑥 } → 𝐴 ∈ V )
39 15 3 4 5 efmnd ( 𝐴 ∈ V → ( EndoFMnd ‘ 𝐴 ) = { ⟨ ( Base ‘ ndx ) , 𝑀 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )
40 38 39 syl ( 𝐴 = { 𝑥 } → ( EndoFMnd ‘ 𝐴 ) = { ⟨ ( Base ‘ ndx ) , 𝑀 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )
41 snsymgefmndeq ( 𝐴 = { 𝑥 } → ( EndoFMnd ‘ 𝐴 ) = ( SymGrp ‘ 𝐴 ) )
42 41 1 eqtr4di ( 𝐴 = { 𝑥 } → ( EndoFMnd ‘ 𝐴 ) = 𝐺 )
43 42 fveq2d ( 𝐴 = { 𝑥 } → ( Base ‘ ( EndoFMnd ‘ 𝐴 ) ) = ( Base ‘ 𝐺 ) )
44 eqid ( Base ‘ ( EndoFMnd ‘ 𝐴 ) ) = ( Base ‘ ( EndoFMnd ‘ 𝐴 ) )
45 15 44 efmndbas ( Base ‘ ( EndoFMnd ‘ 𝐴 ) ) = ( 𝐴m 𝐴 )
46 45 3 eqtr4i ( Base ‘ ( EndoFMnd ‘ 𝐴 ) ) = 𝑀
47 23 2 eqtr4i ( Base ‘ 𝐺 ) = 𝐵
48 43 46 47 3eqtr3g ( 𝐴 = { 𝑥 } → 𝑀 = 𝐵 )
49 48 opeq2d ( 𝐴 = { 𝑥 } → ⟨ ( Base ‘ ndx ) , 𝑀 ⟩ = ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ )
50 49 tpeq1d ( 𝐴 = { 𝑥 } → { ⟨ ( Base ‘ ndx ) , 𝑀 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )
51 40 42 50 3eqtr3d ( 𝐴 = { 𝑥 } → 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )
52 51 exlimiv ( ∃ 𝑥 𝐴 = { 𝑥 } → 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )
53 35 52 syl6bi ( 𝐴𝑉 → ( ( ♯ ‘ 𝐴 ) = 1 → 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ) )
54 ssnpss ( ( 𝐴m 𝐴 ) ⊆ 𝐵 → ¬ 𝐵 ⊊ ( 𝐴m 𝐴 ) )
55 15 1 symgpssefmnd ( ( 𝐴𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → ( Base ‘ 𝐺 ) ⊊ ( Base ‘ ( EndoFMnd ‘ 𝐴 ) ) )
56 2 23 eqtr4i 𝐵 = ( Base ‘ 𝐺 )
57 45 eqcomi ( 𝐴m 𝐴 ) = ( Base ‘ ( EndoFMnd ‘ 𝐴 ) )
58 56 57 psseq12i ( 𝐵 ⊊ ( 𝐴m 𝐴 ) ↔ ( Base ‘ 𝐺 ) ⊊ ( Base ‘ ( EndoFMnd ‘ 𝐴 ) ) )
59 55 58 sylibr ( ( 𝐴𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → 𝐵 ⊊ ( 𝐴m 𝐴 ) )
60 54 59 nsyl3 ( ( 𝐴𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → ¬ ( 𝐴m 𝐴 ) ⊆ 𝐵 )
61 fvexd ( ( 𝐴𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → ( EndoFMnd ‘ 𝐴 ) ∈ V )
62 f1osetex { 𝑥𝑥 : 𝐴1-1-onto𝐴 } ∈ V
63 2 62 eqeltri 𝐵 ∈ V
64 63 a1i ( ( 𝐴𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → 𝐵 ∈ V )
65 1 2 symgval 𝐺 = ( ( EndoFMnd ‘ 𝐴 ) ↾s 𝐵 )
66 65 57 ressval2 ( ( ¬ ( 𝐴m 𝐴 ) ⊆ 𝐵 ∧ ( EndoFMnd ‘ 𝐴 ) ∈ V ∧ 𝐵 ∈ V ) → 𝐺 = ( ( EndoFMnd ‘ 𝐴 ) sSet ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( 𝐴m 𝐴 ) ) ⟩ ) )
67 60 61 64 66 syl3anc ( ( 𝐴𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → 𝐺 = ( ( EndoFMnd ‘ 𝐴 ) sSet ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( 𝐴m 𝐴 ) ) ⟩ ) )
68 ovex ( 𝐴m 𝐴 ) ∈ V
69 68 inex2 ( 𝐵 ∩ ( 𝐴m 𝐴 ) ) ∈ V
70 setsval ( ( ( EndoFMnd ‘ 𝐴 ) ∈ V ∧ ( 𝐵 ∩ ( 𝐴m 𝐴 ) ) ∈ V ) → ( ( EndoFMnd ‘ 𝐴 ) sSet ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( 𝐴m 𝐴 ) ) ⟩ ) = ( ( ( EndoFMnd ‘ 𝐴 ) ↾ ( V ∖ { ( Base ‘ ndx ) } ) ) ∪ { ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( 𝐴m 𝐴 ) ) ⟩ } ) )
71 61 69 70 sylancl ( ( 𝐴𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → ( ( EndoFMnd ‘ 𝐴 ) sSet ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( 𝐴m 𝐴 ) ) ⟩ ) = ( ( ( EndoFMnd ‘ 𝐴 ) ↾ ( V ∖ { ( Base ‘ ndx ) } ) ) ∪ { ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( 𝐴m 𝐴 ) ) ⟩ } ) )
72 16 adantr ( ( 𝐴𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → ( EndoFMnd ‘ 𝐴 ) = { ⟨ ( Base ‘ ndx ) , 𝑀 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )
73 72 reseq1d ( ( 𝐴𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → ( ( EndoFMnd ‘ 𝐴 ) ↾ ( V ∖ { ( Base ‘ ndx ) } ) ) = ( { ⟨ ( Base ‘ ndx ) , 𝑀 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ↾ ( V ∖ { ( Base ‘ ndx ) } ) ) )
74 73 uneq1d ( ( 𝐴𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → ( ( ( EndoFMnd ‘ 𝐴 ) ↾ ( V ∖ { ( Base ‘ ndx ) } ) ) ∪ { ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( 𝐴m 𝐴 ) ) ⟩ } ) = ( ( { ⟨ ( Base ‘ ndx ) , 𝑀 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ↾ ( V ∖ { ( Base ‘ ndx ) } ) ) ∪ { ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( 𝐴m 𝐴 ) ) ⟩ } ) )
75 eqidd ( ( 𝐴𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → { ⟨ ( Base ‘ ndx ) , 𝑀 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝑀 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )
76 fvexd ( ( 𝐴𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → ( +g ‘ ndx ) ∈ V )
77 fvexd ( ( 𝐴𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → ( TopSet ‘ ndx ) ∈ V )
78 3 68 eqeltri 𝑀 ∈ V
79 78 78 mpoex ( 𝑓𝑀 , 𝑔𝑀 ↦ ( 𝑓𝑔 ) ) ∈ V
80 4 79 eqeltri + ∈ V
81 80 a1i ( ( 𝐴𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → + ∈ V )
82 5 fvexi 𝐽 ∈ V
83 82 a1i ( ( 𝐴𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → 𝐽 ∈ V )
84 basendxnplusgndx ( Base ‘ ndx ) ≠ ( +g ‘ ndx )
85 84 necomi ( +g ‘ ndx ) ≠ ( Base ‘ ndx )
86 85 a1i ( ( 𝐴𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → ( +g ‘ ndx ) ≠ ( Base ‘ ndx ) )
87 tsetndxnbasendx ( TopSet ‘ ndx ) ≠ ( Base ‘ ndx )
88 87 a1i ( ( 𝐴𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → ( TopSet ‘ ndx ) ≠ ( Base ‘ ndx ) )
89 75 76 77 81 83 86 88 tpres ( ( 𝐴𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → ( { ⟨ ( Base ‘ ndx ) , 𝑀 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ↾ ( V ∖ { ( Base ‘ ndx ) } ) ) = { ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )
90 89 uneq1d ( ( 𝐴𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → ( ( { ⟨ ( Base ‘ ndx ) , 𝑀 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ↾ ( V ∖ { ( Base ‘ ndx ) } ) ) ∪ { ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( 𝐴m 𝐴 ) ) ⟩ } ) = ( { ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ∪ { ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( 𝐴m 𝐴 ) ) ⟩ } ) )
91 uncom ( { ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ∪ { ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( 𝐴m 𝐴 ) ) ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( 𝐴m 𝐴 ) ) ⟩ } ∪ { ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )
92 tpass { ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( 𝐴m 𝐴 ) ) ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } = ( { ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( 𝐴m 𝐴 ) ) ⟩ } ∪ { ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )
93 91 92 eqtr4i ( { ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ∪ { ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( 𝐴m 𝐴 ) ) ⟩ } ) = { ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( 𝐴m 𝐴 ) ) ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ }
94 1 56 symgbasmap ( 𝑥𝐵𝑥 ∈ ( 𝐴m 𝐴 ) )
95 94 a1i ( ( 𝐴𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → ( 𝑥𝐵𝑥 ∈ ( 𝐴m 𝐴 ) ) )
96 95 ssrdv ( ( 𝐴𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → 𝐵 ⊆ ( 𝐴m 𝐴 ) )
97 df-ss ( 𝐵 ⊆ ( 𝐴m 𝐴 ) ↔ ( 𝐵 ∩ ( 𝐴m 𝐴 ) ) = 𝐵 )
98 96 97 sylib ( ( 𝐴𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → ( 𝐵 ∩ ( 𝐴m 𝐴 ) ) = 𝐵 )
99 98 opeq2d ( ( 𝐴𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( 𝐴m 𝐴 ) ) ⟩ = ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ )
100 99 tpeq1d ( ( 𝐴𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → { ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( 𝐴m 𝐴 ) ) ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )
101 93 100 eqtrid ( ( 𝐴𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → ( { ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ∪ { ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( 𝐴m 𝐴 ) ) ⟩ } ) = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )
102 74 90 101 3eqtrd ( ( 𝐴𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → ( ( ( EndoFMnd ‘ 𝐴 ) ↾ ( V ∖ { ( Base ‘ ndx ) } ) ) ∪ { ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( 𝐴m 𝐴 ) ) ⟩ } ) = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )
103 67 71 102 3eqtrd ( ( 𝐴𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )
104 103 ex ( 𝐴𝑉 → ( 1 < ( ♯ ‘ 𝐴 ) → 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ) )
105 34 53 104 3jaod ( 𝐴𝑉 → ( ( ( ♯ ‘ 𝐴 ) = 0 ∨ ( ♯ ‘ 𝐴 ) = 1 ∨ 1 < ( ♯ ‘ 𝐴 ) ) → 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ) )
106 6 105 mpd ( 𝐴𝑉𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )