This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ¬ 𝐴 ⊆ 𝑂 → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) = ∅ )