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

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 ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) = ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) )

Proof

Step Hyp Ref Expression
1 indv ⊢ ( 𝑂 ∈ 𝑉 → ( 𝟭 ‘ 𝑂 ) = ( 𝑎 ∈ 𝒫 𝑂 ↦ ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) ) )
2 1 adantr ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( 𝟭 ‘ 𝑂 ) = ( 𝑎 ∈ 𝒫 𝑂 ↦ ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) ) )
3 eleq2 ⊢ ( 𝑎 = 𝐴 → ( 𝑥 ∈ 𝑎 ↔ 𝑥 ∈ 𝐴 ) )
4 3 ifbid ⊢ ( 𝑎 = 𝐴 → if ( 𝑥 ∈ 𝑎 , 1 , 0 ) = if ( 𝑥 ∈ 𝐴 , 1 , 0 ) )
5 4 mpteq2dv ⊢ ( 𝑎 = 𝐴 → ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) = ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) )
6 5 adantl ⊢ ( ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) ∧ 𝑎 = 𝐴 ) → ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) = ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) )
7 ssexg ⊢ ( ( 𝐴 ⊆ 𝑂 ∧ 𝑂 ∈ 𝑉 ) → 𝐴 ∈ V )
8 7 ancoms ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → 𝐴 ∈ V )
9 simpr ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → 𝐴 ⊆ 𝑂 )
10 8 9 elpwd ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → 𝐴 ∈ 𝒫 𝑂 )
11 mptexg ⊢ ( 𝑂 ∈ 𝑉 → ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ∈ V )
12 11 adantr ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ∈ V )
13 2 6 10 12 fvmptd ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) = ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) )