Theorem uniimaelsetpreimafv

Description: The union of the image of an element of the preimage of a function value is an element of the range of the function. (Contributed by AV, 5-Mar-2024) (Revised by AV, 22-Mar-2024)

	Ref	Expression
Hypothesis	setpreimafvex.p	|- P = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) }
Assertion	uniimaelsetpreimafv	|- ( ( F Fn A /\ S e. P ) -> U. ( F " S ) e. ran F )

Proof

Step	Hyp	Ref	Expression
1		setpreimafvex.p	|- P = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) }
2	1	0nelsetpreimafv	|- ( F Fn A -> (/) e/ P )
3		elnelne2	|- ( ( S e. P /\ (/) e/ P ) -> S =/= (/) )
4		n0	|- ( S =/= (/) <-> E. y y e. S )
5	3 4	sylib	|- ( ( S e. P /\ (/) e/ P ) -> E. y y e. S )
6	5	expcom	|- ( (/) e/ P -> ( S e. P -> E. y y e. S ) )
7	2 6	syl	|- ( F Fn A -> ( S e. P -> E. y y e. S ) )
8	7	imp	|- ( ( F Fn A /\ S e. P ) -> E. y y e. S )
9	1	imaelsetpreimafv	|- ( ( F Fn A /\ S e. P /\ y e. S ) -> ( F " S ) = { ( F ` y ) } )
10	9	3expa	|- ( ( ( F Fn A /\ S e. P ) /\ y e. S ) -> ( F " S ) = { ( F ` y ) } )
11	10	unieqd	|- ( ( ( F Fn A /\ S e. P ) /\ y e. S ) -> U. ( F " S ) = U. { ( F ` y ) } )
12		fvex	|- ( F ` y ) e. _V
13	12	unisn	|- U. { ( F ` y ) } = ( F ` y )
14	11 13	eqtrdi	|- ( ( ( F Fn A /\ S e. P ) /\ y e. S ) -> U. ( F " S ) = ( F ` y ) )
15		dffn3	|- ( F Fn A <-> F : A --> ran F )
16	15	biimpi	|- ( F Fn A -> F : A --> ran F )
17	16	ad2antrr	|- ( ( ( F Fn A /\ S e. P ) /\ y e. S ) -> F : A --> ran F )
18	1	elsetpreimafvssdm	|- ( ( F Fn A /\ S e. P ) -> S C_ A )
19	18	sselda	|- ( ( ( F Fn A /\ S e. P ) /\ y e. S ) -> y e. A )
20	17 19	ffvelrnd	|- ( ( ( F Fn A /\ S e. P ) /\ y e. S ) -> ( F ` y ) e. ran F )
21	14 20	eqeltrd	|- ( ( ( F Fn A /\ S e. P ) /\ y e. S ) -> U. ( F " S ) e. ran F )
22	8 21	exlimddv	|- ( ( F Fn A /\ S e. P ) -> U. ( F " S ) e. ran F )