MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-fi Structured version   Unicode version

Definition df-fi 7653
Description: Function whose value is the class of all the finite intersections of the elements of  x. (Contributed by FL, 27-Apr-2008.)
Assertion
Ref Expression
df-fi  |-  fi  =  ( x  e.  _V  |->  { z  |  E. y  e.  ( ~P x  i^i  Fin ) z  =  |^| y } )
Distinct variable group:    x, y, z

Detailed syntax breakdown of Definition df-fi
StepHypRef Expression
1 cfi 7652 . 2  class  fi
2 vx . . 3  setvar  x
3 cvv 2967 . . 3  class  _V
4 vz . . . . . . 7  setvar  z
54cv 1368 . . . . . 6  class  z
6 vy . . . . . . . 8  setvar  y
76cv 1368 . . . . . . 7  class  y
87cint 4123 . . . . . 6  class  |^| y
95, 8wceq 1369 . . . . 5  wff  z  = 
|^| y
102cv 1368 . . . . . . 7  class  x
1110cpw 3855 . . . . . 6  class  ~P x
12 cfn 7302 . . . . . 6  class  Fin
1311, 12cin 3322 . . . . 5  class  ( ~P x  i^i  Fin )
149, 6, 13wrex 2711 . . . 4  wff  E. y  e.  ( ~P x  i^i 
Fin ) z  = 
|^| y
1514, 4cab 2424 . . 3  class  { z  |  E. y  e.  ( ~P x  i^i 
Fin ) z  = 
|^| y }
162, 3, 15cmpt 4345 . 2  class  ( x  e.  _V  |->  { z  |  E. y  e.  ( ~P x  i^i 
Fin ) z  = 
|^| y } )
171, 16wceq 1369 1  wff  fi  =  ( x  e.  _V  |->  { z  |  E. y  e.  ( ~P x  i^i  Fin ) z  =  |^| y } )
Colors of variables: wff setvar class
This definition is referenced by:  fival  7654
  Copyright terms: Public domain W3C validator