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	Could not format ( EndoFMnd ` (/) ) = ( SymGrp ` (/) ) : No typesetting found for |- ( EndoFMnd ` (/) ) = ( SymGrp ` (/) ) with typecode |-
9	8	eqcomi	Could not format ( SymGrp ` (/) ) = ( EndoFMnd ` (/) ) : No typesetting found for |- ( SymGrp ` (/) ) = ( EndoFMnd ` (/) ) with typecode |-
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	Could not format ( A = (/) -> ( EndoFMnd ` A ) = ( EndoFMnd ` (/) ) ) : No typesetting found for |- ( A = (/) -> ( EndoFMnd ` A ) = ( EndoFMnd ` (/) ) ) with typecode |-
13	9 11 12	3eqtr4a	Could not format ( A = (/) -> G = ( EndoFMnd ` A ) ) : No typesetting found for |- ( A = (/) -> G = ( EndoFMnd ` A ) ) with typecode |-
14	13	adantl	Could not format ( ( A e. V /\ A = (/) ) -> G = ( EndoFMnd ` A ) ) : No typesetting found for |- ( ( A e. V /\ A = (/) ) -> G = ( EndoFMnd ` A ) ) with typecode |-
15		eqid	Could not format ( EndoFMnd ` A ) = ( EndoFMnd ` A ) : No typesetting found for |- ( EndoFMnd ` A ) = ( EndoFMnd ` A ) with typecode |-
16	15 3 4 5	efmnd	Could not format ( A e. V -> ( EndoFMnd ` A ) = { <. ( Base ` ndx ) , M >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } ) : No typesetting found for |- ( A e. V -> ( EndoFMnd ` A ) = { <. ( Base ` ndx ) , M >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } ) with typecode |-
17	16	adantr	Could not format ( ( A e. V /\ A = (/) ) -> ( EndoFMnd ` A ) = { <. ( Base ` ndx ) , M >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } ) : No typesetting found for |- ( ( A e. V /\ A = (/) ) -> ( EndoFMnd ` A ) = { <. ( Base ` ndx ) , M >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } ) with typecode |-
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	Could not format ( A e. _V -> ( EndoFMnd ` A ) = { <. ( Base ` ndx ) , M >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } ) : No typesetting found for |- ( A e. _V -> ( EndoFMnd ` A ) = { <. ( Base ` ndx ) , M >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } ) with typecode |-
40	38 39	syl	Could not format ( A = { x } -> ( EndoFMnd ` A ) = { <. ( Base ` ndx ) , M >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } ) : No typesetting found for |- ( A = { x } -> ( EndoFMnd ` A ) = { <. ( Base ` ndx ) , M >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } ) with typecode |-
41		snsymgefmndeq	Could not format ( A = { x } -> ( EndoFMnd ` A ) = ( SymGrp ` A ) ) : No typesetting found for |- ( A = { x } -> ( EndoFMnd ` A ) = ( SymGrp ` A ) ) with typecode |-
42	41 1	eqtr4di	Could not format ( A = { x } -> ( EndoFMnd ` A ) = G ) : No typesetting found for |- ( A = { x } -> ( EndoFMnd ` A ) = G ) with typecode |-
43	42	fveq2d	Could not format ( A = { x } -> ( Base ` ( EndoFMnd ` A ) ) = ( Base ` G ) ) : No typesetting found for |- ( A = { x } -> ( Base ` ( EndoFMnd ` A ) ) = ( Base ` G ) ) with typecode |-
44		eqid	Could not format ( Base ` ( EndoFMnd ` A ) ) = ( Base ` ( EndoFMnd ` A ) ) : No typesetting found for |- ( Base ` ( EndoFMnd ` A ) ) = ( Base ` ( EndoFMnd ` A ) ) with typecode |-
45	15 44	efmndbas	Could not format ( Base ` ( EndoFMnd ` A ) ) = ( A ^m A ) : No typesetting found for |- ( Base ` ( EndoFMnd ` A ) ) = ( A ^m A ) with typecode |-
46	45 3	eqtr4i	Could not format ( Base ` ( EndoFMnd ` A ) ) = M : No typesetting found for |- ( Base ` ( EndoFMnd ` A ) ) = M with typecode |-
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	syl6bi	$$⊢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	Could not format ( ( A e. V /\ 1 < ( # ` A ) ) -> ( Base ` G ) C. ( Base ` ( EndoFMnd ` A ) ) ) : No typesetting found for |- ( ( A e. V /\ 1 < ( # ` A ) ) -> ( Base ` G ) C. ( Base ` ( EndoFMnd ` A ) ) ) with typecode |-
56	2 23	eqtr4i	$$⊢B={\mathrm{Base}}_G$$
57	45	eqcomi	Could not format ( A ^m A ) = ( Base ` ( EndoFMnd ` A ) ) : No typesetting found for |- ( A ^m A ) = ( Base ` ( EndoFMnd ` A ) ) with typecode |-
58	56 57	psseq12i	Could not format ( B C. ( A ^m A ) <-> ( Base ` G ) C. ( Base ` ( EndoFMnd ` A ) ) ) : No typesetting found for |- ( B C. ( A ^m A ) <-> ( Base ` G ) C. ( Base ` ( EndoFMnd ` A ) ) ) with typecode |-
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	Could not format ( ( A e. V /\ 1 < ( # ` A ) ) -> ( EndoFMnd ` A ) e. _V ) : No typesetting found for |- ( ( A e. V /\ 1 < ( # ` A ) ) -> ( EndoFMnd ` A ) e. _V ) with typecode |-
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	Could not format G = ( ( EndoFMnd ` A ) |`s B ) : No typesetting found for |- G = ( ( EndoFMnd ` A ) |`s B ) with typecode |-
66	65 57	ressval2	Could not format ( ( -. ( A ^m A ) C_ B /\ ( EndoFMnd ` A ) e. _V /\ B e. _V ) -> G = ( ( EndoFMnd ` A ) sSet <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. ) ) : No typesetting found for |- ( ( -. ( A ^m A ) C_ B /\ ( EndoFMnd ` A ) e. _V /\ B e. _V ) -> G = ( ( EndoFMnd ` A ) sSet <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. ) ) with typecode |-
67	60 61 64 66	syl3anc	Could not format ( ( A e. V /\ 1 < ( # ` A ) ) -> G = ( ( EndoFMnd ` A ) sSet <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. ) ) : No typesetting found for |- ( ( A e. V /\ 1 < ( # ` A ) ) -> G = ( ( EndoFMnd ` A ) sSet <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. ) ) with typecode |-
68		ovex	$$⊢A^A\in \mathrm{V}$$
69	68	inex2	$$⊢B\cap \left(A^A\right)\in \mathrm{V}$$
70		setsval	Could not format ( ( ( EndoFMnd ` A ) e. _V /\ ( B i^i ( A ^m A ) ) e. _V ) -> ( ( EndoFMnd ` A ) sSet <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. ) = ( ( ( EndoFMnd ` A ) |` ( _V \ { ( Base ` ndx ) } ) ) u. { <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. } ) ) : No typesetting found for |- ( ( ( EndoFMnd ` A ) e. _V /\ ( B i^i ( A ^m A ) ) e. _V ) -> ( ( EndoFMnd ` A ) sSet <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. ) = ( ( ( EndoFMnd ` A ) |` ( _V \ { ( Base ` ndx ) } ) ) u. { <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. } ) ) with typecode |-
71	61 69 70	sylancl	Could not format ( ( A e. V /\ 1 < ( # ` A ) ) -> ( ( EndoFMnd ` A ) sSet <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. ) = ( ( ( EndoFMnd ` A ) |` ( _V \ { ( Base ` ndx ) } ) ) u. { <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. } ) ) : No typesetting found for |- ( ( A e. V /\ 1 < ( # ` A ) ) -> ( ( EndoFMnd ` A ) sSet <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. ) = ( ( ( EndoFMnd ` A ) |` ( _V \ { ( Base ` ndx ) } ) ) u. { <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. } ) ) with typecode |-
72	16	adantr	Could not format ( ( A e. V /\ 1 < ( # ` A ) ) -> ( EndoFMnd ` A ) = { <. ( Base ` ndx ) , M >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } ) : No typesetting found for |- ( ( A e. V /\ 1 < ( # ` A ) ) -> ( EndoFMnd ` A ) = { <. ( Base ` ndx ) , M >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } ) with typecode |-
73	72	reseq1d	Could not format ( ( A e. V /\ 1 < ( # ` A ) ) -> ( ( EndoFMnd ` A ) |` ( _V \ { ( Base ` ndx ) } ) ) = ( { <. ( Base ` ndx ) , M >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } |` ( _V \ { ( Base ` ndx ) } ) ) ) : No typesetting found for |- ( ( A e. V /\ 1 < ( # ` A ) ) -> ( ( EndoFMnd ` A ) |` ( _V \ { ( Base ` ndx ) } ) ) = ( { <. ( Base ` ndx ) , M >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } |` ( _V \ { ( Base ` ndx ) } ) ) ) with typecode |-
74	73	uneq1d	Could not format ( ( A e. V /\ 1 < ( # ` A ) ) -> ( ( ( EndoFMnd ` A ) |` ( _V \ { ( Base ` ndx ) } ) ) u. { <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. } ) = ( ( { <. ( Base ` ndx ) , M >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } |` ( _V \ { ( Base ` ndx ) } ) ) u. { <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. } ) ) : No typesetting found for |- ( ( A e. V /\ 1 < ( # ` A ) ) -> ( ( ( EndoFMnd ` A ) |` ( _V \ { ( Base ` ndx ) } ) ) u. { <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. } ) = ( ( { <. ( Base ` ndx ) , M >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } |` ( _V \ { ( Base ` ndx ) } ) ) u. { <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. } ) ) with typecode |-
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		df-ss	$$⊢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	Could not format ( ( A e. V /\ 1 < ( # ` A ) ) -> ( ( ( EndoFMnd ` A ) |` ( _V \ { ( Base ` ndx ) } ) ) u. { <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. } ) = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } ) : No typesetting found for |- ( ( A e. V /\ 1 < ( # ` A ) ) -> ( ( ( EndoFMnd ` A ) |` ( _V \ { ( Base ` ndx ) } ) ) u. { <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. } ) = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } ) with typecode |-
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\}$$