Metamath Proof Explorer

Theorem indpreima

Description: A function with range { 0 , 1 } as an indicator of the preimage of { 1 } . (Contributed by Thierry Arnoux, 23-Aug-2017)

Ref Expression
Assertion indpreima 
|- ( ( O e. V /\ F : O --> { 0 , 1 } ) -> F = ( ( _Ind ` O ) ` ( `' F " { 1 } ) ) )

Proof

Step Hyp Ref Expression
1 ffn 
 |-  ( F : O --> { 0 , 1 } -> F Fn O )
2 1 adantl 
 |-  ( ( O e. V /\ F : O --> { 0 , 1 } ) -> F Fn O )
3 cnvimass 
 |-  ( `' F " { 1 } ) C_ dom F
4 fdm 
 |-  ( F : O --> { 0 , 1 } -> dom F = O )
5 4 adantl 
 |-  ( ( O e. V /\ F : O --> { 0 , 1 } ) -> dom F = O )
6 3 5 sseqtrid 
 |-  ( ( O e. V /\ F : O --> { 0 , 1 } ) -> ( `' F " { 1 } ) C_ O )
7 indf 
 |-  ( ( O e. V /\ ( `' F " { 1 } ) C_ O ) -> ( ( _Ind ` O ) ` ( `' F " { 1 } ) ) : O --> { 0 , 1 } )
8 6 7 syldan 
 |-  ( ( O e. V /\ F : O --> { 0 , 1 } ) -> ( ( _Ind ` O ) ` ( `' F " { 1 } ) ) : O --> { 0 , 1 } )
9 8 ffnd 
 |-  ( ( O e. V /\ F : O --> { 0 , 1 } ) -> ( ( _Ind ` O ) ` ( `' F " { 1 } ) ) Fn O )
10 simpr 
 |-  ( ( O e. V /\ F : O --> { 0 , 1 } ) -> F : O --> { 0 , 1 } )
11 10 ffvelrnda 
 |-  ( ( ( O e. V /\ F : O --> { 0 , 1 } ) /\ x e. O ) -> ( F ` x ) e. { 0 , 1 } )
12 prcom 
 |-  { 0 , 1 } = { 1 , 0 }
13 11 12 eleqtrdi 
 |-  ( ( ( O e. V /\ F : O --> { 0 , 1 } ) /\ x e. O ) -> ( F ` x ) e. { 1 , 0 } )
14 8 ffvelrnda 
 |-  ( ( ( O e. V /\ F : O --> { 0 , 1 } ) /\ x e. O ) -> ( ( ( _Ind ` O ) ` ( `' F " { 1 } ) ) ` x ) e. { 0 , 1 } )
15 14 12 eleqtrdi 
 |-  ( ( ( O e. V /\ F : O --> { 0 , 1 } ) /\ x e. O ) -> ( ( ( _Ind ` O ) ` ( `' F " { 1 } ) ) ` x ) e. { 1 , 0 } )
16 simpll 
 |-  ( ( ( O e. V /\ F : O --> { 0 , 1 } ) /\ x e. O ) -> O e. V )
17 6 adantr 
 |-  ( ( ( O e. V /\ F : O --> { 0 , 1 } ) /\ x e. O ) -> ( `' F " { 1 } ) C_ O )
18 simpr 
 |-  ( ( ( O e. V /\ F : O --> { 0 , 1 } ) /\ x e. O ) -> x e. O )
19 ind1a 
 |-  ( ( O e. V /\ ( `' F " { 1 } ) C_ O /\ x e. O ) -> ( ( ( ( _Ind ` O ) ` ( `' F " { 1 } ) ) ` x ) = 1 <-> x e. ( `' F " { 1 } ) ) )
20 16 17 18 19 syl3anc 
 |-  ( ( ( O e. V /\ F : O --> { 0 , 1 } ) /\ x e. O ) -> ( ( ( ( _Ind ` O ) ` ( `' F " { 1 } ) ) ` x ) = 1 <-> x e. ( `' F " { 1 } ) ) )
21 fniniseg 
 |-  ( F Fn O -> ( x e. ( `' F " { 1 } ) <-> ( x e. O /\ ( F ` x ) = 1 ) ) )
22 2 21 syl 
 |-  ( ( O e. V /\ F : O --> { 0 , 1 } ) -> ( x e. ( `' F " { 1 } ) <-> ( x e. O /\ ( F ` x ) = 1 ) ) )
23 22 baibd 
 |-  ( ( ( O e. V /\ F : O --> { 0 , 1 } ) /\ x e. O ) -> ( x e. ( `' F " { 1 } ) <-> ( F ` x ) = 1 ) )
24 20 23 bitr2d 
 |-  ( ( ( O e. V /\ F : O --> { 0 , 1 } ) /\ x e. O ) -> ( ( F ` x ) = 1 <-> ( ( ( _Ind ` O ) ` ( `' F " { 1 } ) ) ` x ) = 1 ) )
25 13 15 24 elpreq 
 |-  ( ( ( O e. V /\ F : O --> { 0 , 1 } ) /\ x e. O ) -> ( F ` x ) = ( ( ( _Ind ` O ) ` ( `' F " { 1 } ) ) ` x ) )
26 2 9 25 eqfnfvd 
 |-  ( ( O e. V /\ F : O --> { 0 , 1 } ) -> F = ( ( _Ind ` O ) ` ( `' F " { 1 } ) ) )