Theorem uniimafveqt

Description: The union of the image of a subset S of the domain of a function with elements having the same function value is the function value at one of the elements of S . (Contributed by AV, 5-Mar-2024)

	Ref	Expression
Assertion	uniimafveqt	|- ( ( F : A --> B /\ S C_ A /\ X e. S ) -> ( A. x e. S ( F ` x ) = ( F ` X ) -> U. ( F " S ) = ( F ` X ) ) )

Proof

Step	Hyp	Ref	Expression
1		ffun	|- ( F : A --> B -> Fun F )
2	1	3ad2ant1	|- ( ( F : A --> B /\ S C_ A /\ X e. S ) -> Fun F )
3	2	adantr	|- ( ( ( F : A --> B /\ S C_ A /\ X e. S ) /\ A. x e. S ( F ` x ) = ( F ` X ) ) -> Fun F )
4		funiunfv	|- ( Fun F -> U_ y e. S ( F ` y ) = U. ( F " S ) )
5	3 4	syl	|- ( ( ( F : A --> B /\ S C_ A /\ X e. S ) /\ A. x e. S ( F ` x ) = ( F ` X ) ) -> U_ y e. S ( F ` y ) = U. ( F " S ) )
6		simp3	|- ( ( F : A --> B /\ S C_ A /\ X e. S ) -> X e. S )
7		fveqeq2	|- ( x = y -> ( ( F ` x ) = ( F ` X ) <-> ( F ` y ) = ( F ` X ) ) )
8	7	cbvralvw	|- ( A. x e. S ( F ` x ) = ( F ` X ) <-> A. y e. S ( F ` y ) = ( F ` X ) )
9	8	biimpi	|- ( A. x e. S ( F ` x ) = ( F ` X ) -> A. y e. S ( F ` y ) = ( F ` X ) )
10		fveq2	|- ( y = X -> ( F ` y ) = ( F ` X ) )
11	10	iuneqconst	|- ( ( X e. S /\ A. y e. S ( F ` y ) = ( F ` X ) ) -> U_ y e. S ( F ` y ) = ( F ` X ) )
12	6 9 11	syl2an	|- ( ( ( F : A --> B /\ S C_ A /\ X e. S ) /\ A. x e. S ( F ` x ) = ( F ` X ) ) -> U_ y e. S ( F ` y ) = ( F ` X ) )
13	5 12	eqtr3d	|- ( ( ( F : A --> B /\ S C_ A /\ X e. S ) /\ A. x e. S ( F ` x ) = ( F ` X ) ) -> U. ( F " S ) = ( F ` X ) )
14	13	ex	|- ( ( F : A --> B /\ S C_ A /\ X e. S ) -> ( A. x e. S ( F ` x ) = ( F ` X ) -> U. ( F " S ) = ( F ` X ) ) )