Theorem predisj

Description: Preimages of disjoint sets are disjoint. (Contributed by Zhi Wang, 9-Sep-2024)

	Ref	Expression
Hypotheses	predisj.1	$$⊢\phi \to \mathrm{Fun}F$$
	predisj.2	$$⊢\phi \to A\cap B=\varnothing$$
	predisj.3	$$⊢\phi \to S\subseteq F^{-1}\left[A\right]$$
	predisj.4	$$⊢\phi \to T\subseteq F^{-1}\left[B\right]$$
Assertion	predisj	$$⊢\phi \to S\cap T=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		predisj.1	$$⊢\phi \to \mathrm{Fun}F$$
2		predisj.2	$$⊢\phi \to A\cap B=\varnothing$$
3		predisj.3	$$⊢\phi \to S\subseteq F^{-1}\left[A\right]$$
4		predisj.4	$$⊢\phi \to T\subseteq F^{-1}\left[B\right]$$
5		inpreima	$$⊢\mathrm{Fun}F\to F^{-1}\left[A\cap B\right]=F^{-1}\left[A\right]\cap F^{-1}\left[B\right]$$
6	1 5	syl	$$⊢\phi \to F^{-1}\left[A\cap B\right]=F^{-1}\left[A\right]\cap F^{-1}\left[B\right]$$
7	2	imaeq2d	$$⊢\phi \to F^{-1}\left[A\cap B\right]=F^{-1}\left[\varnothing \right]$$
8		ima0	$$⊢F^{-1}\left[\varnothing \right]=\varnothing$$
9	7 8	eqtrdi	$$⊢\phi \to F^{-1}\left[A\cap B\right]=\varnothing$$
10	6 9	eqtr3d	$$⊢\phi \to F^{-1}\left[A\right]\cap F^{-1}\left[B\right]=\varnothing$$
11	3 10	ssdisjd	$$⊢\phi \to S\cap F^{-1}\left[B\right]=\varnothing$$
12	4 11	ssdisjdr	$$⊢\phi \to S\cap T=\varnothing$$