Description: If a collection is disjoint, so is the collection of the intersections with a given set. (Contributed by Thierry Arnoux, 14-Feb-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | disjin | |- ( Disj_ x e. B C -> Disj_ x e. B ( C i^i A ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elinel1 | |- ( y e. ( C i^i A ) -> y e. C ) |
|
2 | 1 | rmoimi | |- ( E* x e. B y e. C -> E* x e. B y e. ( C i^i A ) ) |
3 | 2 | alimi | |- ( A. y E* x e. B y e. C -> A. y E* x e. B y e. ( C i^i A ) ) |
4 | df-disj | |- ( Disj_ x e. B C <-> A. y E* x e. B y e. C ) |
|
5 | df-disj | |- ( Disj_ x e. B ( C i^i A ) <-> A. y E* x e. B y e. ( C i^i A ) ) |
|
6 | 3 4 5 | 3imtr4i | |- ( Disj_ x e. B C -> Disj_ x e. B ( C i^i A ) ) |