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	$$⊢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	syl5eq	$$⊢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	syl5eq	$$⊢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	syl5eq	$$⊢\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	1 56	symgbasex	$$⊢A\in V\to B\in \mathrm{V}$$
63	62	adantr	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to B\in \mathrm{V}$$
64	1 2	symgval	Could not format G = ( ( EndoFMnd ` A ) |`s B ) : No typesetting found for |- G = ( ( EndoFMnd ` A ) |`s B ) with typecode |-
65	64 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 |-
66	60 61 63 65	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 |-
67		ovex	$$⊢A^A\in \mathrm{V}$$
68	67	inex2	$$⊢B\cap \left(A^A\right)\in \mathrm{V}$$
69		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 |-
70	61 68 69	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 |-
71	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 |-
72	71	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 |-
73	72	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 |-
74		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\}$$
75		fvexd	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to {+}_{\mathrm{ndx}}\in \mathrm{V}$$
76		fvexd	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to \mathrm{TopSet}\left(\mathrm{ndx}\right)\in \mathrm{V}$$
77	3 67	eqeltri	$$⊢M\in \mathrm{V}$$
78	77 77	mpoex	$$⊢\left(f\in M,g\in M⟼f\circ g\right)\in \mathrm{V}$$
79	4 78	eqeltri	$$⊢\underset{\dot{}}{+}\in \mathrm{V}$$
80	79	a1i	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to \underset{\dot{}}{+}\in \mathrm{V}$$
81	5	fvexi	$$⊢J\in \mathrm{V}$$
82	81	a1i	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to J\in \mathrm{V}$$
83		basendxnplusgndx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne {+}_{\mathrm{ndx}}$$
84	83	necomi	$$⊢{+}_{\mathrm{ndx}}\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
85	84	a1i	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to {+}_{\mathrm{ndx}}\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
86		tsetndx	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)=9$$
87		1re	$$⊢1\in ℝ$$
88		1lt9	$$⊢1<9$$
89	87 88	gtneii	$$⊢9\ne 1$$
90		df-base	$$⊢\mathrm{Base}=\mathrm{Slot}1$$
91		1nn	$$⊢1\in \mathbb{N}$$
92	90 91	ndxarg	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}=1$$
93	89 92	neeqtrri	$$⊢9\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
94	86 93	eqnetri	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
95	94	a1i	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to \mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
96	74 75 76 80 82 85 95	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\}$$
97	96	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\}$$
98		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\}$$
99		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\}$$
100	98 99	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\}$$
101	1 56	symgbasmap	$$⊢x\in B\to x\in \left(A^A\right)$$
102	101	a1i	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to \left(x\in B\to x\in \left(A^A\right)\right)$$
103	102	ssrdv	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to B\subseteq A^A$$
104		df-ss	$$⊢B\subseteq A^A\leftrightarrow B\cap \left(A^A\right)=B$$
105	103 104	sylib	$$⊢\left(A\in V\wedge 1<\left|A\right|\right)\to B\cap \left(A^A\right)=B$$
106	105	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⟩$$
107	106	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\}$$
108	100 107	syl5eq	$$⊢\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\}$$
109	73 97 108	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 |-
110	66 70 109	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\}$$
111	110	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)$$
112	34 53 111	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)$$
113	6 112	mpd	$$⊢A\in V\to G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}$$