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 ⊢ ¬ A ⊆ O → 𝟙 O ⁡ A = ∅

Proof

Step Hyp Ref Expression
1 indv ⊢ O ∈ V → 𝟙 O = a ∈ 𝒫 O ⟼ x ∈ O ⟼ if x ∈ a 1 0
2 1 fveq1d ⊢ O ∈ V → 𝟙 O ⁡ A = a ∈ 𝒫 O ⟼ x ∈ O ⟼ if x ∈ a 1 0 ⁡ A
3 2 adantr ⊢ O ∈ V ∧ ¬ A ⊆ O → 𝟙 O ⁡ A = a ∈ 𝒫 O ⟼ x ∈ O ⟼ if x ∈ a 1 0 ⁡ A
4 elpwi ⊢ A ∈ 𝒫 O → A ⊆ O
5 4 con3i ⊢ ¬ A ⊆ O → ¬ A ∈ 𝒫 O
6 5 adantl ⊢ O ∈ V ∧ ¬ A ⊆ O → ¬ A ∈ 𝒫 O
7 eqid ⊢ a ∈ 𝒫 O ⟼ x ∈ O ⟼ if x ∈ a 1 0 = a ∈ 𝒫 O ⟼ x ∈ O ⟼ if x ∈ a 1 0
8 7 fvmptndm ⊢ ¬ A ∈ 𝒫 O → a ∈ 𝒫 O ⟼ x ∈ O ⟼ if x ∈ a 1 0 ⁡ A = ∅
9 6 8 syl ⊢ O ∈ V ∧ ¬ A ⊆ O → a ∈ 𝒫 O ⟼ x ∈ O ⟼ if x ∈ a 1 0 ⁡ A = ∅
10 3 9 eqtrd ⊢ O ∈ V ∧ ¬ A ⊆ O → 𝟙 O ⁡ A = ∅
11 10 ex ⊢ O ∈ V → ¬ A ⊆ O → 𝟙 O ⁡ A = ∅
12 fv2prc ⊢ ¬ O ∈ V → 𝟙 O ⁡ A = ∅
13 12 a1d ⊢ ¬ O ∈ V → ¬ A ⊆ O → 𝟙 O ⁡ A = ∅
14 11 13 pm2.61i ⊢ ¬ A ⊆ O → 𝟙 O ⁡ A = ∅