Metamath Proof Explorer


Theorem oprabss

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

Ref Expression
Assertion oprabss
|- { <. <. x , y >. , z >. | ph } C_ ( ( _V X. _V ) X. _V )

Proof

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 )