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 } ) = 𝐴 )