Metamath Proof Explorer

Theorem unipreima

Description: Preimage of a class union. (Contributed by Thierry Arnoux, 7-Feb-2017)

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

Proof

Step	Hyp	Ref	Expression
1		funfn	$⊢ Fun F \leftrightarrow F Fn dom F$
2		r19.42v	$⊢ \exists x \in A (y \in dom F \land F (y) \in x) \leftrightarrow (y \in dom F \land \exists x \in A F (y) \in x)$
3	2	bicomi	$⊢ (y \in dom F \land \exists x \in A F (y) \in x) \leftrightarrow \exists x \in A (y \in dom F \land F (y) \in x)$
4	3	a1i	$⊢ F Fn dom F \to ((y \in dom F \land \exists x \in A F (y) \in x) \leftrightarrow \exists x \in A (y \in dom F \land F (y) \in x))$
5		eluni2	$⊢ F (y) \in ⋃ A \leftrightarrow \exists x \in A F (y) \in x$
6	5	anbi2i	$⊢ (y \in dom F \land F (y) \in ⋃ A) \leftrightarrow (y \in dom F \land \exists x \in A F (y) \in x)$
7	6	a1i	$⊢ F Fn dom F \to ((y \in dom F \land F (y) \in ⋃ A) \leftrightarrow (y \in dom F \land \exists x \in A F (y) \in x))$
8		elpreima	$⊢ F Fn dom F \to (y \in F^{-1} [x] \leftrightarrow (y \in dom F \land F (y) \in x))$
9	8	rexbidv	$⊢ F Fn dom F \to (\exists x \in A y \in F^{-1} [x] \leftrightarrow \exists x \in A (y \in dom F \land F (y) \in x))$
10	4 7 9	3bitr4d	$⊢ F Fn dom F \to ((y \in dom F \land F (y) \in ⋃ A) \leftrightarrow \exists x \in A y \in F^{-1} [x])$
11		elpreima	$⊢ F Fn dom F \to (y \in F^{-1} [⋃ A] \leftrightarrow (y \in dom F \land F (y) \in ⋃ A))$
12		eliun	$⊢ y \in ⋃_{x \in A} F^{-1} [x] \leftrightarrow \exists x \in A y \in F^{-1} [x]$
13	12	a1i	$⊢ F Fn dom F \to (y \in ⋃_{x \in A} F^{-1} [x] \leftrightarrow \exists x \in A y \in F^{-1} [x])$
14	10 11 13	3bitr4d	$⊢ F Fn dom F \to (y \in F^{-1} [⋃ A] \leftrightarrow y \in ⋃_{x \in A} F^{-1} [x])$
15	14	eqrdv	$⊢ F Fn dom F \to F^{-1} [⋃ A] = ⋃_{x \in A} F^{-1} [x]$
16	1 15	sylbi	$⊢ Fun F \to F^{-1} [⋃ A] = ⋃_{x \in A} F^{-1} [x]$