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		vex	|- x e. _V
7	3 6	brcnv	|- ( y `' R x <-> x R y )
8	7	biranri	|- ( ( x R y /\ x e. A ) -> y `' R x )
9	5 8	jca	|- ( ( x R y /\ x e. A ) -> ( y e. ( R " A ) /\ y `' R x ) )
10	9	eximi	|- ( E. y ( x R y /\ x e. A ) -> E. y ( y e. ( R " A ) /\ y `' R x ) )
11	6	eldm	|- ( x e. dom R <-> E. y x R y )
12	11	anbi1i	|- ( ( x e. dom R /\ x e. A ) <-> ( E. y x R y /\ x e. A ) )
13		elin	|- ( x e. ( dom R i^i A ) <-> ( x e. dom R /\ x e. A ) )
14		19.41v	|- ( E. y ( x R y /\ x e. A ) <-> ( E. y x R y /\ x e. A ) )
15	12 13 14	3bitr4i	|- ( x e. ( dom R i^i A ) <-> E. y ( x R y /\ x e. A ) )
16	6	elima2	|- ( x e. ( `' R " ( R " A ) ) <-> E. y ( y e. ( R " A ) /\ y `' R x ) )
17	10 15 16	3imtr4i	|- ( x e. ( dom R i^i A ) -> x e. ( `' R " ( R " A ) ) )
18	17	ssriv	|- ( dom R i^i A ) C_ ( `' R " ( R " A ) )