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