This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-ind

Description: Define the indicator function generator. It generates an indicator function ( ( _IndO )A ) for a given domain O and a given subset A of the domain, see indval . In contrast to the definitions and notations in Wikipedia and Lang2 p. 3, the domain and the subset are always mentioned explicitly. (Contributed by Thierry Arnoux, 20-Jan-2017)

Ref Expression
Assertion df-ind ⊢ 𝟙 = o ∈ V ⟼ a ∈ 𝒫 o ⟼ x ∈ o ⟼ if x ∈ a 1 0

Detailed syntax breakdown

Step Hyp Ref Expression
0 cind class 𝟙
1 vo setvar o
2 cvv class V
3 va setvar a
4 1 cv setvar o
5 4 cpw class 𝒫 o
6 vx setvar x
7 6 cv setvar x
8 3 cv setvar a
9 7 8 wcel wff x ∈ a
10 c1 class 1
11 cc0 class 0
12 9 10 11 cif class if x ∈ a 1 0
13 6 4 12 cmpt class x ∈ o ⟼ if x ∈ a 1 0
14 3 5 13 cmpt class a ∈ 𝒫 o ⟼ x ∈ o ⟼ if x ∈ a 1 0
15 1 2 14 cmpt class o ∈ V ⟼ a ∈ 𝒫 o ⟼ x ∈ o ⟼ if x ∈ a 1 0
16 0 15 wceq wff 𝟙 = o ∈ V ⟼ a ∈ 𝒫 o ⟼ x ∈ o ⟼ if x ∈ a 1 0