Theorem predisj

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

	Ref	Expression
Hypotheses	predisj.1	⊢ ( 𝜑 → Fun 𝐹 )
	predisj.2	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
	predisj.3	⊢ ( 𝜑 → 𝑆 ⊆ ( ◡ 𝐹 “ 𝐴 ) )
	predisj.4	⊢ ( 𝜑 → 𝑇 ⊆ ( ◡ 𝐹 “ 𝐵 ) )
Assertion	predisj	⊢ ( 𝜑 → ( 𝑆 ∩ 𝑇 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		predisj.1	⊢ ( 𝜑 → Fun 𝐹 )
2		predisj.2	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
3		predisj.3	⊢ ( 𝜑 → 𝑆 ⊆ ( ◡ 𝐹 “ 𝐴 ) )
4		predisj.4	⊢ ( 𝜑 → 𝑇 ⊆ ( ◡ 𝐹 “ 𝐵 ) )
5		inpreima	⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ( 𝐴 ∩ 𝐵 ) ) = ( ( ◡ 𝐹 “ 𝐴 ) ∩ ( ◡ 𝐹 “ 𝐵 ) ) )
6	1 5	syl	⊢ ( 𝜑 → ( ◡ 𝐹 “ ( 𝐴 ∩ 𝐵 ) ) = ( ( ◡ 𝐹 “ 𝐴 ) ∩ ( ◡ 𝐹 “ 𝐵 ) ) )
7	2	imaeq2d	⊢ ( 𝜑 → ( ◡ 𝐹 “ ( 𝐴 ∩ 𝐵 ) ) = ( ◡ 𝐹 “ ∅ ) )
8		ima0	⊢ ( ◡ 𝐹 “ ∅ ) = ∅
9	7 8	eqtrdi	⊢ ( 𝜑 → ( ◡ 𝐹 “ ( 𝐴 ∩ 𝐵 ) ) = ∅ )
10	6 9	eqtr3d	⊢ ( 𝜑 → ( ( ◡ 𝐹 “ 𝐴 ) ∩ ( ◡ 𝐹 “ 𝐵 ) ) = ∅ )
11	3 10	ssdisjd	⊢ ( 𝜑 → ( 𝑆 ∩ ( ◡ 𝐹 “ 𝐵 ) ) = ∅ )
12	4 11	ssdisjdr	⊢ ( 𝜑 → ( 𝑆 ∩ 𝑇 ) = ∅ )