This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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