Theorem indval0

Description: The indicator function generator does not generate a (meaningful) indicator function for a class which is not a subset of the domain. (Contributed by AV, 11-Apr-2026)

	Ref	Expression
Assertion	indval0	⊢ ( ¬ 𝐴 ⊆ 𝑂 → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		indv	⊢ ( 𝑂 ∈ V → ( 𝟭 ‘ 𝑂 ) = ( 𝑎 ∈ 𝒫 𝑂 ↦ ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) ) )
2	1	fveq1d	⊢ ( 𝑂 ∈ V → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) = ( ( 𝑎 ∈ 𝒫 𝑂 ↦ ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) ) ‘ 𝐴 ) )
3	2	adantr	⊢ ( ( 𝑂 ∈ V ∧ ¬ 𝐴 ⊆ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) = ( ( 𝑎 ∈ 𝒫 𝑂 ↦ ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) ) ‘ 𝐴 ) )
4		elpwi	⊢ ( 𝐴 ∈ 𝒫 𝑂 → 𝐴 ⊆ 𝑂 )
5	4	con3i	⊢ ( ¬ 𝐴 ⊆ 𝑂 → ¬ 𝐴 ∈ 𝒫 𝑂 )
6	5	adantl	⊢ ( ( 𝑂 ∈ V ∧ ¬ 𝐴 ⊆ 𝑂 ) → ¬ 𝐴 ∈ 𝒫 𝑂 )
7		eqid	⊢ ( 𝑎 ∈ 𝒫 𝑂 ↦ ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) ) = ( 𝑎 ∈ 𝒫 𝑂 ↦ ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) )
8	7	fvmptndm	⊢ ( ¬ 𝐴 ∈ 𝒫 𝑂 → ( ( 𝑎 ∈ 𝒫 𝑂 ↦ ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) ) ‘ 𝐴 ) = ∅ )
9	6 8	syl	⊢ ( ( 𝑂 ∈ V ∧ ¬ 𝐴 ⊆ 𝑂 ) → ( ( 𝑎 ∈ 𝒫 𝑂 ↦ ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) ) ‘ 𝐴 ) = ∅ )
10	3 9	eqtrd	⊢ ( ( 𝑂 ∈ V ∧ ¬ 𝐴 ⊆ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) = ∅ )
11	10	ex	⊢ ( 𝑂 ∈ V → ( ¬ 𝐴 ⊆ 𝑂 → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) = ∅ ) )
12		fv2prc	⊢ ( ¬ 𝑂 ∈ V → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) = ∅ )
13	12	a1d	⊢ ( ¬ 𝑂 ∈ V → ( ¬ 𝐴 ⊆ 𝑂 → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) = ∅ ) )
14	11 13	pm2.61i	⊢ ( ¬ 𝐴 ⊆ 𝑂 → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) = ∅ )