iinpreima

		Ref	Expression
	Assertion	iinpreima	$⊢ (Fun F \land A \neq \emptyset) \to F^{-1} [⋂_{x \in A} B] = ⋂_{x \in A} F^{-1} [B]$

Proof

Step	Hyp	Ref	Expression
1		simpll	$⊢ ((Fun F \land A \neq \emptyset) \land y \in F^{-1} [⋂_{x \in A} B]) \to Fun F$
2		cnvimass	$⊢ F^{-1} [⋂_{x \in A} B] \subseteq dom F$
3	2	sseli	$⊢ y \in F^{-1} [⋂_{x \in A} B] \to y \in dom F$
4	3	adantl	$⊢ ((Fun F \land A \neq \emptyset) \land y \in F^{-1} [⋂_{x \in A} B]) \to y \in dom F$
5		fvex	$⊢ F (y) \in V$
6		fvimacnvi	$⊢ (Fun F \land y \in F^{-1} [⋂_{x \in A} B]) \to F (y) \in ⋂_{x \in A} B$
7	6	adantlr	$⊢ ((Fun F \land A \neq \emptyset) \land y \in F^{-1} [⋂_{x \in A} B]) \to F (y) \in ⋂_{x \in A} B$
8		eliin	$⊢ F (y) \in V \to (F (y) \in ⋂_{x \in A} B \leftrightarrow \forall x \in A F (y) \in B)$
9	8	biimpa	$⊢ (F (y) \in V \land F (y) \in ⋂_{x \in A} B) \to \forall x \in A F (y) \in B$
10	5 7 9	sylancr	$⊢ ((Fun F \land A \neq \emptyset) \land y \in F^{-1} [⋂_{x \in A} B]) \to \forall x \in A F (y) \in B$
11		fvimacnv	$⊢ (Fun F \land y \in dom F) \to (F (y) \in B \leftrightarrow y \in F^{-1} [B])$
12	11	ralbidv	$⊢ (Fun F \land y \in dom F) \to (\forall x \in A F (y) \in B \leftrightarrow \forall x \in A y \in F^{-1} [B])$
13	12	biimpa	$⊢ ((Fun F \land y \in dom F) \land \forall x \in A F (y) \in B) \to \forall x \in A y \in F^{-1} [B]$
14	1 4 10 13	syl21anc	$⊢ ((Fun F \land A \neq \emptyset) \land y \in F^{-1} [⋂_{x \in A} B]) \to \forall x \in A y \in F^{-1} [B]$
15		eliin	$⊢ y \in V \to (y \in ⋂_{x \in A} F^{-1} [B] \leftrightarrow \forall x \in A y \in F^{-1} [B])$
16	15	elv	$⊢ y \in ⋂_{x \in A} F^{-1} [B] \leftrightarrow \forall x \in A y \in F^{-1} [B]$
17	14 16	sylibr	$⊢ ((Fun F \land A \neq \emptyset) \land y \in F^{-1} [⋂_{x \in A} B]) \to y \in ⋂_{x \in A} F^{-1} [B]$
18		simpll	$⊢ ((Fun F \land A \neq \emptyset) \land y \in ⋂_{x \in A} F^{-1} [B]) \to Fun F$
19	15	biimpd	$⊢ y \in V \to (y \in ⋂_{x \in A} F^{-1} [B] \to \forall x \in A y \in F^{-1} [B])$
20	19	elv	$⊢ y \in ⋂_{x \in A} F^{-1} [B] \to \forall x \in A y \in F^{-1} [B]$
21	20	adantl	$⊢ ((Fun F \land A \neq \emptyset) \land y \in ⋂_{x \in A} F^{-1} [B]) \to \forall x \in A y \in F^{-1} [B]$
22		fvimacnvi	$⊢ (Fun F \land y \in F^{-1} [B]) \to F (y) \in B$
23	22	ex	$⊢ Fun F \to (y \in F^{-1} [B] \to F (y) \in B)$
24	23	ralimdv	$⊢ Fun F \to (\forall x \in A y \in F^{-1} [B] \to \forall x \in A F (y) \in B)$
25	18 21 24	sylc	$⊢ ((Fun F \land A \neq \emptyset) \land y \in ⋂_{x \in A} F^{-1} [B]) \to \forall x \in A F (y) \in B$
26	5 8	ax-mp	$⊢ F (y) \in ⋂_{x \in A} B \leftrightarrow \forall x \in A F (y) \in B$
27	25 26	sylibr	$⊢ ((Fun F \land A \neq \emptyset) \land y \in ⋂_{x \in A} F^{-1} [B]) \to F (y) \in ⋂_{x \in A} B$
28		r19.2zb	$⊢ A \neq \emptyset \leftrightarrow (\forall x \in A y \in F^{-1} [B] \to \exists x \in A y \in F^{-1} [B])$
29	28	biimpi	$⊢ A \neq \emptyset \to (\forall x \in A y \in F^{-1} [B] \to \exists x \in A y \in F^{-1} [B])$
30		cnvimass	$⊢ F^{-1} [B] \subseteq dom F$
31	30	sseli	$⊢ y \in F^{-1} [B] \to y \in dom F$
32	31	rexlimivw	$⊢ \exists x \in A y \in F^{-1} [B] \to y \in dom F$
33	29 32	syl6	$⊢ A \neq \emptyset \to (\forall x \in A y \in F^{-1} [B] \to y \in dom F)$
34	16 33	syl5bi	$⊢ A \neq \emptyset \to (y \in ⋂_{x \in A} F^{-1} [B] \to y \in dom F)$
35	34	adantl	$⊢ (Fun F \land A \neq \emptyset) \to (y \in ⋂_{x \in A} F^{-1} [B] \to y \in dom F)$
36	35	imp	$⊢ ((Fun F \land A \neq \emptyset) \land y \in ⋂_{x \in A} F^{-1} [B]) \to y \in dom F$
37		fvimacnv	$⊢ (Fun F \land y \in dom F) \to (F (y) \in ⋂_{x \in A} B \leftrightarrow y \in F^{-1} [⋂_{x \in A} B])$
38	18 36 37	syl2anc	$⊢ ((Fun F \land A \neq \emptyset) \land y \in ⋂_{x \in A} F^{-1} [B]) \to (F (y) \in ⋂_{x \in A} B \leftrightarrow y \in F^{-1} [⋂_{x \in A} B])$
39	27 38	mpbid	$⊢ ((Fun F \land A \neq \emptyset) \land y \in ⋂_{x \in A} F^{-1} [B]) \to y \in F^{-1} [⋂_{x \in A} B]$
40	17 39	impbida	$⊢ (Fun F \land A \neq \emptyset) \to (y \in F^{-1} [⋂_{x \in A} B] \leftrightarrow y \in ⋂_{x \in A} F^{-1} [B])$
41	40	eqrdv	$⊢ (Fun F \land A \neq \emptyset) \to F^{-1} [⋂_{x \in A} B] = ⋂_{x \in A} F^{-1} [B]$

Metamath Proof Explorer

Theorem iinpreima

Proof