Theorem indconst0

Description: Indicator of the empty set. (Contributed by Thierry Arnoux, 25-Jan-2026)

	Ref	Expression
Assertion	indconst0	⊢ ( 𝑂 ∈ 𝑉 → ( ( 𝟭 ‘ 𝑂 ) ‘ ∅ ) = ( 𝑂 × { 0 } ) )

Proof

Step	Hyp	Ref	Expression
1		0ss	⊢ ∅ ⊆ 𝑂
2		indval2	⊢ ( ( 𝑂 ∈ 𝑉 ∧ ∅ ⊆ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ ∅ ) = ( ( ∅ × { 1 } ) ∪ ( ( 𝑂 ∖ ∅ ) × { 0 } ) ) )
3	1 2	mpan2	⊢ ( 𝑂 ∈ 𝑉 → ( ( 𝟭 ‘ 𝑂 ) ‘ ∅ ) = ( ( ∅ × { 1 } ) ∪ ( ( 𝑂 ∖ ∅ ) × { 0 } ) ) )
4		0xp	⊢ ( ∅ × { 1 } ) = ∅
5		dif0	⊢ ( 𝑂 ∖ ∅ ) = 𝑂
6	5	xpeq1i	⊢ ( ( 𝑂 ∖ ∅ ) × { 0 } ) = ( 𝑂 × { 0 } )
7	4 6	uneq12i	⊢ ( ( ∅ × { 1 } ) ∪ ( ( 𝑂 ∖ ∅ ) × { 0 } ) ) = ( ∅ ∪ ( 𝑂 × { 0 } ) )
8	7	a1i	⊢ ( 𝑂 ∈ 𝑉 → ( ( ∅ × { 1 } ) ∪ ( ( 𝑂 ∖ ∅ ) × { 0 } ) ) = ( ∅ ∪ ( 𝑂 × { 0 } ) ) )
9		0un	⊢ ( ∅ ∪ ( 𝑂 × { 0 } ) ) = ( 𝑂 × { 0 } )
10	9	a1i	⊢ ( 𝑂 ∈ 𝑉 → ( ∅ ∪ ( 𝑂 × { 0 } ) ) = ( 𝑂 × { 0 } ) )
11	3 8 10	3eqtrd	⊢ ( 𝑂 ∈ 𝑉 → ( ( 𝟭 ‘ 𝑂 ) ‘ ∅ ) = ( 𝑂 × { 0 } ) )