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 ran (x \in A ⟼ B)}{Disj} y$

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

Metamath Proof Explorer