Metamath Proof Explorer

Theorem ssrnres

Description: Two ways to express surjectivity of a restricted and corestricted binary relation (intersection of a binary relation with a Cartesian product): the LHS expresses inclusion in the range of the restricted relation, while the RHS expresses equality with the range of the restricted and corestricted relation. (Contributed by NM, 16-Jan-2006) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion ssrnres ⊢ B ⊆ ran ⁡ C ↾ A ↔ ran ⁡ C ∩ A × B = B

Proof

Step Hyp Ref Expression
1 inss2 ⊢ C ∩ A × B ⊆ A × B
2 1 rnssi ⊢ ran ⁡ C ∩ A × B ⊆ ran ⁡ A × B
3 rnxpss ⊢ ran ⁡ A × B ⊆ B
4 2 3 sstri ⊢ ran ⁡ C ∩ A × B ⊆ B
5 eqss ⊢ ran ⁡ C ∩ A × B = B ↔ ran ⁡ C ∩ A × B ⊆ B ∧ B ⊆ ran ⁡ C ∩ A × B
6 4 5 mpbiran ⊢ ran ⁡ C ∩ A × B = B ↔ B ⊆ ran ⁡ C ∩ A × B
7 inxpssres ⊢ C ∩ A × B ⊆ C ↾ A
8 7 rnssi ⊢ ran ⁡ C ∩ A × B ⊆ ran ⁡ C ↾ A
9 sstr ⊢ B ⊆ ran ⁡ C ∩ A × B ∧ ran ⁡ C ∩ A × B ⊆ ran ⁡ C ↾ A → B ⊆ ran ⁡ C ↾ A
10 8 9 mpan2 ⊢ B ⊆ ran ⁡ C ∩ A × B → B ⊆ ran ⁡ C ↾ A
11 ssel ⊢ B ⊆ ran ⁡ C ↾ A → y ∈ B → y ∈ ran ⁡ C ↾ A
12 vex ⊢ y ∈ V
13 12 elrn2 ⊢ y ∈ ran ⁡ C ↾ A ↔ ∃ x x y ∈ C ↾ A
14 11 13 syl6ib ⊢ B ⊆ ran ⁡ C ↾ A → y ∈ B → ∃ x x y ∈ C ↾ A
15 14 ancld ⊢ B ⊆ ran ⁡ C ↾ A → y ∈ B → y ∈ B ∧ ∃ x x y ∈ C ↾ A
16 12 elrn2 ⊢ y ∈ ran ⁡ C ∩ A × B ↔ ∃ x x y ∈ C ∩ A × B
17 opelinxp ⊢ x y ∈ C ∩ A × B ↔ x ∈ A ∧ y ∈ B ∧ x y ∈ C
18 12 opelresi ⊢ x y ∈ C ↾ A ↔ x ∈ A ∧ x y ∈ C
19 18 bianassc ⊢ y ∈ B ∧ x y ∈ C ↾ A ↔ x ∈ A ∧ y ∈ B ∧ x y ∈ C
20 17 19 bitr4i ⊢ x y ∈ C ∩ A × B ↔ y ∈ B ∧ x y ∈ C ↾ A
21 20 exbii ⊢ ∃ x x y ∈ C ∩ A × B ↔ ∃ x y ∈ B ∧ x y ∈ C ↾ A
22 19.42v ⊢ ∃ x y ∈ B ∧ x y ∈ C ↾ A ↔ y ∈ B ∧ ∃ x x y ∈ C ↾ A
23 16 21 22 3bitri ⊢ y ∈ ran ⁡ C ∩ A × B ↔ y ∈ B ∧ ∃ x x y ∈ C ↾ A
24 15 23 syl6ibr ⊢ B ⊆ ran ⁡ C ↾ A → y ∈ B → y ∈ ran ⁡ C ∩ A × B
25 24 ssrdv ⊢ B ⊆ ran ⁡ C ↾ A → B ⊆ ran ⁡ C ∩ A × B
26 10 25 impbii ⊢ B ⊆ ran ⁡ C ∩ A × B ↔ B ⊆ ran ⁡ C ↾ A
27 6 26 bitr2i ⊢ B ⊆ ran ⁡ C ↾ A ↔ ran ⁡ C ∩ A × B = B