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=\bigcup _{i\in I}F\left(i\right)$$
Assertion	fviunfun	$$⊢\left(\mathrm{Fun}U\wedge J\in I\wedge X\in \mathrm{dom}F\left(J\right)\right)\to U\left(X\right)=F\left(J\right)\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		fviunfun.u	$$⊢U=\bigcup _{i\in I}F\left(i\right)$$
2		fveq2	$$⊢i=J\to F\left(i\right)=F\left(J\right)$$
3	2	ssiun2s	$$⊢J\in I\to F\left(J\right)\subseteq \bigcup _{i\in I}F\left(i\right)$$
4	3 1	sseqtrrdi	$$⊢J\in I\to F\left(J\right)\subseteq U$$
5		funssfv	$$⊢\left(\mathrm{Fun}U\wedge F\left(J\right)\subseteq U\wedge X\in \mathrm{dom}F\left(J\right)\right)\to U\left(X\right)=F\left(J\right)\left(X\right)$$
6	4 5	syl3an2	$$⊢\left(\mathrm{Fun}U\wedge J\in I\wedge X\in \mathrm{dom}F\left(J\right)\right)\to U\left(X\right)=F\left(J\right)\left(X\right)$$