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	syl6bb	|- ( ( 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	syl6bbr	|- ( ( 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 ) ) )