This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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