Metamath Proof Explorer


Theorem unima

Description: Image of a union. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion unima
|- ( ( F Fn A /\ B C_ A /\ C C_ A ) -> ( F " ( B u. C ) ) = ( ( F " B ) u. ( F " C ) ) )

Proof

Step Hyp Ref Expression
1 simp1
 |-  ( ( F Fn A /\ B C_ A /\ C C_ A ) -> F Fn A )
2 simpl
 |-  ( ( B C_ A /\ C C_ A ) -> B C_ A )
3 simpr
 |-  ( ( B C_ A /\ C C_ A ) -> C C_ A )
4 2 3 unssd
 |-  ( ( B C_ A /\ C C_ A ) -> ( B u. C ) C_ A )
5 4 3adant1
 |-  ( ( F Fn A /\ B C_ A /\ C C_ A ) -> ( B u. C ) C_ A )
6 1 5 fvelimabd
 |-  ( ( F Fn A /\ B C_ A /\ C C_ A ) -> ( y e. ( F " ( B u. C ) ) <-> E. x e. ( B u. C ) ( F ` x ) = y ) )
7 rexun
 |-  ( E. x e. ( B u. C ) ( F ` x ) = y <-> ( E. x e. B ( F ` x ) = y \/ E. x e. C ( F ` x ) = y ) )
8 6 7 bitrdi
 |-  ( ( F Fn A /\ B C_ A /\ C C_ A ) -> ( y e. ( F " ( B u. C ) ) <-> ( E. x e. B ( F ` x ) = y \/ E. x e. C ( F ` x ) = y ) ) )
9 fvelimab
 |-  ( ( F Fn A /\ B C_ A ) -> ( y e. ( F " B ) <-> E. x e. B ( F ` x ) = y ) )
10 9 3adant3
 |-  ( ( F Fn A /\ B C_ A /\ C C_ A ) -> ( y e. ( F " B ) <-> E. x e. B ( F ` x ) = y ) )
11 fvelimab
 |-  ( ( F Fn A /\ C C_ A ) -> ( y e. ( F " C ) <-> E. x e. C ( F ` x ) = y ) )
12 11 3adant2
 |-  ( ( F Fn A /\ B C_ A /\ C C_ A ) -> ( y e. ( F " C ) <-> E. x e. C ( F ` x ) = y ) )
13 10 12 orbi12d
 |-  ( ( F Fn A /\ B C_ A /\ C C_ A ) -> ( ( y e. ( F " B ) \/ y e. ( F " C ) ) <-> ( E. x e. B ( F ` x ) = y \/ E. x e. C ( F ` x ) = y ) ) )
14 8 13 bitr4d
 |-  ( ( F Fn A /\ B C_ A /\ C C_ A ) -> ( y e. ( F " ( B u. C ) ) <-> ( y e. ( F " B ) \/ y e. ( F " C ) ) ) )
15 elun
 |-  ( y e. ( ( F " B ) u. ( F " C ) ) <-> ( y e. ( F " B ) \/ y e. ( F " C ) ) )
16 14 15 bitr4di
 |-  ( ( F Fn A /\ B C_ A /\ C C_ A ) -> ( y e. ( F " ( B u. C ) ) <-> y e. ( ( F " B ) u. ( F " C ) ) ) )
17 16 eqrdv
 |-  ( ( F Fn A /\ B C_ A /\ C C_ A ) -> ( F " ( B u. C ) ) = ( ( F " B ) u. ( F " C ) ) )