disjlem14

		Ref	Expression
	Assertion	disjlem14	$⊢ Disj R \to ((x \in dom R \land y \in dom R) \to ((A \in [x] R \land A \in [y] R) \to [x] R = [y] R))$

Step	Hyp	Ref	Expression
1		dfdisjALTV5	$⊢ Disj R \leftrightarrow (\forall x \in dom R \forall y \in dom R (x = y \lor [x] R \cap [y] R = \emptyset) \land Rel R)$
2	1	simplbi	$⊢ Disj R \to \forall x \in dom R \forall y \in dom R (x = y \lor [x] R \cap [y] R = \emptyset)$
3		rsp2	$⊢ \forall x \in dom R \forall y \in dom R (x = y \lor [x] R \cap [y] R = \emptyset) \to ((x \in dom R \land y \in dom R) \to (x = y \lor [x] R \cap [y] R = \emptyset))$
4	2 3	syl	$⊢ Disj R \to ((x \in dom R \land y \in dom R) \to (x = y \lor [x] R \cap [y] R = \emptyset))$
5		eceq1	$⊢ x = y \to [x] R = [y] R$
6	5	a1d	$⊢ x = y \to ((A \in [x] R \land A \in [y] R) \to [x] R = [y] R)$
7		elin	$⊢ A \in ([x] R \cap [y] R) \leftrightarrow (A \in [x] R \land A \in [y] R)$
8		nel02	$⊢ [x] R \cap [y] R = \emptyset \to \neg A \in ([x] R \cap [y] R)$
9	8	pm2.21d	$⊢ [x] R \cap [y] R = \emptyset \to (A \in ([x] R \cap [y] R) \to [x] R = [y] R)$
10	7 9	biimtrrid	$⊢ [x] R \cap [y] R = \emptyset \to ((A \in [x] R \land A \in [y] R) \to [x] R = [y] R)$
11	6 10	jaoi	$⊢ (x = y \lor [x] R \cap [y] R = \emptyset) \to ((A \in [x] R \land A \in [y] R) \to [x] R = [y] R)$
12	4 11	syl6	$⊢ Disj R \to ((x \in dom R \land y \in dom R) \to ((A \in [x] R \land A \in [y] R) \to [x] R = [y] R))$

Metamath Proof Explorer