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

Metamath Proof Explorer

Theorem indconst1

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

Ref Expression
Assertion indconst1 ( 𝑂 ∈ 𝑉 → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝑂 ) = ( 𝑂 × { 1 } ) )

Proof

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