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∈V∧F:O⟶01→F=𝟙O⁡F-11

Proof

Step Hyp Ref Expression
1 ffn ⊢F:O⟶01→FFnO
2 1 adantl ⊢O∈V∧F:O⟶01→FFnO
3 cnvimass ⊢F-11⊆dom⁡F
4 fdm ⊢F:O⟶01→dom⁡F=O
5 4 adantl ⊢O∈V∧F:O⟶01→dom⁡F=O
6 3 5 sseqtrid ⊢O∈V∧F:O⟶01→F-11⊆O
7 indf ⊢O∈V∧F-11⊆O→𝟙O⁡F-11:O⟶01
8 6 7 syldan ⊢O∈V∧F:O⟶01→𝟙O⁡F-11:O⟶01
9 8 ffnd ⊢O∈V∧F:O⟶01→𝟙O⁡F-11FnO
10 simpr ⊢O∈V∧F:O⟶01→F:O⟶01
11 10 ffvelcdmda ⊢O∈V∧F:O⟶01∧x∈O→F⁡x∈01
12 prcom ⊢01=10
13 11 12 eleqtrdi ⊢O∈V∧F:O⟶01∧x∈O→F⁡x∈10
14 8 ffvelcdmda ⊢O∈V∧F:O⟶01∧x∈O→𝟙O⁡F-11⁡x∈01
15 14 12 eleqtrdi ⊢O∈V∧F:O⟶01∧x∈O→𝟙O⁡F-11⁡x∈10
16 simpll ⊢O∈V∧F:O⟶01∧x∈O→O∈V
17 6 adantr ⊢O∈V∧F:O⟶01∧x∈O→F-11⊆O
18 simpr ⊢O∈V∧F:O⟶01∧x∈O→x∈O
19 ind1a ⊢O∈V∧F-11⊆O∧x∈O→𝟙O⁡F-11⁡x=1↔x∈F-11
20 16 17 18 19 syl3anc ⊢O∈V∧F:O⟶01∧x∈O→𝟙O⁡F-11⁡x=1↔x∈F-11
21 fniniseg ⊢FFnO→x∈F-11↔x∈O∧F⁡x=1
22 2 21 syl ⊢O∈V∧F:O⟶01→x∈F-11↔x∈O∧F⁡x=1
23 22 baibd ⊢O∈V∧F:O⟶01∧x∈O→x∈F-11↔F⁡x=1
24 20 23 bitr2d ⊢O∈V∧F:O⟶01∧x∈O→F⁡x=1↔𝟙O⁡F-11⁡x=1
25 13 15 24 elpreq ⊢O∈V∧F:O⟶01∧x∈O→F⁡x=𝟙O⁡F-11⁡x
26 2 9 25 eqfnfvd ⊢O∈V∧F:O⟶01→F=𝟙O⁡F-11