Metamath Proof Explorer

Theorem rninxp

Description: Two ways to express surjectivity of a restricted and corestricted binary relation (intersection of a binary relation with a Cartesian product). (Contributed by NM, 17-Jan-2006) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion rninxp ⊢ ran ⁡ C ∩ A × B = B ↔ ∀ y ∈ B ∃ x ∈ A x C y

Proof

Step Hyp Ref Expression
1 dfss3 ⊢ B ⊆ ran ⁡ C ↾ A ↔ ∀ y ∈ B y ∈ ran ⁡ C ↾ A
2 ssrnres ⊢ B ⊆ ran ⁡ C ↾ A ↔ ran ⁡ C ∩ A × B = B
3 df-ima ⊢ C A = ran ⁡ C ↾ A
4 3 eleq2i ⊢ y ∈ C A ↔ y ∈ ran ⁡ C ↾ A
5 vex ⊢ y ∈ V
6 5 elima ⊢ y ∈ C A ↔ ∃ x ∈ A x C y
7 4 6 bitr3i ⊢ y ∈ ran ⁡ C ↾ A ↔ ∃ x ∈ A x C y
8 7 ralbii ⊢ ∀ y ∈ B y ∈ ran ⁡ C ↾ A ↔ ∀ y ∈ B ∃ x ∈ A x C y
9 1 2 8 3bitr3i ⊢ ran ⁡ C ∩ A × B = B ↔ ∀ y ∈ B ∃ x ∈ A x C y