Theorem elefmndbas2

Description: Two ways of saying a function is a mapping of A to itself. (Contributed by AV, 27-Jan-2024) (Proof shortened by AV, 29-Mar-2024)

	Ref	Expression
Hypotheses	efmndbas.g	No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
	efmndbas.b	$$⊢B={\mathrm{Base}}_G$$
Assertion	elefmndbas2	$$⊢F\in V\to \left(F\in B\leftrightarrow F:A⟶A\right)$$

Proof

Step	Hyp	Ref	Expression
1		efmndbas.g	Could not format G = ( EndoFMnd ` A ) : No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
2		efmndbas.b	$$⊢B={\mathrm{Base}}_G$$
3	1 2	efmndbasabf	$$⊢B=\left\{f|f:A⟶A\right\}$$
4	3	a1i	$$⊢F\in V\to B=\left\{f|f:A⟶A\right\}$$
5	4	eleq2d	$$⊢F\in V\to \left(F\in B\leftrightarrow F\in \left\{f|f:A⟶A\right\}\right)$$
6		feq1	$$⊢f=F\to \left(f:A⟶A\leftrightarrow F:A⟶A\right)$$
7		eqid	$$⊢\left\{f|f:A⟶A\right\}=\left\{f|f:A⟶A\right\}$$
8	6 7	elab2g	$$⊢F\in V\to \left(F\in \left\{f|f:A⟶A\right\}\leftrightarrow F:A⟶A\right)$$
9	5 8	bitrd	$$⊢F\in V\to \left(F\in B\leftrightarrow F:A⟶A\right)$$