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 e. V /\ A C_ O ) -> ( `' ( ( _Ind ` O ) ` A ) " { 1 } ) = A )

Proof

Step Hyp Ref Expression
1 ind1a 
 |-  ( ( O e. V /\ A C_ O /\ x e. O ) -> ( ( ( ( _Ind ` O ) ` A ) ` x ) = 1 <-> x e. A ) )
2 1 3expia 
 |-  ( ( O e. V /\ A C_ O ) -> ( x e. O -> ( ( ( ( _Ind ` O ) ` A ) ` x ) = 1 <-> x e. A ) ) )
3 2 pm5.32d 
 |-  ( ( O e. V /\ A C_ O ) -> ( ( x e. O /\ ( ( ( _Ind ` O ) ` A ) ` x ) = 1 ) <-> ( x e. O /\ x e. A ) ) )
4 indf 
 |-  ( ( O e. V /\ A C_ O ) -> ( ( _Ind ` O ) ` A ) : O --> { 0 , 1 } )
5 ffn 
 |-  ( ( ( _Ind ` O ) ` A ) : O --> { 0 , 1 } -> ( ( _Ind ` O ) ` A ) Fn O )
6 fniniseg 
 |-  ( ( ( _Ind ` O ) ` A ) Fn O -> ( x e. ( `' ( ( _Ind ` O ) ` A ) " { 1 } ) <-> ( x e. O /\ ( ( ( _Ind ` O ) ` A ) ` x ) = 1 ) ) )
7 4 5 6 3syl 
 |-  ( ( O e. V /\ A C_ O ) -> ( x e. ( `' ( ( _Ind ` O ) ` A ) " { 1 } ) <-> ( x e. O /\ ( ( ( _Ind ` O ) ` A ) ` x ) = 1 ) ) )
8 ssel 
 |-  ( A C_ O -> ( x e. A -> x e. O ) )
9 8 pm4.71rd 
 |-  ( A C_ O -> ( x e. A <-> ( x e. O /\ x e. A ) ) )
10 9 adantl 
 |-  ( ( O e. V /\ A C_ O ) -> ( x e. A <-> ( x e. O /\ x e. A ) ) )
11 3 7 10 3bitr4d 
 |-  ( ( O e. V /\ A C_ O ) -> ( x e. ( `' ( ( _Ind ` O ) ` A ) " { 1 } ) <-> x e. A ) )
12 11 eqrdv 
 |-  ( ( O e. V /\ A C_ O ) -> ( `' ( ( _Ind ` O ) ` A ) " { 1 } ) = A )