Metamath Proof Explorer

Theorem iunpreima

Description: Preimage of an indexed union. (Contributed by Thierry Arnoux, 27-Mar-2018)

Ref Expression
Assertion iunpreima 
|- ( Fun F -> ( `' F " U_ x e. A B ) = U_ x e. A ( `' F " B ) )

Proof

Step Hyp Ref Expression
1 eliun 
 |-  ( ( F ` y ) e. U_ x e. A B <-> E. x e. A ( F ` y ) e. B )
2 1 a1i 
 |-  ( Fun F -> ( ( F ` y ) e. U_ x e. A B <-> E. x e. A ( F ` y ) e. B ) )
3 2 rabbidv 
 |-  ( Fun F -> { y e. dom F | ( F ` y ) e. U_ x e. A B } = { y e. dom F | E. x e. A ( F ` y ) e. B } )
4 funfn 
 |-  ( Fun F <-> F Fn dom F )
5 fncnvima2 
 |-  ( F Fn dom F -> ( `' F " U_ x e. A B ) = { y e. dom F | ( F ` y ) e. U_ x e. A B } )
6 4 5 sylbi 
 |-  ( Fun F -> ( `' F " U_ x e. A B ) = { y e. dom F | ( F ` y ) e. U_ x e. A B } )
7 iunrab 
 |-  U_ x e. A { y e. dom F | ( F ` y ) e. B } = { y e. dom F | E. x e. A ( F ` y ) e. B }
8 7 a1i 
 |-  ( Fun F -> U_ x e. A { y e. dom F | ( F ` y ) e. B } = { y e. dom F | E. x e. A ( F ` y ) e. B } )
9 3 6 8 3eqtr4d 
 |-  ( Fun F -> ( `' F " U_ x e. A B ) = U_ x e. A { y e. dom F | ( F ` y ) e. B } )
10 fncnvima2 
 |-  ( F Fn dom F -> ( `' F " B ) = { y e. dom F | ( F ` y ) e. B } )
11 4 10 sylbi 
 |-  ( Fun F -> ( `' F " B ) = { y e. dom F | ( F ` y ) e. B } )
12 11 iuneq2d 
 |-  ( Fun F -> U_ x e. A ( `' F " B ) = U_ x e. A { y e. dom F | ( F ` y ) e. B } )
13 9 12 eqtr4d 
 |-  ( Fun F -> ( `' F " U_ x e. A B ) = U_ x e. A ( `' F " B ) )