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		vex	$⊢ x \in V$
7	3 6	brcnv	$⊢ y R^{-1} x \leftrightarrow x R y$
8	7	biranri	$⊢ (x R y \land x \in A) \to y R^{-1} x$
9	5 8	jca	$⊢ (x R y \land x \in A) \to (y \in R [A] \land y R^{-1} x)$
10	9	eximi	$⊢ \exists y (x R y \land x \in A) \to \exists y (y \in R [A] \land y R^{-1} x)$
11	6	eldm	$⊢ x \in dom R \leftrightarrow \exists y x R y$
12	11	anbi1i	$⊢ (x \in dom R \land x \in A) \leftrightarrow (\exists y x R y \land x \in A)$
13		elin	$⊢ x \in (dom R \cap A) \leftrightarrow (x \in dom R \land x \in A)$
14		19.41v	$⊢ \exists y (x R y \land x \in A) \leftrightarrow (\exists y x R y \land x \in A)$
15	12 13 14	3bitr4i	$⊢ x \in (dom R \cap A) \leftrightarrow \exists y (x R y \land x \in A)$
16	6	elima2	$⊢ x \in R^{-1} [R [A]] \leftrightarrow \exists y (y \in R [A] \land y R^{-1} x)$
17	10 15 16	3imtr4i	$⊢ x \in (dom R \cap A) \to x \in R^{-1} [R [A]]$
18	17	ssriv	$⊢ dom R \cap A \subseteq R^{-1} [R [A]]$