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

Metamath Proof Explorer

Theorem qsdisj2

Description: A quotient set is a disjoint set. (Contributed by Mario Carneiro, 10-Dec-2016)

Ref Expression
Assertion qsdisj2 
|- ( R Er X -> Disj_ x e. ( A /. R ) x )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( R Er X /\ ( x e. ( A /. R ) /\ y e. ( A /. R ) ) ) -> R Er X )
2 simprl 
 |-  ( ( R Er X /\ ( x e. ( A /. R ) /\ y e. ( A /. R ) ) ) -> x e. ( A /. R ) )
3 simprr 
 |-  ( ( R Er X /\ ( x e. ( A /. R ) /\ y e. ( A /. R ) ) ) -> y e. ( A /. R ) )
4 1 2 3 qsdisj 
 |-  ( ( R Er X /\ ( x e. ( A /. R ) /\ y e. ( A /. R ) ) ) -> ( x = y \/ ( x i^i y ) = (/) ) )
5 4 ralrimivva 
 |-  ( R Er X -> A. x e. ( A /. R ) A. y e. ( A /. R ) ( x = y \/ ( x i^i y ) = (/) ) )
6 id 
 |-  ( x = y -> x = y )
7 6 disjor 
 |-  ( Disj_ x e. ( A /. R ) x <-> A. x e. ( A /. R ) A. y e. ( A /. R ) ( x = y \/ ( x i^i y ) = (/) ) )
8 5 7 sylibr 
 |-  ( R Er X -> Disj_ x e. ( A /. R ) x )