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 ( ( 𝑂 ∈ 𝑉 ∧ 𝐹 : 𝑂 ⟶ { 0 , 1 } ) → 𝐹 = ( ( 𝟭 ‘ 𝑂 ) ‘ ( ◡ 𝐹 “ { 1 } ) ) )

Proof

Step Hyp Ref Expression
1 ffn ⊢ ( 𝐹 : 𝑂 ⟶ { 0 , 1 } → 𝐹 Fn 𝑂 )
2 1 adantl ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐹 : 𝑂 ⟶ { 0 , 1 } ) → 𝐹 Fn 𝑂 )
3 cnvimass ⊢ ( ◡ 𝐹 “ { 1 } ) ⊆ dom 𝐹
4 fdm ⊢ ( 𝐹 : 𝑂 ⟶ { 0 , 1 } → dom 𝐹 = 𝑂 )
5 4 adantl ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐹 : 𝑂 ⟶ { 0 , 1 } ) → dom 𝐹 = 𝑂 )
6 3 5 sseqtrid ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐹 : 𝑂 ⟶ { 0 , 1 } ) → ( ◡ 𝐹 “ { 1 } ) ⊆ 𝑂 )
7 indf ⊢ ( ( 𝑂 ∈ 𝑉 ∧ ( ◡ 𝐹 “ { 1 } ) ⊆ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ ( ◡ 𝐹 “ { 1 } ) ) : 𝑂 ⟶ { 0 , 1 } )
8 6 7 syldan ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐹 : 𝑂 ⟶ { 0 , 1 } ) → ( ( 𝟭 ‘ 𝑂 ) ‘ ( ◡ 𝐹 “ { 1 } ) ) : 𝑂 ⟶ { 0 , 1 } )
9 8 ffnd ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐹 : 𝑂 ⟶ { 0 , 1 } ) → ( ( 𝟭 ‘ 𝑂 ) ‘ ( ◡ 𝐹 “ { 1 } ) ) Fn 𝑂 )
10 simpr ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐹 : 𝑂 ⟶ { 0 , 1 } ) → 𝐹 : 𝑂 ⟶ { 0 , 1 } )
11 10 ffvelcdmda ⊢ ( ( ( 𝑂 ∈ 𝑉 ∧ 𝐹 : 𝑂 ⟶ { 0 , 1 } ) ∧ 𝑥 ∈ 𝑂 ) → ( 𝐹 ‘ 𝑥 ) ∈ { 0 , 1 } )
12 prcom ⊢ { 0 , 1 } = { 1 , 0 }
13 11 12 eleqtrdi ⊢ ( ( ( 𝑂 ∈ 𝑉 ∧ 𝐹 : 𝑂 ⟶ { 0 , 1 } ) ∧ 𝑥 ∈ 𝑂 ) → ( 𝐹 ‘ 𝑥 ) ∈ { 1 , 0 } )
14 8 ffvelcdmda ⊢ ( ( ( 𝑂 ∈ 𝑉 ∧ 𝐹 : 𝑂 ⟶ { 0 , 1 } ) ∧ 𝑥 ∈ 𝑂 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ ( ◡ 𝐹 “ { 1 } ) ) ‘ 𝑥 ) ∈ { 0 , 1 } )
15 14 12 eleqtrdi ⊢ ( ( ( 𝑂 ∈ 𝑉 ∧ 𝐹 : 𝑂 ⟶ { 0 , 1 } ) ∧ 𝑥 ∈ 𝑂 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ ( ◡ 𝐹 “ { 1 } ) ) ‘ 𝑥 ) ∈ { 1 , 0 } )
16 simpll ⊢ ( ( ( 𝑂 ∈ 𝑉 ∧ 𝐹 : 𝑂 ⟶ { 0 , 1 } ) ∧ 𝑥 ∈ 𝑂 ) → 𝑂 ∈ 𝑉 )
17 6 adantr ⊢ ( ( ( 𝑂 ∈ 𝑉 ∧ 𝐹 : 𝑂 ⟶ { 0 , 1 } ) ∧ 𝑥 ∈ 𝑂 ) → ( ◡ 𝐹 “ { 1 } ) ⊆ 𝑂 )
18 simpr ⊢ ( ( ( 𝑂 ∈ 𝑉 ∧ 𝐹 : 𝑂 ⟶ { 0 , 1 } ) ∧ 𝑥 ∈ 𝑂 ) → 𝑥 ∈ 𝑂 )
19 ind1a ⊢ ( ( 𝑂 ∈ 𝑉 ∧ ( ◡ 𝐹 “ { 1 } ) ⊆ 𝑂 ∧ 𝑥 ∈ 𝑂 ) → ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ ( ◡ 𝐹 “ { 1 } ) ) ‘ 𝑥 ) = 1 ↔ 𝑥 ∈ ( ◡ 𝐹 “ { 1 } ) ) )
20 16 17 18 19 syl3anc ⊢ ( ( ( 𝑂 ∈ 𝑉 ∧ 𝐹 : 𝑂 ⟶ { 0 , 1 } ) ∧ 𝑥 ∈ 𝑂 ) → ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ ( ◡ 𝐹 “ { 1 } ) ) ‘ 𝑥 ) = 1 ↔ 𝑥 ∈ ( ◡ 𝐹 “ { 1 } ) ) )
21 fniniseg ⊢ ( 𝐹 Fn 𝑂 → ( 𝑥 ∈ ( ◡ 𝐹 “ { 1 } ) ↔ ( 𝑥 ∈ 𝑂 ∧ ( 𝐹 ‘ 𝑥 ) = 1 ) ) )
22 2 21 syl ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐹 : 𝑂 ⟶ { 0 , 1 } ) → ( 𝑥 ∈ ( ◡ 𝐹 “ { 1 } ) ↔ ( 𝑥 ∈ 𝑂 ∧ ( 𝐹 ‘ 𝑥 ) = 1 ) ) )
23 22 baibd ⊢ ( ( ( 𝑂 ∈ 𝑉 ∧ 𝐹 : 𝑂 ⟶ { 0 , 1 } ) ∧ 𝑥 ∈ 𝑂 ) → ( 𝑥 ∈ ( ◡ 𝐹 “ { 1 } ) ↔ ( 𝐹 ‘ 𝑥 ) = 1 ) )
24 20 23 bitr2d ⊢ ( ( ( 𝑂 ∈ 𝑉 ∧ 𝐹 : 𝑂 ⟶ { 0 , 1 } ) ∧ 𝑥 ∈ 𝑂 ) → ( ( 𝐹 ‘ 𝑥 ) = 1 ↔ ( ( ( 𝟭 ‘ 𝑂 ) ‘ ( ◡ 𝐹 “ { 1 } ) ) ‘ 𝑥 ) = 1 ) )
25 13 15 24 elpreq ⊢ ( ( ( 𝑂 ∈ 𝑉 ∧ 𝐹 : 𝑂 ⟶ { 0 , 1 } ) ∧ 𝑥 ∈ 𝑂 ) → ( 𝐹 ‘ 𝑥 ) = ( ( ( 𝟭 ‘ 𝑂 ) ‘ ( ◡ 𝐹 “ { 1 } ) ) ‘ 𝑥 ) )
26 2 9 25 eqfnfvd ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐹 : 𝑂 ⟶ { 0 , 1 } ) → 𝐹 = ( ( 𝟭 ‘ 𝑂 ) ‘ ( ◡ 𝐹 “ { 1 } ) ) )