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 ⟶ 0 1 → F = 𝟙 O ⁡ F -1 1

Proof

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