Definition df-fi 8317

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

Step	Hyp	Ref	Expression
1		cfi 8316	. 2 class fi
2		vx	. . 3 setvar x
3		cvv 3200	. . 3 class _V
4		vz	. . . . . . 7 setvar z
5	4	cv 1482	. . . . . 6 class z
6		vy	. . . . . . . 8 setvar y
7	6	cv 1482	. . . . . . 7 class y
8	7	cint 4475	. . . . . 6 class |^| y
9	5, 8	wceq 1483	. . . . 5 wff z = |^| y
10	2	cv 1482	. . . . . . 7 class x
11	10	cpw 4158	. . . . . 6 class ~P x
12		cfn 7955	. . . . . 6 class Fin
13	11, 12	cin 3573	. . . . 5 class ( ~P x i^i Fin )
14	9, 6, 13	wrex 2913	. . . 4 wff E. y e. ( ~P x i^i Fin ) z = |^| y
15	14, 4	cab 2608	. . 3 class { z | E. y e. ( ~P x i^i Fin ) z = |^| y }
16	2, 3, 15	cmpt 4729	. 2 class ( x e. _V |-> { z | E. y e. ( ~P x i^i Fin ) z = |^| y } )
17	1, 16	wceq 1483	1 wff fi = ( x e. _V |-> { z | E. y e. ( ~P x i^i Fin ) z = |^| y } )

This definition is referenced by:  fival  8318