This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem disji

Description: Property of a disjoint collection: if B ( X ) = C and B ( Y ) = D have a common element Z , then X = Y . (Contributed by Mario Carneiro, 14-Nov-2016)

		Ref	Expression
	Hypotheses	disji.1	$⊢ x = X \to B = C$
		disji.2	$⊢ x = Y \to B = D$
	Assertion	disji	$⊢ (\underset{x \in A}{Disj} B \land (X \in A \land Y \in A) \land (Z \in C \land Z \in D)) \to X = Y$

Proof

Step	Hyp	Ref	Expression
1		disji.1	$⊢ x = X \to B = C$
2		disji.2	$⊢ x = Y \to B = D$
3		inelcm	$⊢ (Z \in C \land Z \in D) \to C \cap D \neq \emptyset$
4	1 2	disji2	$⊢ (\underset{x \in A}{Disj} B \land (X \in A \land Y \in A) \land X \neq Y) \to C \cap D = \emptyset$
5	4	3expia	$⊢ (\underset{x \in A}{Disj} B \land (X \in A \land Y \in A)) \to (X \neq Y \to C \cap D = \emptyset)$
6	5	necon1d	$⊢ (\underset{x \in A}{Disj} B \land (X \in A \land Y \in A)) \to (C \cap D \neq \emptyset \to X = Y)$
7	6	3impia	$⊢ (\underset{x \in A}{Disj} B \land (X \in A \land Y \in A) \land C \cap D \neq \emptyset) \to X = Y$
8	3 7	syl3an3	$⊢ (\underset{x \in A}{Disj} B \land (X \in A \land Y \in A) \land (Z \in C \land Z \in D)) \to X = Y$