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 |