Metamath Proof Explorer

Theorem imasetpreimafvbijlemf1

Description: Lemma for imasetpreimafvbij : the mapping H is an injective function into the range of function F . (Contributed by AV, 9-Mar-2024) (Revised 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 imasetpreimafvbijlemf1 
|- ( F Fn A -> H : P -1-1-> ( 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 1 2 imasetpreimafvbijlemfv1 
 |-  ( ( F Fn A /\ s e. P ) -> E. b e. s ( H ` s ) = ( F ` b ) )
5 1 2 imasetpreimafvbijlemfv1 
 |-  ( ( F Fn A /\ r e. P ) -> E. a e. r ( H ` r ) = ( F ` a ) )
6 4 5 anim12dan 
 |-  ( ( F Fn A /\ ( s e. P /\ r e. P ) ) -> ( E. b e. s ( H ` s ) = ( F ` b ) /\ E. a e. r ( H ` r ) = ( F ` a ) ) )
7 eqeq12 
 |-  ( ( ( H ` s ) = ( F ` b ) /\ ( H ` r ) = ( F ` a ) ) -> ( ( H ` s ) = ( H ` r ) <-> ( F ` b ) = ( F ` a ) ) )
8 7 ancoms 
 |-  ( ( ( H ` r ) = ( F ` a ) /\ ( H ` s ) = ( F ` b ) ) -> ( ( H ` s ) = ( H ` r ) <-> ( F ` b ) = ( F ` a ) ) )
9 8 adantl 
 |-  ( ( ( ( ( F Fn A /\ ( s e. P /\ r e. P ) ) /\ b e. s ) /\ a e. r ) /\ ( ( H ` r ) = ( F ` a ) /\ ( H ` s ) = ( F ` b ) ) ) -> ( ( H ` s ) = ( H ` r ) <-> ( F ` b ) = ( F ` a ) ) )
10 simplll 
 |-  ( ( ( ( F Fn A /\ ( s e. P /\ r e. P ) ) /\ b e. s ) /\ a e. r ) -> F Fn A )
11 simpllr 
 |-  ( ( ( ( F Fn A /\ ( s e. P /\ r e. P ) ) /\ b e. s ) /\ a e. r ) -> ( s e. P /\ r e. P ) )
12 simpr 
 |-  ( ( ( F Fn A /\ ( s e. P /\ r e. P ) ) /\ b e. s ) -> b e. s )
13 12 anim1i 
 |-  ( ( ( ( F Fn A /\ ( s e. P /\ r e. P ) ) /\ b e. s ) /\ a e. r ) -> ( b e. s /\ a e. r ) )
14 1 elsetpreimafveq 
 |-  ( ( F Fn A /\ ( s e. P /\ r e. P ) /\ ( b e. s /\ a e. r ) ) -> ( ( F ` b ) = ( F ` a ) -> s = r ) )
15 10 11 13 14 syl3anc 
 |-  ( ( ( ( F Fn A /\ ( s e. P /\ r e. P ) ) /\ b e. s ) /\ a e. r ) -> ( ( F ` b ) = ( F ` a ) -> s = r ) )
16 15 adantr 
 |-  ( ( ( ( ( F Fn A /\ ( s e. P /\ r e. P ) ) /\ b e. s ) /\ a e. r ) /\ ( ( H ` r ) = ( F ` a ) /\ ( H ` s ) = ( F ` b ) ) ) -> ( ( F ` b ) = ( F ` a ) -> s = r ) )
17 9 16 sylbid 
 |-  ( ( ( ( ( F Fn A /\ ( s e. P /\ r e. P ) ) /\ b e. s ) /\ a e. r ) /\ ( ( H ` r ) = ( F ` a ) /\ ( H ` s ) = ( F ` b ) ) ) -> ( ( H ` s ) = ( H ` r ) -> s = r ) )
18 17 exp32 
 |-  ( ( ( ( F Fn A /\ ( s e. P /\ r e. P ) ) /\ b e. s ) /\ a e. r ) -> ( ( H ` r ) = ( F ` a ) -> ( ( H ` s ) = ( F ` b ) -> ( ( H ` s ) = ( H ` r ) -> s = r ) ) ) )
19 18 rexlimdva 
 |-  ( ( ( F Fn A /\ ( s e. P /\ r e. P ) ) /\ b e. s ) -> ( E. a e. r ( H ` r ) = ( F ` a ) -> ( ( H ` s ) = ( F ` b ) -> ( ( H ` s ) = ( H ` r ) -> s = r ) ) ) )
20 19 com23 
 |-  ( ( ( F Fn A /\ ( s e. P /\ r e. P ) ) /\ b e. s ) -> ( ( H ` s ) = ( F ` b ) -> ( E. a e. r ( H ` r ) = ( F ` a ) -> ( ( H ` s ) = ( H ` r ) -> s = r ) ) ) )
21 20 rexlimdva 
 |-  ( ( F Fn A /\ ( s e. P /\ r e. P ) ) -> ( E. b e. s ( H ` s ) = ( F ` b ) -> ( E. a e. r ( H ` r ) = ( F ` a ) -> ( ( H ` s ) = ( H ` r ) -> s = r ) ) ) )
22 21 impd 
 |-  ( ( F Fn A /\ ( s e. P /\ r e. P ) ) -> ( ( E. b e. s ( H ` s ) = ( F ` b ) /\ E. a e. r ( H ` r ) = ( F ` a ) ) -> ( ( H ` s ) = ( H ` r ) -> s = r ) ) )
23 6 22 mpd 
 |-  ( ( F Fn A /\ ( s e. P /\ r e. P ) ) -> ( ( H ` s ) = ( H ` r ) -> s = r ) )
24 23 ralrimivva 
 |-  ( F Fn A -> A. s e. P A. r e. P ( ( H ` s ) = ( H ` r ) -> s = r ) )
25 dff13 
 |-  ( H : P -1-1-> ( F " A ) <-> ( H : P --> ( F " A ) /\ A. s e. P A. r e. P ( ( H ` s ) = ( H ` r ) -> s = r ) ) )
26 3 24 25 sylanbrc 
 |-  ( F Fn A -> H : P -1-1-> ( F " A ) )