Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-cap Structured version   Unicode version

Definition df-cap 29747
Description: Define the little cap function. See brcap 29818 for its value. (Contributed by Scott Fenton, 17-Apr-2014.)
Assertion
Ref Expression
df-cap  |- Cap  =  ( ( ( _V  X.  _V )  X.  _V )  \  ran  ( ( _V 
(x)  _E  )  /_\  ( ( ( `' 1st  o.  _E  )  i^i  ( `' 2nd  o.  _E  )
)  (x)  _V )
) )

Detailed syntax breakdown of Definition df-cap
StepHypRef Expression
1 ccap 29724 . 2  class Cap
2 cvv 3106 . . . . 5  class  _V
32, 2cxp 4986 . . . 4  class  ( _V 
X.  _V )
43, 2cxp 4986 . . 3  class  ( ( _V  X.  _V )  X.  _V )
5 cep 4778 . . . . . 6  class  _E
62, 5ctxp 29707 . . . . 5  class  ( _V 
(x)  _E  )
7 c1st 6771 . . . . . . . . 9  class  1st
87ccnv 4987 . . . . . . . 8  class  `' 1st
98, 5ccom 4992 . . . . . . 7  class  ( `' 1st  o.  _E  )
10 c2nd 6772 . . . . . . . . 9  class  2nd
1110ccnv 4987 . . . . . . . 8  class  `' 2nd
1211, 5ccom 4992 . . . . . . 7  class  ( `' 2nd  o.  _E  )
139, 12cin 3460 . . . . . 6  class  ( ( `' 1st  o.  _E  )  i^i  ( `' 2nd  o.  _E  ) )
1413, 2ctxp 29707 . . . . 5  class  ( ( ( `' 1st  o.  _E  )  i^i  ( `' 2nd  o.  _E  )
)  (x)  _V )
156, 14csymdif 3714 . . . 4  class  ( ( _V  (x)  _E  )  /_\  ( ( ( `' 1st  o.  _E  )  i^i  ( `' 2nd  o.  _E  ) )  (x)  _V ) )
1615crn 4989 . . 3  class  ran  (
( _V  (x)  _E  )  /_\  ( ( ( `' 1st  o.  _E  )  i^i  ( `' 2nd  o.  _E  ) )  (x)  _V ) )
174, 16cdif 3458 . 2  class  ( ( ( _V  X.  _V )  X.  _V )  \  ran  ( ( _V  (x)  _E  )  /_\  ( ( ( `' 1st  o.  _E  )  i^i  ( `' 2nd  o.  _E  ) )  (x)  _V ) ) )
181, 17wceq 1398 1  wff Cap  =  ( ( ( _V  X.  _V )  X.  _V )  \  ran  ( ( _V 
(x)  _E  )  /_\  ( ( ( `' 1st  o.  _E  )  i^i  ( `' 2nd  o.  _E  )
)  (x)  _V )
) )
Colors of variables: wff setvar class
This definition is referenced by:  brcap  29818
  Copyright terms: Public domain W3C validator