Metamath Proof Explorer

Theorem intimag

Description: Requirement for the image under the intersection of relations to equal the intersection of the images of those relations. (Contributed by RP, 13-Apr-2020)

Ref Expression
Assertion intimag ⊢∀y∀a∈A∃b∈Bby∈a→∃b∈B∀a∈Aby∈a→⋂AB=⋂x|∃a∈Ax=aB

Proof

Step Hyp Ref Expression
1 r19.12 ⊢∃b∈B∀a∈Aby∈a→∀a∈A∃b∈Bby∈a
2 id ⊢∀a∈A∃b∈Bby∈a→∃b∈B∀a∈Aby∈a→∀a∈A∃b∈Bby∈a→∃b∈B∀a∈Aby∈a
3 1 2 impbid2 ⊢∀a∈A∃b∈Bby∈a→∃b∈B∀a∈Aby∈a→∃b∈B∀a∈Aby∈a↔∀a∈A∃b∈Bby∈a
4 elimaint ⊢y∈⋂AB↔∃b∈B∀a∈Aby∈a
5 elintima ⊢y∈⋂x|∃a∈Ax=aB↔∀a∈A∃b∈Bby∈a
6 3 4 5 3bitr4g ⊢∀a∈A∃b∈Bby∈a→∃b∈B∀a∈Aby∈a→y∈⋂AB↔y∈⋂x|∃a∈Ax=aB
7 6 alimi ⊢∀y∀a∈A∃b∈Bby∈a→∃b∈B∀a∈Aby∈a→∀yy∈⋂AB↔y∈⋂x|∃a∈Ax=aB
8 dfcleq ⊢⋂AB=⋂x|∃a∈Ax=aB↔∀yy∈⋂AB↔y∈⋂x|∃a∈Ax=aB
9 7 8 sylibr ⊢∀y∀a∈A∃b∈Bby∈a→∃b∈B∀a∈Aby∈a→⋂AB=⋂x|∃a∈Ax=aB