Metamath Proof Explorer

Theorem imasetpreimafvbijlemfv

Description: Lemma for imasetpreimafvbij : the value of the mapping H at a preimage of a value of function F . (Contributed by AV, 5-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 imasetpreimafvbijlemfv 
|- ( ( F Fn A /\ Y e. P /\ X e. Y ) -> ( H ` Y ) = ( F ` X ) )

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 fnfun 
 |-  ( F Fn A -> Fun F )
4 3 anim1i 
 |-  ( ( F Fn A /\ Y e. P ) -> ( Fun F /\ Y e. P ) )
5 4 3adant3 
 |-  ( ( F Fn A /\ Y e. P /\ X e. Y ) -> ( Fun F /\ Y e. P ) )
6 1 2 fundcmpsurinjlem3 
 |-  ( ( Fun F /\ Y e. P ) -> ( H ` Y ) = U. ( F " Y ) )
7 5 6 syl 
 |-  ( ( F Fn A /\ Y e. P /\ X e. Y ) -> ( H ` Y ) = U. ( F " Y ) )
8 3 3ad2ant1 
 |-  ( ( F Fn A /\ Y e. P /\ X e. Y ) -> Fun F )
9 funiunfv 
 |-  ( Fun F -> U_ y e. Y ( F ` y ) = U. ( F " Y ) )
10 8 9 syl 
 |-  ( ( F Fn A /\ Y e. P /\ X e. Y ) -> U_ y e. Y ( F ` y ) = U. ( F " Y ) )
11 simp3 
 |-  ( ( F Fn A /\ Y e. P /\ X e. Y ) -> X e. Y )
12 simpl1 
 |-  ( ( ( F Fn A /\ Y e. P /\ X e. Y ) /\ y e. Y ) -> F Fn A )
13 simpl2 
 |-  ( ( ( F Fn A /\ Y e. P /\ X e. Y ) /\ y e. Y ) -> Y e. P )
14 simpr 
 |-  ( ( ( F Fn A /\ Y e. P /\ X e. Y ) /\ y e. Y ) -> y e. Y )
15 simpl3 
 |-  ( ( ( F Fn A /\ Y e. P /\ X e. Y ) /\ y e. Y ) -> X e. Y )
16 1 elsetpreimafveqfv 
 |-  ( ( F Fn A /\ ( Y e. P /\ y e. Y /\ X e. Y ) ) -> ( F ` y ) = ( F ` X ) )
17 12 13 14 15 16 syl13anc 
 |-  ( ( ( F Fn A /\ Y e. P /\ X e. Y ) /\ y e. Y ) -> ( F ` y ) = ( F ` X ) )
18 17 ralrimiva 
 |-  ( ( F Fn A /\ Y e. P /\ X e. Y ) -> A. y e. Y ( F ` y ) = ( F ` X ) )
19 fveq2 
 |-  ( y = X -> ( F ` y ) = ( F ` X ) )
20 19 iuneqconst 
 |-  ( ( X e. Y /\ A. y e. Y ( F ` y ) = ( F ` X ) ) -> U_ y e. Y ( F ` y ) = ( F ` X ) )
21 11 18 20 syl2anc 
 |-  ( ( F Fn A /\ Y e. P /\ X e. Y ) -> U_ y e. Y ( F ` y ) = ( F ` X ) )
22 7 10 21 3eqtr2d 
 |-  ( ( F Fn A /\ Y e. P /\ X e. Y ) -> ( H ` Y ) = ( F ` X ) )