Metamath Proof Explorer

Theorem fosetex

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

Ref Expression
Assertion fosetex 
|- { f | f : A -onto-> B } e. _V

Proof

Step Hyp Ref Expression
1 ovex 
 |-  ( B ^m A ) e. _V
2 mapfoss 
 |-  { f | f : A -onto-> B } C_ ( B ^m A )
3 1 2 ssexi 
 |-  { f | f : A -onto-> B } e. _V