Theorem 1aryenef

Description: The set of unary (endo)functions and the set of endofunctions are equinumerous. (Contributed by AV, 19-May-2024)

	Ref	Expression
Assertion	1aryenef	Could not format assertion : No typesetting found for |- ( 1 -aryF X ) ~~ ( X ^m X ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		ovex	Could not format ( 1 -aryF X ) e. _V : No typesetting found for |- ( 1 -aryF X ) e. _V with typecode |-
2	1	mptex	Could not format ( f e. ( 1 -aryF X ) |-> ( x e. X |-> ( f ` { <. 0 , x >. } ) ) ) e. _V : No typesetting found for |- ( f e. ( 1 -aryF X ) |-> ( x e. X |-> ( f ` { <. 0 , x >. } ) ) ) e. _V with typecode |-
3	2	a1i	Could not format ( X e. _V -> ( f e. ( 1 -aryF X ) |-> ( x e. X |-> ( f ` { <. 0 , x >. } ) ) ) e. _V ) : No typesetting found for |- ( X e. _V -> ( f e. ( 1 -aryF X ) |-> ( x e. X |-> ( f ` { <. 0 , x >. } ) ) ) e. _V ) with typecode |-
4		eqid	Could not format ( f e. ( 1 -aryF X ) |-> ( x e. X |-> ( f ` { <. 0 , x >. } ) ) ) = ( f e. ( 1 -aryF X ) |-> ( x e. X |-> ( f ` { <. 0 , x >. } ) ) ) : No typesetting found for |- ( f e. ( 1 -aryF X ) |-> ( x e. X |-> ( f ` { <. 0 , x >. } ) ) ) = ( f e. ( 1 -aryF X ) |-> ( x e. X |-> ( f ` { <. 0 , x >. } ) ) ) with typecode |-
5	4	1arymaptf1o	Could not format ( X e. _V -> ( f e. ( 1 -aryF X ) |-> ( x e. X |-> ( f ` { <. 0 , x >. } ) ) ) : ( 1 -aryF X ) -1-1-onto-> ( X ^m X ) ) : No typesetting found for |- ( X e. _V -> ( f e. ( 1 -aryF X ) |-> ( x e. X |-> ( f ` { <. 0 , x >. } ) ) ) : ( 1 -aryF X ) -1-1-onto-> ( X ^m X ) ) with typecode |-
6		f1oeq1	Could not format ( h = ( f e. ( 1 -aryF X ) |-> ( x e. X |-> ( f ` { <. 0 , x >. } ) ) ) -> ( h : ( 1 -aryF X ) -1-1-onto-> ( X ^m X ) <-> ( f e. ( 1 -aryF X ) |-> ( x e. X |-> ( f ` { <. 0 , x >. } ) ) ) : ( 1 -aryF X ) -1-1-onto-> ( X ^m X ) ) ) : No typesetting found for |- ( h = ( f e. ( 1 -aryF X ) |-> ( x e. X |-> ( f ` { <. 0 , x >. } ) ) ) -> ( h : ( 1 -aryF X ) -1-1-onto-> ( X ^m X ) <-> ( f e. ( 1 -aryF X ) |-> ( x e. X |-> ( f ` { <. 0 , x >. } ) ) ) : ( 1 -aryF X ) -1-1-onto-> ( X ^m X ) ) ) with typecode |-
7	3 5 6	spcedv	Could not format ( X e. _V -> E. h h : ( 1 -aryF X ) -1-1-onto-> ( X ^m X ) ) : No typesetting found for |- ( X e. _V -> E. h h : ( 1 -aryF X ) -1-1-onto-> ( X ^m X ) ) with typecode |-
8		bren	Could not format ( ( 1 -aryF X ) ~~ ( X ^m X ) <-> E. h h : ( 1 -aryF X ) -1-1-onto-> ( X ^m X ) ) : No typesetting found for |- ( ( 1 -aryF X ) ~~ ( X ^m X ) <-> E. h h : ( 1 -aryF X ) -1-1-onto-> ( X ^m X ) ) with typecode |-
9	7 8	sylibr	Could not format ( X e. _V -> ( 1 -aryF X ) ~~ ( X ^m X ) ) : No typesetting found for |- ( X e. _V -> ( 1 -aryF X ) ~~ ( X ^m X ) ) with typecode |-
10		0ex	$$⊢\varnothing \in \mathrm{V}$$
11	10	enref	$$⊢\varnothing \approx \varnothing$$
12	11	a1i	$$⊢\neg X\in \mathrm{V}\to \varnothing \approx \varnothing$$
13		df-naryf	Could not format -aryF = ( n e. NN0 , x e. _V |-> ( x ^m ( x ^m ( 0 ..^ n ) ) ) ) : No typesetting found for |- -aryF = ( n e. NN0 , x e. _V |-> ( x ^m ( x ^m ( 0 ..^ n ) ) ) ) with typecode |-
14	13	reldmmpo	Could not format Rel dom -aryF : No typesetting found for |- Rel dom -aryF with typecode |-
15	14	ovprc2	Could not format ( -. X e. _V -> ( 1 -aryF X ) = (/) ) : No typesetting found for |- ( -. X e. _V -> ( 1 -aryF X ) = (/) ) with typecode |-
16		reldmmap	$$⊢\mathrm{Rel}\mathrm{dom}{\uparrow }_{𝑚}$$
17	16	ovprc1	$$⊢\neg X\in \mathrm{V}\to X^X=\varnothing$$
18	12 15 17	3brtr4d	Could not format ( -. X e. _V -> ( 1 -aryF X ) ~~ ( X ^m X ) ) : No typesetting found for |- ( -. X e. _V -> ( 1 -aryF X ) ~~ ( X ^m X ) ) with typecode |-
19	9 18	pm2.61i	Could not format ( 1 -aryF X ) ~~ ( X ^m X ) : No typesetting found for |- ( 1 -aryF X ) ~~ ( X ^m X ) with typecode |-