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	⊢ ( ∅ ∘ 𝐴 ) = ∅