Metamath Proof Explorer

Theorem dminss

Description: An upper bound for intersection with a domain. Theorem 40 of Suppes p. 66, who calls it "somewhat surprising". (Contributed by NM, 11-Aug-2004)

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

Proof

Step	Hyp	Ref	Expression
1		19.8a	$⊢ (x \in A \land x R y) \to \exists x (x \in A \land x R y)$
2	1	ancoms	$⊢ (x R y \land x \in A) \to \exists x (x \in A \land x R y)$
3		vex	$⊢ y \in V$
4	3	elima2	$⊢ y \in R [A] \leftrightarrow \exists x (x \in A \land x R y)$
5	2 4	sylibr	$⊢ (x R y \land x \in A) \to y \in R [A]$
6		simpl	$⊢ (x R y \land x \in A) \to x R y$
7		vex	$⊢ x \in V$
8	3 7	brcnv	$⊢ y R^{-1} x \leftrightarrow x R y$
9	6 8	sylibr	$⊢ (x R y \land x \in A) \to y R^{-1} x$
10	5 9	jca	$⊢ (x R y \land x \in A) \to (y \in R [A] \land y R^{-1} x)$
11	10	eximi	$⊢ \exists y (x R y \land x \in A) \to \exists y (y \in R [A] \land y R^{-1} x)$
12	7	eldm	$⊢ x \in dom R \leftrightarrow \exists y x R y$
13	12	anbi1i	$⊢ (x \in dom R \land x \in A) \leftrightarrow (\exists y x R y \land x \in A)$
14		elin	$⊢ x \in (dom R \cap A) \leftrightarrow (x \in dom R \land x \in A)$
15		19.41v	$⊢ \exists y (x R y \land x \in A) \leftrightarrow (\exists y x R y \land x \in A)$
16	13 14 15	3bitr4i	$⊢ x \in (dom R \cap A) \leftrightarrow \exists y (x R y \land x \in A)$
17	7	elima2	$⊢ x \in R^{-1} [R [A]] \leftrightarrow \exists y (y \in R [A] \land y R^{-1} x)$
18	11 16 17	3imtr4i	$⊢ x \in (dom R \cap A) \to x \in R^{-1} [R [A]]$
19	18	ssriv	$⊢ dom R \cap A \subseteq R^{-1} [R [A]]$