Theorem co02

Description: Composition with the empty set. Theorem 20 of Suppes p. 63. (Contributed by NM, 24-Apr-2004)

	Ref	Expression
Assertion	co02	⊢ ( 𝐴 ∘ ∅ ) = ∅

Proof

Step	Hyp	Ref	Expression
1		relco	⊢ Rel ( 𝐴 ∘ ∅ )
2		rel0	⊢ Rel ∅
3		br0	⊢ ¬ 𝑥 ∅ 𝑧
4	3	intnanr	⊢ ¬ ( 𝑥 ∅ 𝑧 ∧ 𝑧 𝐴 𝑦 )
5	4	nex	⊢ ¬ ∃ 𝑧 ( 𝑥 ∅ 𝑧 ∧ 𝑧 𝐴 𝑦 )
6		vex	⊢ 𝑥 ∈ V
7		vex	⊢ 𝑦 ∈ V
8	6 7	opelco	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 ∘ ∅ ) ↔ ∃ 𝑧 ( 𝑥 ∅ 𝑧 ∧ 𝑧 𝐴 𝑦 ) )
9	5 8	mtbir	⊢ ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 ∘ ∅ )
10		noel	⊢ ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ ∅
11	9 10	2false	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 ∘ ∅ ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ∅ )
12	1 2 11	eqrelriiv	⊢ ( 𝐴 ∘ ∅ ) = ∅