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

Metamath Proof Explorer

Theorem disjrnmpt

Description: Rewriting a disjoint collection using the range of a mapping. (Contributed by Thierry Arnoux, 27-May-2020)

Ref Expression
Assertion disjrnmpt 
|- ( Disj_ x e. A B -> Disj_ y e. ran ( x e. A |-> B ) y )

Proof

Step Hyp Ref Expression
1 disjabrex 
 |-  ( Disj_ x e. A B -> Disj_ y e. { z | E. x e. A z = B } y )
2 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
3 2 rnmpt 
 |-  ran ( x e. A |-> B ) = { z | E. x e. A z = B }
4 disjeq1 
 |-  ( ran ( x e. A |-> B ) = { z | E. x e. A z = B } -> ( Disj_ y e. ran ( x e. A |-> B ) y <-> Disj_ y e. { z | E. x e. A z = B } y ) )
5 3 4 ax-mp 
 |-  ( Disj_ y e. ran ( x e. A |-> B ) y <-> Disj_ y e. { z | E. x e. A z = B } y )
6 1 5 sylibr 
 |-  ( Disj_ x e. A B -> Disj_ y e. ran ( x e. A |-> B ) y )