Metamath Proof Explorer

Theorem imasetpreimafvbijlemfo

Description: Lemma for imasetpreimafvbij : the mapping H is a function onto the range of function F . (Contributed by AV, 22-Mar-2024)

Ref Expression
Hypotheses fundcmpsurinj.p 
|- P = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) }
fundcmpsurinj.h 
|- H = ( p e. P |-> U. ( F " p ) )
Assertion imasetpreimafvbijlemfo 
|- ( ( F Fn A /\ A e. V ) -> H : P -onto-> ( F " A ) )

Proof

Step Hyp Ref Expression
1 fundcmpsurinj.p 
 |-  P = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) }
2 fundcmpsurinj.h 
 |-  H = ( p e. P |-> U. ( F " p ) )
3 1 2 imasetpreimafvbijlemf 
 |-  ( F Fn A -> H : P --> ( F " A ) )
4 3 adantr 
 |-  ( ( F Fn A /\ A e. V ) -> H : P --> ( F " A ) )
5 1 preimafvelsetpreimafv 
 |-  ( ( F Fn A /\ A e. V /\ a e. A ) -> ( `' F " { ( F ` a ) } ) e. P )
6 5 3expa 
 |-  ( ( ( F Fn A /\ A e. V ) /\ a e. A ) -> ( `' F " { ( F ` a ) } ) e. P )
7 imaeq2 
 |-  ( p = ( `' F " { ( F ` a ) } ) -> ( F " p ) = ( F " ( `' F " { ( F ` a ) } ) ) )
8 7 unieqd 
 |-  ( p = ( `' F " { ( F ` a ) } ) -> U. ( F " p ) = U. ( F " ( `' F " { ( F ` a ) } ) ) )
