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 ∈ V ∧ A ⊆ O → 𝟙 O ⁡ A -1 1 = A

Proof

Step Hyp Ref Expression
1 ind1a ⊢ O ∈ V ∧ A ⊆ O ∧ x ∈ O → 𝟙 O ⁡ A ⁡ x = 1 ↔ x ∈ A
2 1 3expia ⊢ O ∈ V ∧ A ⊆ O → x ∈ O → 𝟙 O ⁡ A ⁡ x = 1 ↔ x ∈ A
3 2 pm5.32d ⊢ O ∈ V ∧ A ⊆ O → x ∈ O ∧ 𝟙 O ⁡ A ⁡ x = 1 ↔ x ∈ O ∧ x ∈ A
4 indf ⊢ O ∈ V ∧ A ⊆ O → 𝟙 O ⁡ A : O ⟶ 0 1
5 ffn ⊢ 𝟙 O ⁡ A : O ⟶ 0 1 → 𝟙 O ⁡ A Fn O
6 fniniseg ⊢ 𝟙 O ⁡ A Fn O → x ∈ 𝟙 O ⁡ A -1 1 ↔ x ∈ O ∧ 𝟙 O ⁡ A ⁡ x = 1
7 4 5 6 3syl ⊢ O ∈ V ∧ A ⊆ O → x ∈ 𝟙 O ⁡ A -1 1 ↔ x ∈ O ∧ 𝟙 O ⁡ A ⁡ x = 1
8 ssel ⊢ A ⊆ O → x ∈ A → x ∈ O
9 8 pm4.71rd ⊢ A ⊆ O → x ∈ A ↔ x ∈ O ∧ x ∈ A
10 9 adantl ⊢ O ∈ V ∧ A ⊆ O → x ∈ A ↔ x ∈ O ∧ x ∈ A
11 3 7 10 3bitr4d ⊢ O ∈ V ∧ A ⊆ O → x ∈ 𝟙 O ⁡ A -1 1 ↔ x ∈ A
12 11 eqrdv ⊢ O ∈ V ∧ A ⊆ O → 𝟙 O ⁡ A -1 1 = A