Theorem f1osetex

Description: The set of bijections between two classes exists. (Contributed by AV, 30-Mar-2024) (Revised by AV, 8-Aug-2024) (Proof shortened by SN, 22-Aug-2024)

	Ref	Expression
Assertion	f1osetex	⊢ { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐵 } ∈ V

Proof

Step	Hyp	Ref	Expression
1		fosetex	⊢ { 𝑓 ∣ 𝑓 : 𝐴 –onto→ 𝐵 } ∈ V
2		f1ofo	⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → 𝑓 : 𝐴 –onto→ 𝐵 )
3	2	ss2abi	⊢ { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐵 } ⊆ { 𝑓 ∣ 𝑓 : 𝐴 –onto→ 𝐵 }
4	1 3	ssexi	⊢ { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐵 } ∈ V