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

Metamath Proof Explorer

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 } ) )