Metamath Proof Explorer

Theorem indconst1

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

Ref Expression
Assertion indconst1 
|- ( O e. V -> ( ( _Ind ` O ) ` O ) = ( O X. { 1 } ) )

Proof

Step Hyp Ref Expression
1 ssid 
 |-  O C_ O
2 indval2 
 |-  ( ( O e. V /\ O C_ O ) -> ( ( _Ind ` O ) ` O ) = ( ( O X. { 1 } ) u. ( ( O \ O ) X. { 0 } ) ) )
3 1 2 mpan2 
 |-  ( O e. V -> ( ( _Ind ` O ) ` O ) = ( ( O X. { 1 } ) u. ( ( O \ O ) X. { 0 } ) ) )
4 difid 
 |-  ( O \ O ) = (/)
5 4 xpeq1i 
 |-  ( ( O \ O ) X. { 0 } ) = ( (/) X. { 0 } )
6 0xp 
 |-  ( (/) X. { 0 } ) = (/)
7 5 6 eqtri 
 |-  ( ( O \ O ) X. { 0 } ) = (/)
8 7 a1i 
 |-  ( O e. V -> ( ( O \ O ) X. { 0 } ) = (/) )
9 8 uneq2d 
 |-  ( O e. V -> ( ( O X. { 1 } ) u. ( ( O \ O ) X. { 0 } ) ) = ( ( O X. { 1 } ) u. (/) ) )
10 un0 
 |-  ( ( O X. { 1 } ) u. (/) ) = ( O X. { 1 } )
11 10 a1i 
 |-  ( O e. V -> ( ( O X. { 1 } ) u. (/) ) = ( O X. { 1 } ) )
12 3 9 11 3eqtrd 
 |-  ( O e. V -> ( ( _Ind ` O ) ` O ) = ( O X. { 1 } ) )