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		eqid	|- ( x e. A |-> g ) = ( x e. A |-> g )
7	5 6	fmptd	|- ( ( ( A e. V /\ X e. A ) /\ g e. B ) -> ( x e. A |-> g ) : A --> B )
8		simpll	|- ( ( ( A e. V /\ X e. A ) /\ g e. B ) -> A e. V )
9	8	mptexd	|- ( ( ( A e. V /\ X e. A ) /\ g e. B ) -> ( x e. A |-> g ) e. _V )
10		feq1	|- ( f = ( x e. A |-> g ) -> ( f : A --> B <-> ( x e. A |-> g ) : A --> B ) )
11	10 1	elab2g	|- ( ( x e. A |-> g ) e. _V -> ( ( x e. A |-> g ) e. F <-> ( x e. A |-> g ) : A --> B ) )
12	9 11	syl	|- ( ( ( A e. V /\ X e. A ) /\ g e. B ) -> ( ( x e. A |-> g ) e. F <-> ( x e. A |-> g ) : A --> B ) )
13	7 12	mpbird	|- ( ( ( A e. V /\ X e. A ) /\ g e. B ) -> ( x e. A |-> g ) e. F )
14		fveq2	|- ( h = ( x e. A |-> g ) -> ( S ` h ) = ( S ` ( x e. A |-> g ) ) )
15	14	eqeq2d	|- ( h = ( x e. A |-> g ) -> ( g = ( S ` h ) <-> g = ( S ` ( x e. A |-> g ) ) ) )
16	15	adantl	|- ( ( ( ( A e. V /\ X e. A ) /\ g e. B ) /\ h = ( x e. A |-> g ) ) -> ( g = ( S ` h ) <-> g = ( S ` ( x e. A |-> g ) ) ) )
17		fveq1	|- ( g = f -> ( g ` X ) = ( f ` X ) )
18	17	cbvmptv	|- ( g e. F |-> ( g ` X ) ) = ( f e. F |-> ( f ` X ) )
19	2 18	eqtri	|- S = ( f e. F |-> ( f ` X ) )
20	19	a1i	|- ( ( ( A e. V /\ X e. A ) /\ g e. B ) -> S = ( f e. F |-> ( f ` X ) ) )
21		fveq1	|- ( f = ( x e. A |-> g ) -> ( f ` X ) = ( ( x e. A |-> g ) ` X ) )
22	21	adantl	|- ( ( ( ( A e. V /\ X e. A ) /\ g e. B ) /\ f = ( x e. A |-> g ) ) -> ( f ` X ) = ( ( x e. A |-> g ) ` X ) )
23		fvexd	|- ( ( ( A e. V /\ X e. A ) /\ g e. B ) -> ( ( x e. A |-> g ) ` X ) e. _V )
24	20 22 13 23	fvmptd	|- ( ( ( A e. V /\ X e. A ) /\ g e. B ) -> ( S ` ( x e. A |-> g ) ) = ( ( x e. A |-> g ) ` X ) )
25		eqidd	|- ( ( A e. V /\ X e. A ) -> ( x e. A |-> g ) = ( x e. A |-> g ) )
26		eqidd	|- ( ( ( A e. V /\ X e. A ) /\ x = X ) -> g = g )
27		simpr	|- ( ( A e. V /\ X e. A ) -> X e. A )
28		vex	|- g e. _V
29	28	a1i	|- ( ( A e. V /\ X e. A ) -> g e. _V )
30	25 26 27 29	fvmptd	|- ( ( A e. V /\ X e. A ) -> ( ( x e. A |-> g ) ` X ) = g )
31	30	adantr	|- ( ( ( A e. V /\ X e. A ) /\ g e. B ) -> ( ( x e. A |-> g ) ` X ) = g )
32	24 31	eqtr2d	|- ( ( ( A e. V /\ X e. A ) /\ g e. B ) -> g = ( S ` ( x e. A |-> g ) ) )
33	13 16 32	rspcedvd	|- ( ( ( A e. V /\ X e. A ) /\ g e. B ) -> E. h e. F g = ( S ` h ) )
34	33	ralrimiva	|- ( ( A e. V /\ X e. A ) -> A. g e. B E. h e. F g = ( S ` h ) )
35		dffo3	|- ( S : F -onto-> B <-> ( S : F --> B /\ A. g e. B E. h e. F g = ( S ` h ) ) )
36	4 34 35	sylanbrc	|- ( ( A e. V /\ X e. A ) -> S : F -onto-> B )