Metamath Proof Explorer


Theorem co01

Description: Composition with the empty set. (Contributed by NM, 24-Apr-2004)

Ref Expression
Assertion co01
|- ( (/) o. A ) = (/)

Proof

Step Hyp Ref Expression
1 cnv0
 |-  `' (/) = (/)
2 cnvco
 |-  `' ( (/) o. A ) = ( `' A o. `' (/) )
3 1 coeq2i
 |-  ( `' A o. `' (/) ) = ( `' A o. (/) )
4 co02
 |-  ( `' A o. (/) ) = (/)
5 2 3 4 3eqtri
 |-  `' ( (/) o. A ) = (/)
6 1 5 eqtr4i
 |-  `' (/) = `' ( (/) o. A )
7 6 cnveqi
 |-  `' `' (/) = `' `' ( (/) o. A )
8 rel0
 |-  Rel (/)
9 dfrel2
 |-  ( Rel (/) <-> `' `' (/) = (/) )
10 8 9 mpbi
 |-  `' `' (/) = (/)
11 relco
 |-  Rel ( (/) o. A )
12 dfrel2
 |-  ( Rel ( (/) o. A ) <-> `' `' ( (/) o. A ) = ( (/) o. A ) )
13 11 12 mpbi
 |-  `' `' ( (/) o. A ) = ( (/) o. A )
14 7 10 13 3eqtr3ri
 |-  ( (/) o. A ) = (/)