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 ⊢ ∅ ∘ A = ∅

Proof

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