Metamath Proof Explorer


Theorem oprabss

Description: Structure of an operation class abstraction. (Contributed by NM, 28-Nov-2006)

Ref Expression
Assertion oprabss xyz|φV×V×V

Proof

Step Hyp Ref Expression
1 reloprab Relxyz|φ
2 relssdmrn Relxyz|φxyz|φdomxyz|φ×ranxyz|φ
3 1 2 ax-mp xyz|φdomxyz|φ×ranxyz|φ
4 reldmoprab Reldomxyz|φ
5 df-rel Reldomxyz|φdomxyz|φV×V
6 4 5 mpbi domxyz|φV×V
7 ssv ranxyz|φV
8 xpss12 domxyz|φV×Vranxyz|φVdomxyz|φ×ranxyz|φV×V×V
9 6 7 8 mp2an domxyz|φ×ranxyz|φV×V×V
10 3 9 sstri xyz|φV×V×V