Theorem fsetfocdm

Description: The class of functions with a given domain that is a set and a given codomain is mapped, through evaluation at a point of the domain, onto the codomain. (Contributed by AV, 15-Sep-2024)

	Ref	Expression
Hypotheses	fsetfocdm.f	|- F = { f | f : A --> B }
	fsetfocdm.s	|- S = ( g e. F |-> ( g ` X ) )
Assertion	fsetfocdm	|- ( ( A e. V /\ X e. A ) -> S : F -onto-> B )

Proof

Step	Hyp	Ref	Expression
1		fsetfocdm.f	|- F = { f | f : A --> B }
2		fsetfocdm.s	|- S = ( g e. F |-> ( g ` X ) )
3	1 2	fsetfcdm	|- ( X e. A -> S : F --> B )
4	3	adantl	|- ( ( A e. V /\ X e. A ) -> S : F --> B )
5		simplr	|- ( ( ( ( A e. V /\ X e. A ) /\ g e. B ) /\ x e. A ) -> g e. B )
6	5	fmpttd	|- ( ( ( A e. V /\ X e. A ) /\ g e. B ) -> ( x e. A |-> g ) : A --> B )
7		simpll	|- ( ( ( A e. V /\ X e. A ) /\ g e. B ) -> A e. V )
8	7	mptexd	|- ( ( ( A e. V /\ X e. A ) /\ g e. B ) -> ( x e. A |-> g ) e. _V )
9		feq1	|- ( f = ( x e. A |-> g ) -> ( f : A --> B <-> ( x e. A |-> g ) : A --> B ) )
10	9 1	elab2g	|- ( ( x e. A |-> g ) e. _V -> ( ( x e. A |-> g ) e. F <-> ( x e. A |-> g ) : A --> B ) )
11	8 10	syl	|- ( ( ( A e. V /\ X e. A ) /\ g e. B ) -> ( ( x e. A |-> g ) e. F <-> ( x e. A |-> g ) : A --> B ) )
12	6 11	mpbird	|- ( ( ( A e. V /\ X e. A ) /\ g e. B ) -> ( x e. A |-> g ) e. F )
13		fveq1	|- ( g = f -> ( g ` X ) = ( f ` X ) )
14	13	cbvmptv	|- ( g e. F |-> ( g ` X ) ) = ( f e. F |-> ( f ` X ) )
15	2 14	eqtri	|- S = ( f e. F |-> ( f ` X ) )
16		fveq1	|- ( f = ( x e. A |-> g ) -> ( f ` X ) = ( ( x e. A |-> g ) ` X ) )
17		fvexd	|- ( ( ( A e. V /\ X e. A ) /\ g e. B ) -> ( ( x e. A |-> g ) ` X ) e. _V )
18	15 16 12 17	fvmptd3	|- ( ( ( A e. V /\ X e. A ) /\ g e. B ) -> ( S ` ( x e. A |-> g ) ) = ( ( x e. A |-> g ) ` X ) )
19		eqidd	|- ( x = X -> g = g )
20		eqid	|- ( x e. A |-> g ) = ( x e. A |-> g )
21		vex	|- g e. _V
22	19 20 21	fvmpt	|- ( X e. A -> ( ( x e. A |-> g ) ` X ) = g )
23	22	ad2antlr	|- ( ( ( A e. V /\ X e. A ) /\ g e. B ) -> ( ( x e. A |-> g ) ` X ) = g )
24	18 23	eqtrd	|- ( ( ( A e. V /\ X e. A ) /\ g e. B ) -> ( S ` ( x e. A |-> g ) ) = g )
25		fveq2	|- ( h = ( x e. A |-> g ) -> ( S ` h ) = ( S ` ( x e. A |-> g ) ) )
26	25	eqcomd	|- ( h = ( x e. A |-> g ) -> ( S ` ( x e. A |-> g ) ) = ( S ` h ) )
27	24 26	sylan9req	|- ( ( ( ( A e. V /\ X e. A ) /\ g e. B ) /\ h = ( x e. A |-> g ) ) -> g = ( S ` h ) )
28	12 27	rspcedeq2vd	|- ( ( ( A e. V /\ X e. A ) /\ g e. B ) -> E. h e. F g = ( S ` h ) )
29	28	ralrimiva	|- ( ( A e. V /\ X e. A ) -> A. g e. B E. h e. F g = ( S ` h ) )
30		dffo3	|- ( S : F -onto-> B <-> ( S : F --> B /\ A. g e. B E. h e. F g = ( S ` h ) ) )
31	4 29 30	sylanbrc	|- ( ( A e. V /\ X e. A ) -> S : F -onto-> B )