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

Metamath Proof Explorer

Theorem indpi1

Description: Preimage of the singleton { 1 } by the indicator function. See i1f1lem . (Contributed by Thierry Arnoux, 21-Aug-2017)

Ref Expression
Assertion indpi1 ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ◡ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) “ { 1 } ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 ind1a ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑥 ∈ 𝑂 ) → ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) = 1 ↔ 𝑥 ∈ 𝐴 ) )
2 1 3expia ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( 𝑥 ∈ 𝑂 → ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) = 1 ↔ 𝑥 ∈ 𝐴 ) ) )
3 2 pm5.32d ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ( 𝑥 ∈ 𝑂 ∧ ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) = 1 ) ↔ ( 𝑥 ∈ 𝑂 ∧ 𝑥 ∈ 𝐴 ) ) )
4 indf ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) : 𝑂 ⟶ { 0 , 1 } )
5 ffn ⊢ ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) : 𝑂 ⟶ { 0 , 1 } → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) Fn 𝑂 )
6 fniniseg ⊢ ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) Fn 𝑂 → ( 𝑥 ∈ ( ◡ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) “ { 1 } ) ↔ ( 𝑥 ∈ 𝑂 ∧ ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) = 1 ) ) )
7 4 5 6 3syl ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( 𝑥 ∈ ( ◡ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) “ { 1 } ) ↔ ( 𝑥 ∈ 𝑂 ∧ ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) = 1 ) ) )
8 ssel ⊢ ( 𝐴 ⊆ 𝑂 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑂 ) )
9 8 pm4.71rd ⊢ ( 𝐴 ⊆ 𝑂 → ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝑂 ∧ 𝑥 ∈ 𝐴 ) ) )
10 9 adantl ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝑂 ∧ 𝑥 ∈ 𝐴 ) ) )
11 3 7 10 3bitr4d ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( 𝑥 ∈ ( ◡ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) “ { 1 } ) ↔ 𝑥 ∈ 𝐴 ) )
12 11 eqrdv ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ◡ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) “ { 1 } ) = 𝐴 )