Theorem symgbas

Description: The base set of the symmetric group. (Contributed by Mario Carneiro, 12-Jan-2015) (Proof shortened by AV, 29-Mar-2024)

	Ref	Expression
Hypotheses	symgbas.1	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
	symgbas.2	$$⊢B={\mathrm{Base}}_G$$
Assertion	symgbas	$$⊢B=\left\{x|x:A\underset{1-1\; onto}{⟶}A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		symgbas.1	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
2		symgbas.2	$$⊢B={\mathrm{Base}}_G$$
3		eqid	$$⊢\left\{x|x:A\underset{1-1\; onto}{⟶}A\right\}=\left\{x|x:A\underset{1-1\; onto}{⟶}A\right\}$$
4	1 3	symgval	Could not format G = ( ( EndoFMnd ` A ) |`s { x | x : A -1-1-onto-> A } ) : No typesetting found for |- G = ( ( EndoFMnd ` A ) |`s { x | x : A -1-1-onto-> A } ) with typecode |-
5	4	eqcomi	Could not format ( ( EndoFMnd ` A ) |`s { x | x : A -1-1-onto-> A } ) = G : No typesetting found for |- ( ( EndoFMnd ` A ) |`s { x | x : A -1-1-onto-> A } ) = G with typecode |-
6	5	fveq2i	Could not format ( Base ` ( ( EndoFMnd ` A ) |`s { x | x : A -1-1-onto-> A } ) ) = ( Base ` G ) : No typesetting found for |- ( Base ` ( ( EndoFMnd ` A ) |`s { x | x : A -1-1-onto-> A } ) ) = ( Base ` G ) with typecode |-
7		f1of	$$⊢x:A\underset{1-1\; onto}{⟶}A\to x:A⟶A$$
8	7	ss2abi	$$⊢\left\{x|x:A\underset{1-1\; onto}{⟶}A\right\}\subseteq \left\{x|x:A⟶A\right\}$$
9		eqid	Could not format ( EndoFMnd ` A ) = ( EndoFMnd ` A ) : No typesetting found for |- ( EndoFMnd ` A ) = ( EndoFMnd ` A ) with typecode |-
10		eqid	Could not format ( Base ` ( EndoFMnd ` A ) ) = ( Base ` ( EndoFMnd ` A ) ) : No typesetting found for |- ( Base ` ( EndoFMnd ` A ) ) = ( Base ` ( EndoFMnd ` A ) ) with typecode |-
11	9 10	efmndbasabf	Could not format ( Base ` ( EndoFMnd ` A ) ) = { x | x : A --> A } : No typesetting found for |- ( Base ` ( EndoFMnd ` A ) ) = { x | x : A --> A } with typecode |-
12	8 11	sseqtrri	Could not format { x | x : A -1-1-onto-> A } C_ ( Base ` ( EndoFMnd ` A ) ) : No typesetting found for |- { x | x : A -1-1-onto-> A } C_ ( Base ` ( EndoFMnd ` A ) ) with typecode |-
13		eqid	Could not format ( ( EndoFMnd ` A ) |`s { x | x : A -1-1-onto-> A } ) = ( ( EndoFMnd ` A ) |`s { x | x : A -1-1-onto-> A } ) : No typesetting found for |- ( ( EndoFMnd ` A ) |`s { x | x : A -1-1-onto-> A } ) = ( ( EndoFMnd ` A ) |`s { x | x : A -1-1-onto-> A } ) with typecode |-
14	13 10	ressbas2	Could not format ( { x | x : A -1-1-onto-> A } C_ ( Base ` ( EndoFMnd ` A ) ) -> { x | x : A -1-1-onto-> A } = ( Base ` ( ( EndoFMnd ` A ) |`s { x | x : A -1-1-onto-> A } ) ) ) : No typesetting found for |- ( { x | x : A -1-1-onto-> A } C_ ( Base ` ( EndoFMnd ` A ) ) -> { x | x : A -1-1-onto-> A } = ( Base ` ( ( EndoFMnd ` A ) |`s { x | x : A -1-1-onto-> A } ) ) ) with typecode |-
15	12 14	ax-mp	Could not format { x | x : A -1-1-onto-> A } = ( Base ` ( ( EndoFMnd ` A ) |`s { x | x : A -1-1-onto-> A } ) ) : No typesetting found for |- { x | x : A -1-1-onto-> A } = ( Base ` ( ( EndoFMnd ` A ) |`s { x | x : A -1-1-onto-> A } ) ) with typecode |-
16	6 15 2	3eqtr4ri	$$⊢B=\left\{x|x:A\underset{1-1\; onto}{⟶}A\right\}$$