Metamath Proof Explorer


Theorem indval

Description: Value of the indicator function generator for a set A and a domain O . (Contributed by Thierry Arnoux, 2-Feb-2017)

Ref Expression
Assertion indval O V A O 𝟙 O A = x O if x A 1 0

Proof

Step Hyp Ref Expression
1 indv O V 𝟙 O = a 𝒫 O x O if x a 1 0
2 1 adantr O V A O 𝟙 O = a 𝒫 O x O if x a 1 0
3 eleq2 a = A x a x A
4 3 ifbid a = A if x a 1 0 = if x A 1 0
5 4 mpteq2dv a = A x O if x a 1 0 = x O if x A 1 0
6 5 adantl O V A O a = A x O if x a 1 0 = x O if x A 1 0
7 ssexg A O O V A V
8 7 ancoms O V A O A V
9 simpr O V A O A O
10 8 9 elpwd O V A O A 𝒫 O
11 mptexg O V x O if x A 1 0 V
12 11 adantr O V A O x O if x A 1 0 V
13 2 6 10 12 fvmptd O V A O 𝟙 O A = x O if x A 1 0