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 O V A O 𝟙 O A -1 1 = A

Proof

Step Hyp Ref Expression
1 ind1a O V A O x O 𝟙 O A x = 1 x A
2 1 3expia O V A O x O 𝟙 O A x = 1 x A
3 2 pm5.32d O V A O x O 𝟙 O A x = 1 x O x A
4 indf O V A O 𝟙 O A : O 0 1
5 ffn 𝟙 O A : O 0 1 𝟙 O A Fn O
6 fniniseg 𝟙 O A Fn O x 𝟙 O A -1 1 x O 𝟙 O A x = 1
7 4 5 6 3syl O V A O x 𝟙 O A -1 1 x O 𝟙 O A x = 1
8 ssel A O x A x O
9 8 pm4.71rd A O x A x O x A
10 9 adantl O V A O x A x O x A
11 3 7 10 3bitr4d O V A O x 𝟙 O A -1 1 x A
12 11 eqrdv O V A O 𝟙 O A -1 1 = A