Metamath Proof Explorer

Theorem indconst0

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

Ref Expression
Assertion indconst0 
|- ( O e. V -> ( ( _Ind ` O ) ` (/) ) = ( O X. { 0 } ) )

Proof

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