Definition df-fi 8317

Description: Function whose value is the class of all the finite intersections of the elements of 𝑥. (Contributed by FL, 27-Apr-2008.)

Assertion

Ref	Expression
df-fi	⊢ fi = (𝑥 ∈ V ↦ {𝑧 ∣ ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑧 = ∩ 𝑦})

Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-fi

Step	Hyp	Ref	Expression
1		cfi 8316	. 2 class fi
2		vx	. . 3 setvar 𝑥
3		cvv 3200	. . 3 class V
4		vz	. . . . . . 7 setvar 𝑧
5	4	cv 1482	. . . . . 6 class 𝑧
6		vy	. . . . . . . 8 setvar 𝑦
7	6	cv 1482	. . . . . . 7 class 𝑦
8	7	cint 4475	. . . . . 6 class ∩ 𝑦
9	5, 8	wceq 1483	. . . . 5 wff 𝑧 = ∩ 𝑦
10	2	cv 1482	. . . . . . 7 class 𝑥
11	10	cpw 4158	. . . . . 6 class 𝒫 𝑥
12		cfn 7955	. . . . . 6 class Fin
13	11, 12	cin 3573	. . . . 5 class (𝒫 𝑥 ∩ Fin)
14	9, 6, 13	wrex 2913	. . . 4 wff ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑧 = ∩ 𝑦
15	14, 4	cab 2608	. . 3 class {𝑧 ∣ ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑧 = ∩ 𝑦}
16	2, 3, 15	cmpt 4729	. 2 class (𝑥 ∈ V ↦ {𝑧 ∣ ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑧 = ∩ 𝑦})
17	1, 16	wceq 1483	1 wff fi = (𝑥 ∈ V ↦ {𝑧 ∣ ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑧 = ∩ 𝑦})

This definition is referenced by:  fival  8318