This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

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