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	⊢ ( 𝐴 ∈ 𝑉 → { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } ∈ V )

Proof

Step	Hyp	Ref	Expression
1		mapex	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐴 } ∈ V )
2	1	anidms	⊢ ( 𝐴 ∈ 𝑉 → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐴 } ∈ V )
3		f1of	⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐴 → 𝑓 : 𝐴 ⟶ 𝐴 )
4	3	ss2abi	⊢ { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } ⊆ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐴 }
5	4	a1i	⊢ ( 𝐴 ∈ 𝑉 → { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } ⊆ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐴 } )
6	2 5	ssexd	⊢ ( 𝐴 ∈ 𝑉 → { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } ∈ V )