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 
|- ( 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 imbitrdi 
 |-  ( 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 )