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

Definition df-fi 8200
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
StepHypRef Expression
1 cfi 8199 . 2 class fi
2 vx . . 3 setvar 𝑥
3 cvv 3173 . . 3 class V
4 vz . . . . . . 7 setvar 𝑧
54cv 1474 . . . . . 6 class 𝑧
6 vy . . . . . . . 8 setvar 𝑦
76cv 1474 . . . . . . 7 class 𝑦
87cint 4410 . . . . . 6 class 𝑦
95, 8wceq 1475 . . . . 5 wff 𝑧 = 𝑦
102cv 1474 . . . . . . 7 class 𝑥
1110cpw 4108 . . . . . 6 class 𝒫 𝑥
12 cfn 7841 . . . . . 6 class Fin
1311, 12cin 3539 . . . . 5 class (𝒫 𝑥 ∩ Fin)
149, 6, 13wrex 2897 . . . 4 wff 𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑧 = 𝑦
1514, 4cab 2596 . . 3 class {𝑧 ∣ ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑧 = 𝑦}
162, 3, 15cmpt 4643 . 2 class (𝑥 ∈ V ↦ {𝑧 ∣ ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑧 = 𝑦})
171, 16wceq 1475 1 wff fi = (𝑥 ∈ V ↦ {𝑧 ∣ ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑧 = 𝑦})
Colors of variables: wff setvar class
This definition is referenced by:  fival  8201
  Copyright terms: Public domain W3C validator