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	⊢ 𝑈 = ∪ 𝑖 ∈ 𝐼 ( 𝐹 ‘ 𝑖 )
Assertion	fviunfun	⊢ ( ( Fun 𝑈 ∧ 𝐽 ∈ 𝐼 ∧ 𝑋 ∈ dom ( 𝐹 ‘ 𝐽 ) ) → ( 𝑈 ‘ 𝑋 ) = ( ( 𝐹 ‘ 𝐽 ) ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		fviunfun.u	⊢ 𝑈 = ∪ 𝑖 ∈ 𝐼 ( 𝐹 ‘ 𝑖 )
2		fveq2	⊢ ( 𝑖 = 𝐽 → ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝐽 ) )
3	2	ssiun2s	⊢ ( 𝐽 ∈ 𝐼 → ( 𝐹 ‘ 𝐽 ) ⊆ ∪ 𝑖 ∈ 𝐼 ( 𝐹 ‘ 𝑖 ) )
4	3 1	sseqtrrdi	⊢ ( 𝐽 ∈ 𝐼 → ( 𝐹 ‘ 𝐽 ) ⊆ 𝑈 )
5		funssfv	⊢ ( ( Fun 𝑈 ∧ ( 𝐹 ‘ 𝐽 ) ⊆ 𝑈 ∧ 𝑋 ∈ dom ( 𝐹 ‘ 𝐽 ) ) → ( 𝑈 ‘ 𝑋 ) = ( ( 𝐹 ‘ 𝐽 ) ‘ 𝑋 ) )
6	4 5	syl3an2	⊢ ( ( Fun 𝑈 ∧ 𝐽 ∈ 𝐼 ∧ 𝑋 ∈ dom ( 𝐹 ‘ 𝐽 ) ) → ( 𝑈 ‘ 𝑋 ) = ( ( 𝐹 ‘ 𝐽 ) ‘ 𝑋 ) )