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	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
	symgvalstruct.b	$$⊢B=\left\{x|x:A\underset{1-1\; onto}{⟶}A\right\}$$
	symgvalstruct.m	$$⊢M=A^A$$
	symgvalstruct.p	$$⊢\underset{\dot{}}{+}=\left(f\in M,g\in M⟼f\circ g\right)$$
	symgvalstruct.j	$$⊢J={\prod }_{𝑡}\left(A\times \left\{𝒫A\right\}\right)$$
Assertion	symgvalstruct	$$⊢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		symgvalstruct.g	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
2		symgvalstruct.b	$$⊢B=\left\{x|x:A\underset{1-1\; onto}{⟶}A\right\}$$
3		symgvalstruct.m	$$⊢M=A^A$$
4		symgvalstruct.p	$$⊢\underset{\dot{}}{+}=\left(f\in M,g\in M⟼f\circ g\right)$$
5		symgvalstruct.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		vsnex	$$⊢\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		tsetndxnbasendx	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
88	87	a1i	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to \mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
89	75 76 77 81 83 86 88	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\}$$
90	89	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\}$$
91		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\}$$
92		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\}$$
93	91 92	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\}$$
94	1 56	symgbasmap	$$⊢x\in B\to x\in \left(A^A\right)$$
95	94	a1i	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to \left(x\in B\to x\in \left(A^A\right)\right)$$
96	95	ssrdv	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to B\subseteq A^A$$
97		dfss2	$$⊢B\subseteq A^A\leftrightarrow B\cap \left(A^A\right)=B$$
98	96 97	sylib	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to B\cap \left(A^A\right)=B$$
99	98	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⟩$$
100	99	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\}$$
101	93 100	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\}$$
102	74 90 101	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\}$$
103	67 71 102	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\}$$
104	103	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)$$
105	34 53 104	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)$$
106	6 105	mpd	$$⊢A\in V\to G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}$$