Theorem uniimaprimaeqfv

Description: The union of the image of the preimage of a function value is the function value. (Contributed by AV, 12-Mar-2024)

	Ref	Expression
Assertion	uniimaprimaeqfv	|- ( ( F Fn A /\ X e. A ) -> U. ( F " ( `' F " { ( F ` X ) } ) ) = ( F ` X ) )

Proof

Step	Hyp	Ref	Expression
1		dffn3	|- ( F Fn A <-> F : A --> ran F )
2	1	birani	|- ( ( F Fn A /\ X e. A ) -> F : A --> ran F )
3		cnvimass	|- ( `' F " { ( F ` X ) } ) C_ dom F
4		fndm	|- ( F Fn A -> dom F = A )
5	3 4	sseqtrid	|- ( F Fn A -> ( `' F " { ( F ` X ) } ) C_ A )
6	5	adantr	|- ( ( F Fn A /\ X e. A ) -> ( `' F " { ( F ` X ) } ) C_ A )
7		preimafvsnel	|- ( ( F Fn A /\ X e. A ) -> X e. ( `' F " { ( F ` X ) } ) )
8	2 6 7	3jca	|- ( ( F Fn A /\ X e. A ) -> ( F : A --> ran F /\ ( `' F " { ( F ` X ) } ) C_ A /\ X e. ( `' F " { ( F ` X ) } ) ) )
9		fniniseg	|- ( F Fn A -> ( x e. ( `' F " { ( F ` X ) } ) <-> ( x e. A /\ ( F ` x ) = ( F ` X ) ) ) )
10	9	adantr	|- ( ( F Fn A /\ X e. A ) -> ( x e. ( `' F " { ( F ` X ) } ) <-> ( x e. A /\ ( F ` x ) = ( F ` X ) ) ) )
11		simpr	|- ( ( x e. A /\ ( F ` x ) = ( F ` X ) ) -> ( F ` x ) = ( F ` X ) )
12	10 11	biimtrdi	|- ( ( F Fn A /\ X e. A ) -> ( x e. ( `' F " { ( F ` X ) } ) -> ( F ` x ) = ( F ` X ) ) )
13	12	ralrimiv	|- ( ( F Fn A /\ X e. A ) -> A. x e. ( `' F " { ( F ` X ) } ) ( F ` x ) = ( F ` X ) )
14		uniimafveqt	|- ( ( F : A --> ran F /\ ( `' F " { ( F ` X ) } ) C_ A /\ X e. ( `' F " { ( F ` X ) } ) ) -> ( A. x e. ( `' F " { ( F ` X ) } ) ( F ` x ) = ( F ` X ) -> U. ( F " ( `' F " { ( F ` X ) } ) ) = ( F ` X ) ) )
15	8 13 14	sylc	|- ( ( F Fn A /\ X e. A ) -> U. ( F " ( `' F " { ( F ` X ) } ) ) = ( F ` X ) )