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	|- ( A. x e. A A. y e. B C = x -> Disj_ x e. A B )

Proof

Step	Hyp	Ref	Expression
1		nfra2w	|- F/ y A. x e. A A. y e. B C = x
2		df-ral	|- ( A. x e. A A. y e. B C = x <-> A. x ( x e. A -> A. y e. B C = x ) )
3		rsp	|- ( A. y e. B C = x -> ( y e. B -> C = x ) )
4		eqcom	|- ( C = x <-> x = C )
5	3 4	syl6ib	|- ( A. y e. B C = x -> ( y e. B -> x = C ) )
6	5	imim2i	|- ( ( x e. A -> A. y e. B C = x ) -> ( x e. A -> ( y e. B -> x = C ) ) )
7	6	impd	|- ( ( x e. A -> A. y e. B C = x ) -> ( ( x e. A /\ y e. B ) -> x = C ) )
8	7	alimi	|- ( A. x ( x e. A -> A. y e. B C = x ) -> A. x ( ( x e. A /\ y e. B ) -> x = C ) )
9	2 8	sylbi	|- ( A. x e. A A. y e. B C = x -> A. x ( ( x e. A /\ y e. B ) -> x = C ) )
10		mo2icl	|- ( A. x ( ( x e. A /\ y e. B ) -> x = C ) -> E* x ( x e. A /\ y e. B ) )
11	9 10	syl	|- ( A. x e. A A. y e. B C = x -> E* x ( x e. A /\ y e. B ) )
12	1 11	alrimi	|- ( A. x e. A A. y e. B C = x -> A. y E* x ( x e. A /\ y e. B ) )
13		dfdisj2	|- ( Disj_ x e. A B <-> A. y E* x ( x e. A /\ y e. B ) )
14	12 13	sylibr	|- ( A. x e. A A. y e. B C = x -> Disj_ x e. A B )