Theorem fosetex

Description: The set of surjections between two classes exists (without any precondition). (Contributed by AV, 8-Aug-2024)

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

Proof

Step	Hyp	Ref	Expression
1		ovex	⊢ ( 𝐵 ↑m 𝐴 ) ∈ V
2		mapfoss	⊢ { 𝑓 ∣ 𝑓 : 𝐴 –onto→ 𝐵 } ⊆ ( 𝐵 ↑m 𝐴 )
3	1 2	ssexi	⊢ { 𝑓 ∣ 𝑓 : 𝐴 –onto→ 𝐵 } ∈ V