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 )