Theorem slotresfo

Description: The condition of a structure component extractor restricted to a class being a surjection. This combined with fonex can be used to prove a class being proper. (Contributed by Zhi Wang, 20-Oct-2025)

	Ref	Expression
Hypotheses	slotresfo.e	|- E Fn _V
	slotresfo.v	|- ( k e. A -> ( E ` k ) e. V )
	slotresfo.k	|- ( b e. V -> K e. A )
	slotresfo.b	|- ( b e. V -> b = ( E ` K ) )
Assertion	slotresfo	|- ( E |` A ) : A -onto-> V

Proof

Step	Hyp	Ref	Expression
1		slotresfo.e	|- E Fn _V
2		slotresfo.v	|- ( k e. A -> ( E ` k ) e. V )
3		slotresfo.k	|- ( b e. V -> K e. A )
4		slotresfo.b	|- ( b e. V -> b = ( E ` K ) )
5		ssv	|- A C_ _V
6		fnssres	|- ( ( E Fn _V /\ A C_ _V ) -> ( E |` A ) Fn A )
7	1 5 6	mp2an	|- ( E |` A ) Fn A
8		fvres	|- ( k e. A -> ( ( E |` A ) ` k ) = ( E ` k ) )
9	8 2	eqeltrd	|- ( k e. A -> ( ( E |` A ) ` k ) e. V )
10	9	rgen	|- A. k e. A ( ( E |` A ) ` k ) e. V
11		fnfvrnss	|- ( ( ( E |` A ) Fn A /\ A. k e. A ( ( E |` A ) ` k ) e. V ) -> ran ( E |` A ) C_ V )
12	7 10 11	mp2an	|- ran ( E |` A ) C_ V
13		df-f	|- ( ( E |` A ) : A --> V <-> ( ( E |` A ) Fn A /\ ran ( E |` A ) C_ V ) )
14	7 12 13	mpbir2an	|- ( E |` A ) : A --> V
15		fveq2	|- ( k = K -> ( E ` k ) = ( E ` K ) )
16	15	eqeq2d	|- ( k = K -> ( b = ( E ` k ) <-> b = ( E ` K ) ) )
17	16 3 4	rspcedvdw	|- ( b e. V -> E. k e. A b = ( E ` k ) )
18	8	eqeq2d	|- ( k e. A -> ( b = ( ( E |` A ) ` k ) <-> b = ( E ` k ) ) )
19	18	rexbiia	|- ( E. k e. A b = ( ( E |` A ) ` k ) <-> E. k e. A b = ( E ` k ) )
20	17 19	sylibr	|- ( b e. V -> E. k e. A b = ( ( E |` A ) ` k ) )
21	20	rgen	|- A. b e. V E. k e. A b = ( ( E |` A ) ` k )
22		dffo3	|- ( ( E |` A ) : A -onto-> V <-> ( ( E |` A ) : A --> V /\ A. b e. V E. k e. A b = ( ( E |` A ) ` k ) ) )
23	14 21 22	mpbir2an	|- ( E |` A ) : A -onto-> V