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		vsnex	⊢ { 𝑥 } ∈ 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	biimtrdi	⊢ ( 𝐴 ∈ 𝑉 → ( ( ♯ ‘ 𝐴 ) = 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		dfss2	⊢ ( 𝐵 ⊆ ( 𝐴 ↑_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 ) , 𝐽 ⟩ } )

Metamath Proof Explorer

Theorem symgvalstruct

Proof