9 8 eqeq2d 
 |-  ( p = ( `' F " { ( F ` a ) } ) -> ( ( F ` a ) = U. ( F " p ) <-> ( F ` a ) = U. ( F " ( `' F " { ( F ` a ) } ) ) ) )
10 9 adantl 
 |-  ( ( ( ( F Fn A /\ A e. V ) /\ a e. A ) /\ p = ( `' F " { ( F ` a ) } ) ) -> ( ( F ` a ) = U. ( F " p ) <-> ( F ` a ) = U. ( F " ( `' F " { ( F ` a ) } ) ) ) )
11 uniimaprimaeqfv 
 |-  ( ( F Fn A /\ a e. A ) -> U. ( F " ( `' F " { ( F ` a ) } ) ) = ( F ` a ) )
12 11 adantlr 
 |-  ( ( ( F Fn A /\ A e. V ) /\ a e. A ) -> U. ( F " ( `' F " { ( F ` a ) } ) ) = ( F ` a ) )
13 12 eqcomd 
 |-  ( ( ( F Fn A /\ A e. V ) /\ a e. A ) -> ( F ` a ) = U. ( F " ( `' F " { ( F ` a ) } ) ) )
14 6 10 13 rspcedvd 
 |-  ( ( ( F Fn A /\ A e. V ) /\ a e. A ) -> E. p e. P ( F ` a ) = U. ( F " p ) )
15 eqeq1 
 |-  ( y = ( F ` a ) -> ( y = U. ( F " p ) <-> ( F ` a ) = U. ( F " p ) ) )
16 15 eqcoms 
 |-  ( ( F ` a ) = y -> ( y = U. ( F " p ) <-> ( F ` a ) = U. ( F " p ) ) )
17 16 rexbidv 
 |-  ( ( F ` a ) = y -> ( E. p e. P y = U. ( F " p ) <-> E. p e. P ( F ` a ) = U. ( F " p ) ) )
18 14 17 syl5ibrcom 
 |-  ( ( ( F Fn A /\ A e. V ) /\ a e. A ) -> ( ( F ` a ) = y -> E. p e. P y = U. ( F " p ) ) )
19 18 rexlimdva 
 |-  ( ( F Fn A /\ A e. V ) -> ( E. a e. A ( F ` a ) = y -> E. p e. P y = U. ( F " p ) ) )
20 8 eqcomd 
 |-  ( p = ( `' F " { ( F ` a ) } ) -> U. ( F " ( `' F " { ( F ` a ) } ) ) = U. ( F " p ) )
21 13 20 sylan9eq 
 |-  ( ( ( ( F Fn A /\ A e. V ) /\ a e. A ) /\ p = ( `' F " { ( F ` a ) } ) ) -> ( F ` a ) = U. ( F " p ) )
22 21 ex 
 |-  ( ( ( F Fn A /\ A e. V ) /\ a e. A ) -> ( p = ( `' F " { ( F ` a ) } ) -> ( F ` a ) = U. ( F " p ) ) )
23 22 reximdva 
 |-  ( ( F Fn A /\ A e. V ) -> ( E. a e. A p = ( `' F " { ( F ` a ) } ) -> E. a e. A ( F ` a ) = U. ( F " p ) ) )
24 1 elsetpreimafv 
 |-  ( p e. P -> E. x e. A p = ( `' F " { ( F ` x ) } ) )
25 fveq2 
 |-  ( a = x -> ( F ` a ) = ( F ` x ) )
26 25 sneqd 
 |-  ( a = x -> { ( F ` a ) } = { ( F ` x ) } )
27 26 imaeq2d 
 |-  ( a = x -> ( `' F " { ( F ` a ) } ) = ( `' F " { ( F ` x ) } ) )
28 27 eqeq2d 
 |-  ( a = x -> ( p = ( `' F " { ( F ` a ) } ) <-> p = ( `' F " { ( F ` x ) } ) ) )
29 28 cbvrexvw 
 |-  ( E. a e. A p = ( `' F " { ( F ` a ) } ) <-> E. x e. A p = ( `' F " { ( F ` x ) } ) )
30 24 29 sylibr 
 |-  ( p e. P -> E. a e. A p = ( `' F " { ( F ` a ) } ) )
31 23 30 impel 
 |-  ( ( ( F Fn A /\ A e. V ) /\ p e. P ) -> E. a e. A ( F ` a ) = U. ( F " p ) )
32 eqeq2 
 |-  ( y = U. ( F " p ) -> ( ( F ` a ) = y <-> ( F ` a ) = U. ( F " p ) ) )
33 32 rexbidv 
 |-  ( y = U. ( F " p ) -> ( E. a e. A ( F ` a ) = y <-> E. a e. A ( F ` a ) = U. ( F " p ) ) )
34 31 33 syl5ibrcom 
 |-  ( ( ( F Fn A /\ A e. V ) /\ p e. P ) -> ( y = U. ( F " p ) -> E. a e. A ( F ` a ) = y ) )
35 34 rexlimdva 
 |-  ( ( F Fn A /\ A e. V ) -> ( E. p e. P y = U. ( F " p ) -> E. a e. A ( F ` a ) = y ) )
36 19 35 impbid 
 |-  ( ( F Fn A /\ A e. V ) -> ( E. a e. A ( F ` a ) = y <-> E. p e. P y = U. ( F " p ) ) )
37 36 abbidv 
 |-  ( ( F Fn A /\ A e. V ) -> { y | E. a e. A ( F ` a ) = y } = { y | E. p e. P y = U. ( F " p ) } )
38 fnfun 
 |-  ( F Fn A -> Fun F )
39 fndm 
 |-  ( F Fn A -> dom F = A )
40 eqimss2 
 |-  ( dom F = A -> A C_ dom F )
41 39 40 syl 
 |-  ( F Fn A -> A C_ dom F )
42 38 41 jca 
 |-  ( F Fn A -> ( Fun F /\ A C_ dom F ) )
43 42 adantr 
 |-  ( ( F Fn A /\ A e. V ) -> ( Fun F /\ A C_ dom F ) )
44 dfimafn 
 |-  ( ( Fun F /\ A C_ dom F ) -> ( F " A ) = { y | E. a e. A ( F ` a ) = y } )
45 43 44 syl 
 |-  ( ( F Fn A /\ A e. V ) -> ( F " A ) = { y | E. a e. A ( F ` a ) = y } )
46 2 rnmpt 
 |-  ran H = { y | E. p e. P y = U. ( F " p ) }
47 46 a1i 
 |-  ( ( F Fn A /\ A e. V ) -> ran H = { y | E. p e. P y = U. ( F " p ) } )
48 37 45 47 3eqtr4rd 
 |-  ( ( F Fn A /\ A e. V ) -> ran H = ( F " A ) )
49 dffo2 
 |-  ( H : P -onto-> ( F " A ) <-> ( H : P --> ( F " A ) /\ ran H = ( F " A ) ) )
50 4 48 49 sylanbrc 
 |-  ( ( F Fn A /\ A e. V ) -> H : P -onto-> ( F " A ) )