Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-indcls Unicode version

Definition df-indcls 25994
Description: Definition of an inductive closure. Top down definition. Gallier p. 19 (Contributed by FL, 14-Jan-2014.)
Assertion
Ref Expression
df-indcls  |-  IndCls  =  ( x  e.  _V , 
y  e.  _V  |->  |^|
{ a  |  ( x  C_  a  /\  A. f  e.  y  A. j  e.  ( dom  f  i^i  ~P ( _V 
X.  a ) ) ( f `  j
)  e.  a ) } )
Distinct variable group:    x, y, a, f, j

Detailed syntax breakdown of Definition df-indcls
StepHypRef Expression
1 clincl 25993 . 2  class  IndCls
2 vx . . 3  set  x
3 vy . . 3  set  y
4 cvv 2788 . . 3  class  _V
52cv 1622 . . . . . . 7  class  x
6 va . . . . . . . 8  set  a
76cv 1622 . . . . . . 7  class  a
85, 7wss 3152 . . . . . 6  wff  x  C_  a
9 vj . . . . . . . . . . 11  set  j
109cv 1622 . . . . . . . . . 10  class  j
11 vf . . . . . . . . . . 11  set  f
1211cv 1622 . . . . . . . . . 10  class  f
1310, 12cfv 5255 . . . . . . . . 9  class  ( f `
 j )
1413, 7wcel 1684 . . . . . . . 8  wff  ( f `
 j )  e.  a
1512cdm 4689 . . . . . . . . 9  class  dom  f
164, 7cxp 4687 . . . . . . . . . 10  class  ( _V 
X.  a )
1716cpw 3625 . . . . . . . . 9  class  ~P ( _V  X.  a )
1815, 17cin 3151 . . . . . . . 8  class  ( dom  f  i^i  ~P ( _V  X.  a ) )
1914, 9, 18wral 2543 . . . . . . 7  wff  A. j  e.  ( dom  f  i^i 
~P ( _V  X.  a ) ) ( f `  j )  e.  a
203cv 1622 . . . . . . 7  class  y
2119, 11, 20wral 2543 . . . . . 6  wff  A. f  e.  y  A. j  e.  ( dom  f  i^i 
~P ( _V  X.  a ) ) ( f `  j )  e.  a
228, 21wa 358 . . . . 5  wff  ( x 
C_  a  /\  A. f  e.  y  A. j  e.  ( dom  f  i^i  ~P ( _V 
X.  a ) ) ( f `  j
)  e.  a )
2322, 6cab 2269 . . . 4  class  { a  |  ( x  C_  a  /\  A. f  e.  y  A. j  e.  ( dom  f  i^i 
~P ( _V  X.  a ) ) ( f `  j )  e.  a ) }
2423cint 3862 . . 3  class  |^| { a  |  ( x  C_  a  /\  A. f  e.  y  A. j  e.  ( dom  f  i^i 
~P ( _V  X.  a ) ) ( f `  j )  e.  a ) }
252, 3, 4, 4, 24cmpt2 5860 . 2  class  ( x  e.  _V ,  y  e.  _V  |->  |^| { a  |  ( x  C_  a  /\  A. f  e.  y  A. j  e.  ( dom  f  i^i 
~P ( _V  X.  a ) ) ( f `  j )  e.  a ) } )
261, 25wceq 1623 1  wff  IndCls  =  ( x  e.  _V , 
y  e.  _V  |->  |^|
{ a  |  ( x  C_  a  /\  A. f  e.  y  A. j  e.  ( dom  f  i^i  ~P ( _V 
X.  a ) ) ( f `  j
)  e.  a ) } )
Colors of variables: wff set class
This definition is referenced by:  indcls2  25996
  Copyright terms: Public domain W3C validator