Step |
Hyp |
Ref |
Expression |
1 |
|
reloprab |
|- Rel { <. <. x , y >. , z >. | ph } |
2 |
|
relssdmrn |
|- ( Rel { <. <. x , y >. , z >. | ph } -> { <. <. x , y >. , z >. | ph } C_ ( dom { <. <. x , y >. , z >. | ph } X. ran { <. <. x , y >. , z >. | ph } ) ) |
3 |
1 2
|
ax-mp |
|- { <. <. x , y >. , z >. | ph } C_ ( dom { <. <. x , y >. , z >. | ph } X. ran { <. <. x , y >. , z >. | ph } ) |
4 |
|
reldmoprab |
|- Rel dom { <. <. x , y >. , z >. | ph } |
5 |
|
df-rel |
|- ( Rel dom { <. <. x , y >. , z >. | ph } <-> dom { <. <. x , y >. , z >. | ph } C_ ( _V X. _V ) ) |
6 |
4 5
|
mpbi |
|- dom { <. <. x , y >. , z >. | ph } C_ ( _V X. _V ) |
7 |
|
ssv |
|- ran { <. <. x , y >. , z >. | ph } C_ _V |
8 |
|
xpss12 |
|- ( ( dom { <. <. x , y >. , z >. | ph } C_ ( _V X. _V ) /\ ran { <. <. x , y >. , z >. | ph } C_ _V ) -> ( dom { <. <. x , y >. , z >. | ph } X. ran { <. <. x , y >. , z >. | ph } ) C_ ( ( _V X. _V ) X. _V ) ) |
9 |
6 7 8
|
mp2an |
|- ( dom { <. <. x , y >. , z >. | ph } X. ran { <. <. x , y >. , z >. | ph } ) C_ ( ( _V X. _V ) X. _V ) |
10 |
3 9
|
sstri |
|- { <. <. x , y >. , z >. | ph } C_ ( ( _V X. _V ) X. _V ) |