Metamath Proof Explorer

Theorem indval

Description: Value of the indicator function generator for a set A and a domain O , i.e., an indicator function for a given domain O and a given subset A of the domain. (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