| 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 |