Theorem fviunfun

Description: The function value of an indexed union is the value of one of the indexed functions. (Contributed by AV, 4-Nov-2023)

	Ref	Expression
Hypothesis	fviunfun.u	|- U = U_ i e. I ( F ` i )
Assertion	fviunfun	|- ( ( Fun U /\ J e. I /\ X e. dom ( F ` J ) ) -> ( U ` X ) = ( ( F ` J ) ` X ) )

Proof

Step	Hyp	Ref	Expression
1		fviunfun.u	|- U = U_ i e. I ( F ` i )
2		fveq2	|- ( i = J -> ( F ` i ) = ( F ` J ) )
3	2	ssiun2s	|- ( J e. I -> ( F ` J ) C_ U_ i e. I ( F ` i ) )
4	3 1	sseqtrrdi	|- ( J e. I -> ( F ` J ) C_ U )
5		funssfv	|- ( ( Fun U /\ ( F ` J ) C_ U /\ X e. dom ( F ` J ) ) -> ( U ` X ) = ( ( F ` J ) ` X ) )
6	4 5	syl3an2	|- ( ( Fun U /\ J e. I /\ X e. dom ( F ` J ) ) -> ( U ` X ) = ( ( F ` J ) ` X ) )