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)

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 tsetndx ⊢ ( TopSet ‘ ndx ) = 9
88 1re ⊢ 1 ∈ ℝ
89 1lt9 ⊢ 1 < 9
90 88 89 gtneii ⊢ 9 ≠ 1
91 df-base ⊢ Base = Slot 1
92 1nn ⊢ 1 ∈ ℕ
93 91 92 ndxarg ⊢ ( Base ‘ ndx ) = 1
94 90 93 neeqtrri ⊢ 9 ≠ ( Base ‘ ndx )
95 87 94 eqnetri ⊢ ( TopSet ‘ ndx ) ≠ ( Base ‘ ndx )
96 95 a1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → ( TopSet ‘ ndx ) ≠ ( Base ‘ ndx ) )
97 75 76 77 81 83 86 96 tpres ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → ( { ⟨ ( Base ‘ ndx ) , 𝑀 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ↾ ( V ∖ { ( Base ‘ ndx ) } ) ) = { ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )
98 97 uneq1d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → ( ( { ⟨ ( Base ‘ ndx ) , 𝑀 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ↾ ( V ∖ { ( Base ‘ ndx ) } ) ) ∪ { ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( 𝐴 ↑m 𝐴 ) ) ⟩ } ) = ( { ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ∪ { ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( 𝐴 ↑m 𝐴 ) ) ⟩ } ) )
99 uncom ⊢ ( { ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ∪ { ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( 𝐴 ↑m 𝐴 ) ) ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( 𝐴 ↑m 𝐴 ) ) ⟩ } ∪ { ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )
100 tpass ⊢ { ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( 𝐴 ↑m 𝐴 ) ) ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } = ( { ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( 𝐴 ↑m 𝐴 ) ) ⟩ } ∪ { ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )
101 99 100 eqtr4i ⊢ ( { ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ∪ { ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( 𝐴 ↑m 𝐴 ) ) ⟩ } ) = { ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( 𝐴 ↑m 𝐴 ) ) ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ }
102 1 56 symgbasmap ⊢ ( 𝑥 ∈ 𝐵 → 𝑥 ∈ ( 𝐴 ↑m 𝐴 ) )
103 102 a1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → ( 𝑥 ∈ 𝐵 → 𝑥 ∈ ( 𝐴 ↑m 𝐴 ) ) )
104 103 ssrdv ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → 𝐵 ⊆ ( 𝐴 ↑m 𝐴 ) )
105 df-ss ⊢ ( 𝐵 ⊆ ( 𝐴 ↑m 𝐴 ) ↔ ( 𝐵 ∩ ( 𝐴 ↑m 𝐴 ) ) = 𝐵 )
106 104 105 sylib ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → ( 𝐵 ∩ ( 𝐴 ↑m 𝐴 ) ) = 𝐵 )
107 106 opeq2d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( 𝐴 ↑m 𝐴 ) ) ⟩ = ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ )
108 107 tpeq1d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → { ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( 𝐴 ↑m 𝐴 ) ) ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )
109 101 108 eqtrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → ( { ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ∪ { ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( 𝐴 ↑m 𝐴 ) ) ⟩ } ) = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )
110 74 98 109 3eqtrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → ( ( ( EndoFMnd ‘ 𝐴 ) ↾ ( V ∖ { ( Base ‘ ndx ) } ) ) ∪ { ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( 𝐴 ↑m 𝐴 ) ) ⟩ } ) = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )
111 67 71 110 3eqtrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )
112 111 ex ⊢ ( 𝐴 ∈ 𝑉 → ( 1 < ( ♯ ‘ 𝐴 ) → 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ) )
113 34 53 112 3jaod ⊢ ( 𝐴 ∈ 𝑉 → ( ( ( ♯ ‘ 𝐴 ) = 0 ∨ ( ♯ ‘ 𝐴 ) = 1 ∨ 1 < ( ♯ ‘ 𝐴 ) ) → 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ) )
114 6 113 mpd ⊢ ( 𝐴 ∈ 𝑉 → 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )