Step |
Hyp |
Ref |
Expression |
1 |
|
isssc.1 |
|- ( ph -> H Fn ( S X. S ) ) |
2 |
|
isssc.2 |
|- ( ph -> J Fn ( T X. T ) ) |
3 |
|
ssc1.3 |
|- ( ph -> H C_cat J ) |
4 |
|
sscrel |
|- Rel C_cat |
5 |
4
|
brrelex2i |
|- ( H C_cat J -> J e. _V ) |
6 |
3 5
|
syl |
|- ( ph -> J e. _V ) |
7 |
2
|
ssclem |
|- ( ph -> ( J e. _V <-> T e. _V ) ) |
8 |
6 7
|
mpbid |
|- ( ph -> T e. _V ) |
9 |
1 2 8
|
isssc |
|- ( ph -> ( H C_cat J <-> ( S C_ T /\ A. x e. S A. y e. S ( x H y ) C_ ( x J y ) ) ) ) |
10 |
3 9
|
mpbid |
|- ( ph -> ( S C_ T /\ A. x e. S A. y e. S ( x H y ) C_ ( x J y ) ) ) |
11 |
10
|
simpld |
|- ( ph -> S C_ T ) |