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

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 ) = (/)