Theorem predisj

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

	Ref	Expression
Hypotheses	predisj.1	|- ( ph -> Fun F )
	predisj.2	|- ( ph -> ( A i^i B ) = (/) )
	predisj.3	|- ( ph -> S C_ ( `' F " A ) )
	predisj.4	|- ( ph -> T C_ ( `' F " B ) )
Assertion	predisj	|- ( ph -> ( S i^i T ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		predisj.1	|- ( ph -> Fun F )
2		predisj.2	|- ( ph -> ( A i^i B ) = (/) )
3		predisj.3	|- ( ph -> S C_ ( `' F " A ) )
4		predisj.4	|- ( ph -> T C_ ( `' F " B ) )
5		inpreima	|- ( Fun F -> ( `' F " ( A i^i B ) ) = ( ( `' F " A ) i^i ( `' F " B ) ) )
6	1 5	syl	|- ( ph -> ( `' F " ( A i^i B ) ) = ( ( `' F " A ) i^i ( `' F " B ) ) )
7	2	imaeq2d	|- ( ph -> ( `' F " ( A i^i B ) ) = ( `' F " (/) ) )
8		ima0	|- ( `' F " (/) ) = (/)
9	7 8	eqtrdi	|- ( ph -> ( `' F " ( A i^i B ) ) = (/) )
10	6 9	eqtr3d	|- ( ph -> ( ( `' F " A ) i^i ( `' F " B ) ) = (/) )
11	3 10	ssdisjd	|- ( ph -> ( S i^i ( `' F " B ) ) = (/) )
12	4 11	ssdisjdr	|- ( ph -> ( S i^i T ) = (/) )