Metamath Proof Explorer

Theorem disjif

Description: Property of a disjoint collection: if B ( x ) and B ( Y ) = D have a common element Z , then x = Y . (Contributed by Thierry Arnoux, 30-Dec-2016)

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

Proof

Step	Hyp	Ref	Expression
1		disjif.1	$⊢ \underline{Ⅎ} x C$
2		disjif.2	$⊢ x = Y \to B = C$
3		inelcm	$⊢ (Z \in B \land Z \in C) \to B \cap C \neq \emptyset$
4	1 2	disji2f	$⊢ (\underset{x \in A}{Disj} B \land (x \in A \land Y \in A) \land x \neq Y) \to B \cap C = \emptyset$
5	4	3expia	$⊢ (\underset{x \in A}{Disj} B \land (x \in A \land Y \in A)) \to (x \neq Y \to B \cap C = \emptyset)$
6	5	necon1d	$⊢ (\underset{x \in A}{Disj} B \land (x \in A \land Y \in A)) \to (B \cap C \neq \emptyset \to x = Y)$
7	6	3impia	$⊢ (\underset{x \in A}{Disj} B \land (x \in A \land Y \in A) \land B \cap C \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 B \land Z \in C)) \to x = Y$