Metamath Proof Explorer


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