Theorem imagesset

Description: The Image functor applied to the converse of the subset relationship yields a subset of the subset relationship. (Contributed by Scott Fenton, 14-Apr-2018)

	Ref	Expression
Assertion	imagesset	|- Image `' SSet C_ SSet

Proof

Step	Hyp	Ref	Expression
1		ssid	|- y C_ y
2		sseq2	|- ( z = y -> ( y C_ z <-> y C_ y ) )
3	2	rspcev	|- ( ( y e. x /\ y C_ y ) -> E. z e. x y C_ z )
4	1 3	mpan2	|- ( y e. x -> E. z e. x y C_ z )
5		vex	|- y e. _V
6	5	elima	|- ( y e. ( `' SSet " x ) <-> E. z e. x z `' SSet y )
7		vex	|- z e. _V
8	7 5	brcnv	|- ( z `' SSet y <-> y SSet z )
9	7	brsset	|- ( y SSet z <-> y C_ z )
10	8 9	bitri	|- ( z `' SSet y <-> y C_ z )
11	10	rexbii	|- ( E. z e. x z `' SSet y <-> E. z e. x y C_ z )
12	6 11	bitri	|- ( y e. ( `' SSet " x ) <-> E. z e. x y C_ z )
13	4 12	sylibr	|- ( y e. x -> y e. ( `' SSet " x ) )
14	13	ssriv	|- x C_ ( `' SSet " x )
15		sseq2	|- ( y = ( `' SSet " x ) -> ( x C_ y <-> x C_ ( `' SSet " x ) ) )
16	14 15	mpbiri	|- ( y = ( `' SSet " x ) -> x C_ y )
17		vex	|- x e. _V
18	17 5	brimage	|- ( x Image `' SSet y <-> y = ( `' SSet " x ) )
19		df-br	|- ( x Image `' SSet y <-> <. x , y >. e. Image `' SSet )
20	18 19	bitr3i	|- ( y = ( `' SSet " x ) <-> <. x , y >. e. Image `' SSet )
21	5	brsset	|- ( x SSet y <-> x C_ y )
22		df-br	|- ( x SSet y <-> <. x , y >. e. SSet )
23	21 22	bitr3i	|- ( x C_ y <-> <. x , y >. e. SSet )
24	16 20 23	3imtr3i	|- ( <. x , y >. e. Image `' SSet -> <. x , y >. e. SSet )
25	24	gen2	|- A. x A. y ( <. x , y >. e. Image `' SSet -> <. x , y >. e. SSet )
26		funimage	|- Fun Image `' SSet
27		funrel	|- ( Fun Image `' SSet -> Rel Image `' SSet )
28		ssrel	|- ( Rel Image `' SSet -> ( Image `' SSet C_ SSet <-> A. x A. y ( <. x , y >. e. Image `' SSet -> <. x , y >. e. SSet ) ) )
29	26 27 28	mp2b	|- ( Image `' SSet C_ SSet <-> A. x A. y ( <. x , y >. e. Image `' SSet -> <. x , y >. e. SSet ) )
30	25 29	mpbir	|- Image `' SSet C_ SSet