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	biimpi	|- ( F Fn A -> F : A --> ran F )
3	2	adantr	|- ( ( F Fn A /\ X e. A ) -> F : A --> ran F )
4		cnvimass	|- ( `' F " { ( F ` X ) } ) C_ dom F
5		fndm	|- ( F Fn A -> dom F = A )
6	4 5	sseqtrid	|- ( F Fn A -> ( `' F " { ( F ` X ) } ) C_ A )
7	6	adantr	|- ( ( F Fn A /\ X e. A ) -> ( `' F " { ( F ` X ) } ) C_ A )
8		preimafvsnel	|- ( ( F Fn A /\ X e. A ) -> X e. ( `' F " { ( F ` X ) } ) )
9	3 7 8	3jca	|- ( ( F Fn A /\ X e. A ) -> ( F : A --> ran F /\ ( `' F " { ( F ` X ) } ) C_ A /\ X e. ( `' F " { ( F ` X ) } ) ) )
10		fniniseg	|- ( F Fn A -> ( x e. ( `' F " { ( F ` X ) } ) <-> ( x e. A /\ ( F ` x ) = ( F ` X ) ) ) )
11	10	adantr	|- ( ( F Fn A /\ X e. A ) -> ( x e. ( `' F " { ( F ` X ) } ) <-> ( x e. A /\ ( F ` x ) = ( F ` X ) ) ) )
12		simpr	|- ( ( x e. A /\ ( F ` x ) = ( F ` X ) ) -> ( F ` x ) = ( F ` X ) )
13	11 12	syl6bi	|- ( ( F Fn A /\ X e. A ) -> ( x e. ( `' F " { ( F ` X ) } ) -> ( F ` x ) = ( F ` X ) ) )
14	13	ralrimiv	|- ( ( F Fn A /\ X e. A ) -> A. x e. ( `' F " { ( F ` X ) } ) ( F ` x ) = ( F ` X ) )
15		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 ) ) )
16	9 14 15	sylc	|- ( ( F Fn A /\ X e. A ) -> U. ( F " ( `' F " { ( F ` X ) } ) ) = ( F ` X ) )