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

Metamath Proof Explorer

Theorem invdisj

Description: If there is a function C ( y ) such that C ( y ) = x for all y e. B ( x ) , then the sets B ( x ) for distinct x e. A are disjoint. (Contributed by Mario Carneiro, 10-Dec-2016)

		Ref	Expression
	Assertion	invdisj	$⊢ \forall x \in A \forall y \in B C = x \to \underset{x \in A}{Disj} B$

Proof

Step	Hyp	Ref	Expression
1		nfra2w	$⊢ Ⅎ y \forall x \in A \forall y \in B C = x$
2		df-ral	$⊢ \forall x \in A \forall y \in B C = x \leftrightarrow \forall x (x \in A \to \forall y \in B C = x)$
3		rsp	$⊢ \forall y \in B C = x \to (y \in B \to C = x)$
4		eqcom	$⊢ C = x \leftrightarrow x = C$
5	3 4	imbitrdi	$⊢ \forall y \in B C = x \to (y \in B \to x = C)$
6	5	imim2i	$⊢ (x \in A \to \forall y \in B C = x) \to (x \in A \to (y \in B \to x = C))$
7	6	impd	$⊢ (x \in A \to \forall y \in B C = x) \to ((x \in A \land y \in B) \to x = C)$
8	7	alimi	$⊢ \forall x (x \in A \to \forall y \in B C = x) \to \forall x ((x \in A \land y \in B) \to x = C)$
9	2 8	sylbi	$⊢ \forall x \in A \forall y \in B C = x \to \forall x ((x \in A \land y \in B) \to x = C)$
10		mo2icl	$⊢ \forall x ((x \in A \land y \in B) \to x = C) \to \exists^{*} x (x \in A \land y \in B)$
11	9 10	syl	$⊢ \forall x \in A \forall y \in B C = x \to \exists^{*} x (x \in A \land y \in B)$
12	1 11	alrimi	$⊢ \forall x \in A \forall y \in B C = x \to \forall y \exists^{*} x (x \in A \land y \in B)$
13		dfdisj2	$⊢ \underset{x \in A}{Disj} B \leftrightarrow \forall y \exists^{*} x (x \in A \land y \in B)$
14	12 13	sylibr	$⊢ \forall x \in A \forall y \in B C = x \to \underset{x \in A}{Disj} B$