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 ∈ B b y ∈ a → ∃ b ∈ B ∀ a ∈ A b y ∈ a → ⋂ A B = ⋂ x | ∃ a ∈ A x = a B

Proof

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