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	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ◡ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) “ { 1 } ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ind1a	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑥 ∈ 𝑂 ) → ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) = 1 ↔ 𝑥 ∈ 𝐴 ) )
2	1	3expia	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( 𝑥 ∈ 𝑂 → ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) = 1 ↔ 𝑥 ∈ 𝐴 ) ) )
3	2	pm5.32d	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ( 𝑥 ∈ 𝑂 ∧ ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) = 1 ) ↔ ( 𝑥 ∈ 𝑂 ∧ 𝑥 ∈ 𝐴 ) ) )
4		indf	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) : 𝑂 ⟶ { 0 , 1 } )
5		ffn	⊢ ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) : 𝑂 ⟶ { 0 , 1 } → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) Fn 𝑂 )
6		fniniseg	⊢ ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) Fn 𝑂 → ( 𝑥 ∈ ( ◡ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) “ { 1 } ) ↔ ( 𝑥 ∈ 𝑂 ∧ ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) = 1 ) ) )
7	4 5 6	3syl	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( 𝑥 ∈ ( ◡ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) “ { 1 } ) ↔ ( 𝑥 ∈ 𝑂 ∧ ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) = 1 ) ) )
8		ssel	⊢ ( 𝐴 ⊆ 𝑂 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑂 ) )
9	8	pm4.71rd	⊢ ( 𝐴 ⊆ 𝑂 → ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝑂 ∧ 𝑥 ∈ 𝐴 ) ) )
10	9	adantl	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝑂 ∧ 𝑥 ∈ 𝐴 ) ) )
11	3 7 10	3bitr4d	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( 𝑥 ∈ ( ◡ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) “ { 1 } ) ↔ 𝑥 ∈ 𝐴 ) )
12	11	eqrdv	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ◡ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) “ { 1 } ) = 𝐴 )