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 ) ) )