Theorem symgvalstructOLD

Description: Obsolete version of symgvalstruct as of 6-Nov-2024. 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) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	symgvalstructOLD.g	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
	symgvalstructOLD.b	$$⊢B=\left\{x|x:A\underset{1-1\; onto}{⟶}A\right\}$$
	symgvalstructOLD.m	$$⊢M=A^A$$
	symgvalstructOLD.p	$$⊢\underset{\dot{}}{+}=\left(f\in M,g\in M⟼f\circ g\right)$$
	symgvalstructOLD.j	$$⊢J={\prod }_{𝑡}\left(A\times \left\{𝒫A\right\}\right)$$
Assertion	symgvalstructOLD	$$⊢A\in V\to G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		symgvalstructOLD.g	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
2		symgvalstructOLD.b	$$⊢B=\left\{x|x:A\underset{1-1\; onto}{⟶}A\right\}$$
3		symgvalstructOLD.m	$$⊢M=A^A$$
4		symgvalstructOLD.p	$$⊢\underset{\dot{}}{+}=\left(f\in M,g\in M⟼f\circ g\right)$$
5		symgvalstructOLD.j	$$⊢J={\prod }_{𝑡}\left(A\times \left\{𝒫A\right\}\right)$$
6		hashv01gt1	$$⊢A\in V\to \left(\left|A\right|=0\vee \left|A\right|=1\vee 1<\left|A\right|\right)$$
7		hasheq0	$$⊢A\in V\to \left(\left|A\right|=0\leftrightarrow A=\varnothing \right)$$
8		0symgefmndeq	$$⊢\mathrm{EndoFMnd}\left(\varnothing \right)=\mathrm{SymGrp}\left(\varnothing \right)$$
9	8	eqcomi	$$⊢\mathrm{SymGrp}\left(\varnothing \right)=\mathrm{EndoFMnd}\left(\varnothing \right)$$
10		fveq2	$$⊢A=\varnothing \to \mathrm{SymGrp}\left(A\right)=\mathrm{SymGrp}\left(\varnothing \right)$$
11	1 10	eqtrid	$$⊢A=\varnothing \to G=\mathrm{SymGrp}\left(\varnothing \right)$$
12		fveq2	$$⊢A=\varnothing \to \mathrm{EndoFMnd}\left(A\right)=\mathrm{EndoFMnd}\left(\varnothing \right)$$
13	9 11 12	3eqtr4a	$$⊢A=\varnothing \to G=\mathrm{EndoFMnd}\left(A\right)$$
14	13	adantl	$$⊢\left(A\in V\wedge A=\varnothing \right)\to G=\mathrm{EndoFMnd}\left(A\right)$$
15		eqid	$$⊢\mathrm{EndoFMnd}\left(A\right)=\mathrm{EndoFMnd}\left(A\right)$$
16	15 3 4 5	efmnd	$$⊢A\in V\to \mathrm{EndoFMnd}\left(A\right)=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},M⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}$$
17	16	adantr	$$⊢\left(A\in V\wedge A=\varnothing \right)\to \mathrm{EndoFMnd}\left(A\right)=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},M⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}$$
18		0map0sn0	$$⊢{\varnothing }^{\varnothing }=\left\{\varnothing \right\}$$
19		id	$$⊢A=\varnothing \to A=\varnothing$$
20	19 19	oveq12d	$$⊢A=\varnothing \to A^A={\varnothing }^{\varnothing }$$
21	11	fveq2d	$$⊢A=\varnothing \to {\mathrm{Base}}_G={\mathrm{Base}}_{\mathrm{SymGrp}\left(\varnothing \right)}$$
22		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
23	1 22	symgbas	$$⊢{\mathrm{Base}}_G=\left\{x|x:A\underset{1-1\; onto}{⟶}A\right\}$$
24		symgbas0	$$⊢{\mathrm{Base}}_{\mathrm{SymGrp}\left(\varnothing \right)}=\left\{\varnothing \right\}$$
25	21 23 24	3eqtr3g	$$⊢A=\varnothing \to \left\{x|x:A\underset{1-1\; onto}{⟶}A\right\}=\left\{\varnothing \right\}$$
26	2 25	eqtrid	$$⊢A=\varnothing \to B=\left\{\varnothing \right\}$$
27	18 20 26	3eqtr4a	$$⊢A=\varnothing \to A^A=B$$
28	27	adantl	$$⊢\left(A\in V\wedge A=\varnothing \right)\to A^A=B$$
29	3 28	eqtrid	$$⊢\left(A\in V\wedge A=\varnothing \right)\to M=B$$
30	29	opeq2d	$$⊢\left(A\in V\wedge A=\varnothing \right)\to ⟨{\mathrm{Base}}_{\mathrm{ndx}},M⟩=⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩$$
31	30	tpeq1d	$$⊢\left(A\in V\wedge A=\varnothing \right)\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},M⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}$$
32	14 17 31	3eqtrd	$$⊢\left(A\in V\wedge A=\varnothing \right)\to G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}$$
33	32	ex	$$⊢A\in V\to \left(A=\varnothing \to G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}\right)$$
34	7 33	sylbid	$$⊢A\in V\to \left(\left|A\right|=0\to G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}\right)$$
35		hash1snb	$$⊢A\in V\to \left(\left|A\right|=1\leftrightarrow \exists xA=\left\{x\right\}\right)$$
36		snex	$$⊢\left\{x\right\}\in \mathrm{V}$$
37		eleq1	$$⊢A=\left\{x\right\}\to \left(A\in \mathrm{V}\leftrightarrow \left\{x\right\}\in \mathrm{V}\right)$$
38	36 37	mpbiri	$$⊢A=\left\{x\right\}\to A\in \mathrm{V}$$
39	15 3 4 5	efmnd	$$⊢A\in \mathrm{V}\to \mathrm{EndoFMnd}\left(A\right)=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},M⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}$$
40	38 39	syl	$$⊢A=\left\{x\right\}\to \mathrm{EndoFMnd}\left(A\right)=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},M⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}$$
41		snsymgefmndeq	$$⊢A=\left\{x\right\}\to \mathrm{EndoFMnd}\left(A\right)=\mathrm{SymGrp}\left(A\right)$$
42	41 1	eqtr4di	$$⊢A=\left\{x\right\}\to \mathrm{EndoFMnd}\left(A\right)=G$$
43	42	fveq2d	$$⊢A=\left\{x\right\}\to {\mathrm{Base}}_{\mathrm{EndoFMnd}\left(A\right)}={\mathrm{Base}}_G$$
44		eqid	$$⊢{\mathrm{Base}}_{\mathrm{EndoFMnd}\left(A\right)}={\mathrm{Base}}_{\mathrm{EndoFMnd}\left(A\right)}$$
45	15 44	efmndbas	$$⊢{\mathrm{Base}}_{\mathrm{EndoFMnd}\left(A\right)}=A^A$$
46	45 3	eqtr4i	$$⊢{\mathrm{Base}}_{\mathrm{EndoFMnd}\left(A\right)}=M$$
47	23 2	eqtr4i	$$⊢{\mathrm{Base}}_G=B$$
48	43 46 47	3eqtr3g	$$⊢A=\left\{x\right\}\to M=B$$
49	48	opeq2d	$$⊢A=\left\{x\right\}\to ⟨{\mathrm{Base}}_{\mathrm{ndx}},M⟩=⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩$$
50	49	tpeq1d	$$⊢A=\left\{x\right\}\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},M⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}$$
51	40 42 50	3eqtr3d	$$⊢A=\left\{x\right\}\to G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}$$
52	51	exlimiv	$$⊢\exists xA=\left\{x\right\}\to G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}$$
53	35 52	biimtrdi	$$⊢A\in V\to \left(\left|A\right|=1\to G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}\right)$$
54		ssnpss	$$⊢A^A\subseteq B\to \neg B\subset A^A$$
55	15 1	symgpssefmnd	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to {\mathrm{Base}}_G\subset {\mathrm{Base}}_{\mathrm{EndoFMnd}\left(A\right)}$$
56	2 23	eqtr4i	$$⊢B={\mathrm{Base}}_G$$
57	45	eqcomi	$$⊢A^A={\mathrm{Base}}_{\mathrm{EndoFMnd}\left(A\right)}$$
58	56 57	psseq12i	$$⊢B\subset A^A\leftrightarrow {\mathrm{Base}}_G\subset {\mathrm{Base}}_{\mathrm{EndoFMnd}\left(A\right)}$$
59	55 58	sylibr	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to B\subset A^A$$
60	54 59	nsyl3	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to \neg A^A\subseteq B$$
61		fvexd	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to \mathrm{EndoFMnd}\left(A\right)\in \mathrm{V}$$
62		f1osetex	$$⊢\left\{x|x:A\underset{1-1\; onto}{⟶}A\right\}\in \mathrm{V}$$
63	2 62	eqeltri	$$⊢B\in \mathrm{V}$$
64	63	a1i	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to B\in \mathrm{V}$$
65	1 2	symgval	$$⊢G=\mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}B$$
66	65 57	ressval2	$$⊢\left(\neg A^A\subseteq B\wedge \mathrm{EndoFMnd}\left(A\right)\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to G=\mathrm{EndoFMnd}\left(A\right)\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},B\cap \left(A^A\right)⟩$$
67	60 61 64 66	syl3anc	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to G=\mathrm{EndoFMnd}\left(A\right)\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},B\cap \left(A^A\right)⟩$$
68		ovex	$$⊢A^A\in \mathrm{V}$$
69	68	inex2	$$⊢B\cap \left(A^A\right)\in \mathrm{V}$$
70		setsval	$$⊢\left(\mathrm{EndoFMnd}\left(A\right)\in \mathrm{V}\wedge B\cap \left(A^A\right)\in \mathrm{V}\right)\to \mathrm{EndoFMnd}\left(A\right)\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},B\cap \left(A^A\right)⟩=\left({\mathrm{EndoFMnd}\left(A\right)\upharpoonright }_{\left(\mathrm{V}\setminus \left\{{\mathrm{Base}}_{\mathrm{ndx}}\right\}\right)}\right)\cup \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\cap \left(A^A\right)⟩\right\}$$
71	61 69 70	sylancl	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to \mathrm{EndoFMnd}\left(A\right)\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},B\cap \left(A^A\right)⟩=\left({\mathrm{EndoFMnd}\left(A\right)\upharpoonright }_{\left(\mathrm{V}\setminus \left\{{\mathrm{Base}}_{\mathrm{ndx}}\right\}\right)}\right)\cup \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\cap \left(A^A\right)⟩\right\}$$
72	16	adantr	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to \mathrm{EndoFMnd}\left(A\right)=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},M⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}$$
73	72	reseq1d	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to {\mathrm{EndoFMnd}\left(A\right)\upharpoonright }_{\left(\mathrm{V}\setminus \left\{{\mathrm{Base}}_{\mathrm{ndx}}\right\}\right)}={\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},M⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}\upharpoonright }_{\left(\mathrm{V}\setminus \left\{{\mathrm{Base}}_{\mathrm{ndx}}\right\}\right)}$$
74	73	uneq1d	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to \left({\mathrm{EndoFMnd}\left(A\right)\upharpoonright }_{\left(\mathrm{V}\setminus \left\{{\mathrm{Base}}_{\mathrm{ndx}}\right\}\right)}\right)\cup \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\cap \left(A^A\right)⟩\right\}=\left({\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},M⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}\upharpoonright }_{\left(\mathrm{V}\setminus \left\{{\mathrm{Base}}_{\mathrm{ndx}}\right\}\right)}\right)\cup \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\cap \left(A^A\right)⟩\right\}$$
75		eqidd	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},M⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},M⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}$$
76		fvexd	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to {+}_{\mathrm{ndx}}\in \mathrm{V}$$
77		fvexd	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to \mathrm{TopSet}\left(\mathrm{ndx}\right)\in \mathrm{V}$$
78	3 68	eqeltri	$$⊢M\in \mathrm{V}$$
79	78 78	mpoex	$$⊢\left(f\in M,g\in M⟼f\circ g\right)\in \mathrm{V}$$
80	4 79	eqeltri	$$⊢\underset{\dot{}}{+}\in \mathrm{V}$$
81	80	a1i	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to \underset{\dot{}}{+}\in \mathrm{V}$$
82	5	fvexi	$$⊢J\in \mathrm{V}$$
83	82	a1i	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to J\in \mathrm{V}$$
84		basendxnplusgndx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne {+}_{\mathrm{ndx}}$$
85	84	necomi	$$⊢{+}_{\mathrm{ndx}}\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
86	85	a1i	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to {+}_{\mathrm{ndx}}\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
87		tsetndx	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)=9$$
88		1re	$$⊢1\in ℝ$$
89		1lt9	$$⊢1<9$$
90	88 89	gtneii	$$⊢9\ne 1$$
91		df-base	$$⊢\mathrm{Base}=\mathrm{Slot}1$$
92		1nn	$$⊢1\in \mathbb{N}$$
93	91 92	ndxarg	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}=1$$
94	90 93	neeqtrri	$$⊢9\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
95	87 94	eqnetri	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
96	95	a1i	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to \mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
97	75 76 77 81 83 86 96	tpres	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to {\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},M⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}\upharpoonright }_{\left(\mathrm{V}\setminus \left\{{\mathrm{Base}}_{\mathrm{ndx}}\right\}\right)}=\left\{⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}$$
98	97	uneq1d	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to \left({\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},M⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}\upharpoonright }_{\left(\mathrm{V}\setminus \left\{{\mathrm{Base}}_{\mathrm{ndx}}\right\}\right)}\right)\cup \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\cap \left(A^A\right)⟩\right\}=\left\{⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}\cup \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\cap \left(A^A\right)⟩\right\}$$
99		uncom	$$⊢\left\{⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}\cup \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\cap \left(A^A\right)⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\cap \left(A^A\right)⟩\right\}\cup \left\{⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}$$
100		tpass	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\cap \left(A^A\right)⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\cap \left(A^A\right)⟩\right\}\cup \left\{⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}$$
101	99 100	eqtr4i	$$⊢\left\{⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}\cup \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\cap \left(A^A\right)⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\cap \left(A^A\right)⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}$$
102	1 56	symgbasmap	$$⊢x\in B\to x\in \left(A^A\right)$$
103	102	a1i	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to \left(x\in B\to x\in \left(A^A\right)\right)$$
104	103	ssrdv	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to B\subseteq A^A$$
105		dfss2	$$⊢B\subseteq A^A\leftrightarrow B\cap \left(A^A\right)=B$$
106	104 105	sylib	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to B\cap \left(A^A\right)=B$$
107	106	opeq2d	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to ⟨{\mathrm{Base}}_{\mathrm{ndx}},B\cap \left(A^A\right)⟩=⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩$$
108	107	tpeq1d	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\cap \left(A^A\right)⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}$$
109	101 108	eqtrid	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to \left\{⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}\cup \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\cap \left(A^A\right)⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}$$
110	74 98 109	3eqtrd	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to \left({\mathrm{EndoFMnd}\left(A\right)\upharpoonright }_{\left(\mathrm{V}\setminus \left\{{\mathrm{Base}}_{\mathrm{ndx}}\right\}\right)}\right)\cup \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\cap \left(A^A\right)⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}$$
111	67 71 110	3eqtrd	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}$$
112	111	ex	$$⊢A\in V\to \left(1<\left|A\right|\to G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}\right)$$
113	34 53 112	3jaod	$$⊢A\in V\to \left(\left(\left|A\right|=0\vee \left|A\right|=1\vee 1<\left|A\right|\right)\to G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}\right)$$
114	6 113	mpd	$$⊢A\in V\to G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}$$