Metamath Proof Explorer

Theorem oprssdm

Description: Domain of closure of an operation. (Contributed by NM, 24-Aug-1995)

Ref Expression
Hypotheses oprssdm.1 
|- -. (/) e. S
oprssdm.2 
|- ( ( x e. S /\ y e. S ) -> ( x F y ) e. S )
Assertion oprssdm 
|- ( S X. S ) C_ dom F

Proof

Step Hyp Ref Expression
1 oprssdm.1 
 |-  -. (/) e. S
2 oprssdm.2 
 |-  ( ( x e. S /\ y e. S ) -> ( x F y ) e. S )
3 relxp 
 |-  Rel ( S X. S )
4 opelxp 
 |-  ( <. x , y >. e. ( S X. S ) <-> ( x e. S /\ y e. S ) )
5 df-ov 
 |-  ( x F y ) = ( F ` <. x , y >. )
6 5 2 eqeltrrid 
 |-  ( ( x e. S /\ y e. S ) -> ( F ` <. x , y >. ) e. S )
7 ndmfv 
 |-  ( -. <. x , y >. e. dom F -> ( F ` <. x , y >. ) = (/) )
8 7 eleq1d 
 |-  ( -. <. x , y >. e. dom F -> ( ( F ` <. x , y >. ) e. S <-> (/) e. S ) )
9 1 8 mtbiri 
 |-  ( -. <. x , y >. e. dom F -> -. ( F ` <. x , y >. ) e. S )
10 9 con4i 
 |-  ( ( F ` <. x , y >. ) e. S -> <. x , y >. e. dom F )
11 6 10 syl 
 |-  ( ( x e. S /\ y e. S ) -> <. x , y >. e. dom F )
12 4 11 sylbi 
 |-  ( <. x , y >. e. ( S X. S ) -> <. x , y >. e. dom F )
13 3 12 relssi 
 |-  ( S X. S ) C_ dom F