Theorem disjrnmpt

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

	Ref	Expression
Assertion	disjrnmpt	$$⊢\underset{x\in A}{Disj}B\to \underset{y\in \mathrm{ran}\left(x\in A⟼B\right)}{Disj}y$$

Proof

Step	Hyp	Ref	Expression
1		disjabrex	$$⊢\underset{x\in A}{Disj}B\to \underset{y\in \left\{z|\exists x\in Az=B\right\}}{Disj}y$$
2		eqid	$$⊢\left(x\in A⟼B\right)=\left(x\in A⟼B\right)$$
3	2	rnmpt	$$⊢\mathrm{ran}\left(x\in A⟼B\right)=\left\{z|\exists x\in Az=B\right\}$$
4		disjeq1	$$⊢\mathrm{ran}\left(x\in A⟼B\right)=\left\{z|\exists x\in Az=B\right\}\to \left(\underset{y\in \mathrm{ran}\left(x\in A⟼B\right)}{Disj}y\leftrightarrow \underset{y\in \left\{z|\exists x\in Az=B\right\}}{Disj}y\right)$$
5	3 4	ax-mp	$$⊢\underset{y\in \mathrm{ran}\left(x\in A⟼B\right)}{Disj}y\leftrightarrow \underset{y\in \left\{z|\exists x\in Az=B\right\}}{Disj}y$$
6	1 5	sylibr	$$⊢\underset{x\in A}{Disj}B\to \underset{y\in \mathrm{ran}\left(x\in A⟼B\right)}{Disj}y$$