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 i^i A ) C_ ( `' R " ( R " A ) )

Proof

Step	Hyp	Ref	Expression
1		19.8a	|- ( ( x e. A /\ x R y ) -> E. x ( x e. A /\ x R y ) )
2	1	ancoms	|- ( ( x R y /\ x e. A ) -> E. x ( x e. A /\ x R y ) )
3		vex	|- y e. _V
4	3	elima2	|- ( y e. ( R " A ) <-> E. x ( x e. A /\ x R y ) )
5	2 4	sylibr	|- ( ( x R y /\ x e. A ) -> y e. ( R " A ) )
6		simpl	|- ( ( x R y /\ x e. A ) -> x R y )
7		vex	|- x e. _V
8	3 7	brcnv	|- ( y `' R x <-> x R y )
9	6 8	sylibr	|- ( ( x R y /\ x e. A ) -> y `' R x )
10	5 9	jca	|- ( ( x R y /\ x e. A ) -> ( y e. ( R " A ) /\ y `' R x ) )
11	10	eximi	|- ( E. y ( x R y /\ x e. A ) -> E. y ( y e. ( R " A ) /\ y `' R x ) )
12	7	eldm	|- ( x e. dom R <-> E. y x R y )
13	12	anbi1i	|- ( ( x e. dom R /\ x e. A ) <-> ( E. y x R y /\ x e. A ) )
14		elin	|- ( x e. ( dom R i^i A ) <-> ( x e. dom R /\ x e. A ) )
15		19.41v	|- ( E. y ( x R y /\ x e. A ) <-> ( E. y x R y /\ x e. A ) )
16	13 14 15	3bitr4i	|- ( x e. ( dom R i^i A ) <-> E. y ( x R y /\ x e. A ) )
17	7	elima2	|- ( x e. ( `' R " ( R " A ) ) <-> E. y ( y e. ( R " A ) /\ y `' R x ) )
18	11 16 17	3imtr4i	|- ( x e. ( dom R i^i A ) -> x e. ( `' R " ( R " A ) ) )
19	18	ssriv	|- ( dom R i^i A ) C_ ( `' R " ( R " A ) )