coeq0i

Description: coeq0 but without explicitly introducing domain and range symbols. (Contributed by Stefan O'Rear, 16-Oct-2014)

		Ref	Expression
	Assertion	coeq0i	$⊢ (A : C ⟶ D \land B : E ⟶ F \land C \cap F = \emptyset) \to A \circ B = \emptyset$

Step	Hyp	Ref	Expression
1		frn	$⊢ B : E ⟶ F \to ran B \subseteq F$
2	1	3ad2ant2	$⊢ (A : C ⟶ D \land B : E ⟶ F \land C \cap F = \emptyset) \to ran B \subseteq F$
3		sslin	$⊢ ran B \subseteq F \to dom A \cap ran B \subseteq dom A \cap F$
4	2 3	syl	$⊢ (A : C ⟶ D \land B : E ⟶ F \land C \cap F = \emptyset) \to dom A \cap ran B \subseteq dom A \cap F$
5		fdm	$⊢ A : C ⟶ D \to dom A = C$
6	5	3ad2ant1	$⊢ (A : C ⟶ D \land B : E ⟶ F \land C \cap F = \emptyset) \to dom A = C$
7	6	ineq1d	$⊢ (A : C ⟶ D \land B : E ⟶ F \land C \cap F = \emptyset) \to dom A \cap F = C \cap F$
8		simp3	$⊢ (A : C ⟶ D \land B : E ⟶ F \land C \cap F = \emptyset) \to C \cap F = \emptyset$
9	7 8	eqtrd	$⊢ (A : C ⟶ D \land B : E ⟶ F \land C \cap F = \emptyset) \to dom A \cap F = \emptyset$
10	4 9	sseqtrd	$⊢ (A : C ⟶ D \land B : E ⟶ F \land C \cap F = \emptyset) \to dom A \cap ran B \subseteq \emptyset$
11		ss0	$⊢ dom A \cap ran B \subseteq \emptyset \to dom A \cap ran B = \emptyset$
12	10 11	syl	$⊢ (A : C ⟶ D \land B : E ⟶ F \land C \cap F = \emptyset) \to dom A \cap ran B = \emptyset$
13	12	coemptyd	$⊢ (A : C ⟶ D \land B : E ⟶ F \land C \cap F = \emptyset) \to A \circ B = \emptyset$

Metamath Proof Explorer