Metamath Proof Explorer


Theorem indv

Description: Value of the indicator function generator with domain O . (Contributed by Thierry Arnoux, 23-Aug-2017)

Ref Expression
Assertion indv O V 𝟙 O = a 𝒫 O x O if x a 1 0

Proof

Step Hyp Ref Expression
1 df-ind 𝟙 = o V a 𝒫 o x o if x a 1 0
2 pweq o = O 𝒫 o = 𝒫 O
3 mpteq1 o = O x o if x a 1 0 = x O if x a 1 0
4 2 3 mpteq12dv o = O a 𝒫 o x o if x a 1 0 = a 𝒫 O x O if x a 1 0
5 elex O V O V
6 pwexg O V 𝒫 O V
7 mptexg 𝒫 O V a 𝒫 O x O if x a 1 0 V
8 5 6 7 3syl O V a 𝒫 O x O if x a 1 0 V
9 1 4 5 8 fvmptd3 O V 𝟙 O = a 𝒫 O x O if x a 1 0