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

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