Description: Composition with the empty set. (Contributed by NM, 24-Apr-2004)
Ref | Expression | ||
---|---|---|---|
Assertion | co01 | ⊢ ( ∅ ∘ 𝐴 ) = ∅ |
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 | ⊢ ( ∅ ∘ 𝐴 ) = ∅ |