Metamath Proof Explorer


Theorem predisj

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

Ref Expression
Hypotheses predisj.1 φFunF
predisj.2 φAB=
predisj.3 φSF-1A
predisj.4 φTF-1B
Assertion predisj φST=

Proof

Step Hyp Ref Expression
1 predisj.1 φFunF
2 predisj.2 φAB=
3 predisj.3 φSF-1A
4 predisj.4 φTF-1B
5 inpreima FunFF-1AB=F-1AF-1B
6 1 5 syl φF-1AB=F-1AF-1B
7 2 imaeq2d φF-1AB=F-1
8 ima0 F-1=
9 7 8 eqtrdi φF-1AB=
10 6 9 eqtr3d φF-1AF-1B=
11 3 10 ssdisjd φSF-1B=
12 4 11 ssdisjdr φST=