Theorem permsetexOLD

Description: Obsolete version of f1osetex as of 8-Aug-2024. (Contributed by AV, 30-Mar-2024) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	permsetexOLD	|- ( A e. V -> { f | f : A -1-1-onto-> A } e. _V )

Proof

Step	Hyp	Ref	Expression
1		mapex	|- ( ( A e. V /\ A e. V ) -> { f | f : A --> A } e. _V )
2	1	anidms	|- ( A e. V -> { f | f : A --> A } e. _V )
3		f1of	|- ( f : A -1-1-onto-> A -> f : A --> A )
4	3	ss2abi	|- { f | f : A -1-1-onto-> A } C_ { f | f : A --> A }
5	4	a1i	|- ( A e. V -> { f | f : A -1-1-onto-> A } C_ { f | f : A --> A } )
6	2 5	ssexd	|- ( A e. V -> { f | f : A -1-1-onto-> A } e. _V )