intimafv

Description: The intersection of an image set, as an indexed intersection of function values. (Contributed by Thierry Arnoux, 15-Jun-2024)

		Ref	Expression
	Assertion	intimafv	$⊢ (Fun F \land A \subseteq dom F) \to ⋂ F [A] = ⋂_{x \in A} F (x)$

Step	Hyp	Ref	Expression
1		dfimafn	$⊢ (Fun F \land A \subseteq dom F) \to F [A] = \{y \| \exists x \in A F (x) = y\}$
2	1	inteqd	$⊢ (Fun F \land A \subseteq dom F) \to ⋂ F [A] = ⋂ \{y \| \exists x \in A F (x) = y\}$
3		fvex	$⊢ F (x) \in V$
4	3	rgenw	$⊢ \forall x \in A F (x) \in V$
5		iinabrex	$⊢ \forall x \in A F (x) \in V \to ⋂_{x \in A} F (x) = ⋂ \{y \| \exists x \in A y = F (x)\}$
6	4 5	ax-mp	$⊢ ⋂_{x \in A} F (x) = ⋂ \{y \| \exists x \in A y = F (x)\}$
7		eqcom	$⊢ F (x) = y \leftrightarrow y = F (x)$
8	7	rexbii	$⊢ \exists x \in A F (x) = y \leftrightarrow \exists x \in A y = F (x)$
9	8	abbii	$⊢ \{y \| \exists x \in A F (x) = y\} = \{y \| \exists x \in A y = F (x)\}$
10	9	inteqi	$⊢ ⋂ \{y \| \exists x \in A F (x) = y\} = ⋂ \{y \| \exists x \in A y = F (x)\}$
11	6 10	eqtr4i	$⊢ ⋂_{x \in A} F (x) = ⋂ \{y \| \exists x \in A F (x) = y\}$
12	2 11	eqtr4di	$⊢ (Fun F \land A \subseteq dom F) \to ⋂ F [A] = ⋂_{x \in A} F (x)$

Metamath Proof Explorer