Metamath Proof Explorer

Theorem indfval

Description: Value of the indicator function. (Contributed by Thierry Arnoux, 13-Aug-2017)

Ref Expression
Assertion indfval ⊢ O ∈ V ∧ A ⊆ O ∧ X ∈ O → 𝟙 O ⁡ A ⁡ X = if X ∈ A 1 0

Proof

Step Hyp Ref Expression
1 indval ⊢ O ∈ V ∧ A ⊆ O → 𝟙 O ⁡ A = x ∈ O ⟼ if x ∈ A 1 0
2 1 3adant3 ⊢ O ∈ V ∧ A ⊆ O ∧ X ∈ O → 𝟙 O ⁡ A = x ∈ O ⟼ if x ∈ A 1 0
3 simpr ⊢ O ∈ V ∧ A ⊆ O ∧ X ∈ O ∧ x = X → x = X
4 3 eleq1d ⊢ O ∈ V ∧ A ⊆ O ∧ X ∈ O ∧ x = X → x ∈ A ↔ X ∈ A
5 4 ifbid ⊢ O ∈ V ∧ A ⊆ O ∧ X ∈ O ∧ x = X → if x ∈ A 1 0 = if X ∈ A 1 0
6 simp3 ⊢ O ∈ V ∧ A ⊆ O ∧ X ∈ O → X ∈ O
7 1re ⊢ 1 ∈ ℝ
8 0re ⊢ 0 ∈ ℝ
9 7 8 ifcli ⊢ if X ∈ A 1 0 ∈ ℝ
10 9 a1i ⊢ O ∈ V ∧ A ⊆ O ∧ X ∈ O → if X ∈ A 1 0 ∈ ℝ
11 2 5 6 10 fvmptd ⊢ O ∈ V ∧ A ⊆ O ∧ X ∈ O → 𝟙 O ⁡ A ⁡ X = if X ∈ A 1 0