Metamath Proof Explorer


Theorem co01

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

Ref Expression
Assertion co01 ( ∅ ∘ 𝐴 ) = ∅

Proof

Step Hyp Ref Expression
1 cnv0 ∅ = ∅
2 cnvco ( ∅ ∘ 𝐴 ) = ( 𝐴 ∅ )
3 1 coeq2i ( 𝐴 ∅ ) = ( 𝐴 ∘ ∅ )
4 co02 ( 𝐴 ∘ ∅ ) = ∅
5 2 3 4 3eqtri ( ∅ ∘ 𝐴 ) = ∅
6 1 5 eqtr4i ∅ = ( ∅ ∘ 𝐴 )
7 6 cnveqi ∅ = ( ∅ ∘ 𝐴 )
8 rel0 Rel ∅
9 dfrel2 ( Rel ∅ ↔ ∅ = ∅ )
10 8 9 mpbi ∅ = ∅
11 relco Rel ( ∅ ∘ 𝐴 )
12 dfrel2 ( Rel ( ∅ ∘ 𝐴 ) ↔ ( ∅ ∘ 𝐴 ) = ( ∅ ∘ 𝐴 ) )
13 11 12 mpbi ( ∅ ∘ 𝐴 ) = ( ∅ ∘ 𝐴 )
14 7 10 13 3eqtr3ri ( ∅ ∘ 𝐴 ) = ∅