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 )