iunpreima

Description: Preimage of an indexed union. (Contributed by Thierry Arnoux, 27-Mar-2018)

		Ref	Expression
	Assertion	iunpreima	$⊢ Fun F \to F^{-1} [⋃_{x \in A} B] = ⋃_{x \in A} F^{-1} [B]$

Step	Hyp	Ref	Expression
1		eliun	$⊢ F (y) \in ⋃_{x \in A} B \leftrightarrow \exists x \in A F (y) \in B$
2	1	a1i	$⊢ Fun F \to (F (y) \in ⋃_{x \in A} B \leftrightarrow \exists x \in A F (y) \in B)$
3	2	rabbidv	$⊢ Fun F \to \{y \in dom F \| F (y) \in ⋃_{x \in A} B\} = \{y \in dom F \| \exists x \in A F (y) \in B\}$
4		funfn	$⊢ Fun F \leftrightarrow F Fn dom F$
5		fncnvima2	$⊢ F Fn dom F \to F^{-1} [⋃_{x \in A} B] = \{y \in dom F \| F (y) \in ⋃_{x \in A} B\}$
6	4 5	sylbi	$⊢ Fun F \to F^{-1} [⋃_{x \in A} B] = \{y \in dom F \| F (y) \in ⋃_{x \in A} B\}$
7		iunrab	$⊢ ⋃_{x \in A} \{y \in dom F \| F (y) \in B\} = \{y \in dom F \| \exists x \in A F (y) \in B\}$
8	7	a1i	$⊢ Fun F \to ⋃_{x \in A} \{y \in dom F \| F (y) \in B\} = \{y \in dom F \| \exists x \in A F (y) \in B\}$
9	3 6 8	3eqtr4d	$⊢ Fun F \to F^{-1} [⋃_{x \in A} B] = ⋃_{x \in A} \{y \in dom F \| F (y) \in B\}$
10		fncnvima2	$⊢ F Fn dom F \to F^{-1} [B] = \{y \in dom F \| F (y) \in B\}$
11	4 10	sylbi	$⊢ Fun F \to F^{-1} [B] = \{y \in dom F \| F (y) \in B\}$
12	11	iuneq2d	$⊢ Fun F \to ⋃_{x \in A} F^{-1} [B] = ⋃_{x \in A} \{y \in dom F \| F (y) \in B\}$
13	9 12	eqtr4d	$⊢ Fun F \to F^{-1} [⋃_{x \in A} B] = ⋃_{x \in A} F^{-1} [B]$

Metamath Proof Explorer