imainss

Description: An upper bound for intersection with an image. Theorem 41 of Suppes p. 66. (Contributed by NM, 11-Aug-2004)

		Ref	Expression
	Assertion	imainss	$⊢ R [A] \cap B \subseteq R [A \cap R^{-1} [B]]$

Proof

Step	Hyp	Ref	Expression
1		vex	$⊢ y \in V$
2		vex	$⊢ x \in V$
3	1 2	brcnv	$⊢ y R^{-1} x \leftrightarrow x R y$
4		19.8a	$⊢ (y \in B \land y R^{-1} x) \to \exists y (y \in B \land y R^{-1} x)$
5	3 4	sylan2br	$⊢ (y \in B \land x R y) \to \exists y (y \in B \land y R^{-1} x)$
6	5	ancoms	$⊢ (x R y \land y \in B) \to \exists y (y \in B \land y R^{-1} x)$
7	6	anim2i	$⊢ (x \in A \land (x R y \land y \in B)) \to (x \in A \land \exists y (y \in B \land y R^{-1} x))$
8		simprl	$⊢ (x \in A \land (x R y \land y \in B)) \to x R y$
9	7 8	jca	$⊢ (x \in A \land (x R y \land y \in B)) \to ((x \in A \land \exists y (y \in B \land y R^{-1} x)) \land x R y)$
10	9	anassrs	$⊢ ((x \in A \land x R y) \land y \in B) \to ((x \in A \land \exists y (y \in B \land y R^{-1} x)) \land x R y)$
11		elin	$⊢ x \in (A \cap R^{-1} [B]) \leftrightarrow (x \in A \land x \in R^{-1} [B])$
12	2	elima2	$⊢ x \in R^{-1} [B] \leftrightarrow \exists y (y \in B \land y R^{-1} x)$
13	12	anbi2i	$⊢ (x \in A \land x \in R^{-1} [B]) \leftrightarrow (x \in A \land \exists y (y \in B \land y R^{-1} x))$
14	11 13	bitri	$⊢ x \in (A \cap R^{-1} [B]) \leftrightarrow (x \in A \land \exists y (y \in B \land y R^{-1} x))$
15	14	anbi1i	$⊢ (x \in (A \cap R^{-1} [B]) \land x R y) \leftrightarrow ((x \in A \land \exists y (y \in B \land y R^{-1} x)) \land x R y)$
16	10 15	sylibr	$⊢ ((x \in A \land x R y) \land y \in B) \to (x \in (A \cap R^{-1} [B]) \land x R y)$
17	16	eximi	$⊢ \exists x ((x \in A \land x R y) \land y \in B) \to \exists x (x \in (A \cap R^{-1} [B]) \land x R y)$
18	1	elima2	$⊢ y \in R [A] \leftrightarrow \exists x (x \in A \land x R y)$
19	18	anbi1i	$⊢ (y \in R [A] \land y \in B) \leftrightarrow (\exists x (x \in A \land x R y) \land y \in B)$
20		elin	$⊢ y \in (R [A] \cap B) \leftrightarrow (y \in R [A] \land y \in B)$
21		19.41v	$⊢ \exists x ((x \in A \land x R y) \land y \in B) \leftrightarrow (\exists x (x \in A \land x R y) \land y \in B)$
22	19 20 21	3bitr4i	$⊢ y \in (R [A] \cap B) \leftrightarrow \exists x ((x \in A \land x R y) \land y \in B)$
23	1	elima2	$⊢ y \in R [A \cap R^{-1} [B]] \leftrightarrow \exists x (x \in (A \cap R^{-1} [B]) \land x R y)$
24	17 22 23	3imtr4i	$⊢ y \in (R [A] \cap B) \to y \in R [A \cap R^{-1} [B]]$
25	24	ssriv	$⊢ R [A] \cap B \subseteq R [A \cap R^{-1} [B]]$

Metamath Proof Explorer

Theorem imainss

Proof