Metamath Proof Explorer

Theorem resssxp

Description: If the R -image of a class A is a subclass of B , then the restriction of R to A is a subset of the Cartesian product of A and B . (Contributed by RP, 24-Dec-2019)

Ref Expression
Assertion resssxp ⊢ R A ⊆ B ↔ R ↾ A ⊆ A × B

Proof

Step Hyp Ref Expression
1 df-ima ⊢ R A = ran ⁡ R ↾ A
2 1 sseq1i ⊢ R A ⊆ B ↔ ran ⁡ R ↾ A ⊆ B
3 dmres ⊢ dom ⁡ R ↾ A = A ∩ dom ⁡ R
4 inss1 ⊢ A ∩ dom ⁡ R ⊆ A
5 3 4 eqsstri ⊢ dom ⁡ R ↾ A ⊆ A
6 5 biantrur ⊢ ran ⁡ R ↾ A ⊆ B ↔ dom ⁡ R ↾ A ⊆ A ∧ ran ⁡ R ↾ A ⊆ B
7 relres ⊢ Rel ⁡ R ↾ A
8 relssdmrn ⊢ Rel ⁡ R ↾ A → R ↾ A ⊆ dom ⁡ R ↾ A × ran ⁡ R ↾ A
9 7 8 ax-mp ⊢ R ↾ A ⊆ dom ⁡ R ↾ A × ran ⁡ R ↾ A
10 xpss12 ⊢ dom ⁡ R ↾ A ⊆ A ∧ ran ⁡ R ↾ A ⊆ B → dom ⁡ R ↾ A × ran ⁡ R ↾ A ⊆ A × B
11 9 10 sstrid ⊢ dom ⁡ R ↾ A ⊆ A ∧ ran ⁡ R ↾ A ⊆ B → R ↾ A ⊆ A × B
12 dmss ⊢ R ↾ A ⊆ A × B → dom ⁡ R ↾ A ⊆ dom ⁡ A × B
13 dmxpss ⊢ dom ⁡ A × B ⊆ A
14 12 13 sstrdi ⊢ R ↾ A ⊆ A × B → dom ⁡ R ↾ A ⊆ A
15 rnss ⊢ R ↾ A ⊆ A × B → ran ⁡ R ↾ A ⊆ ran ⁡ A × B
16 rnxpss ⊢ ran ⁡ A × B ⊆ B
17 15 16 sstrdi ⊢ R ↾ A ⊆ A × B → ran ⁡ R ↾ A ⊆ B
18 14 17 jca ⊢ R ↾ A ⊆ A × B → dom ⁡ R ↾ A ⊆ A ∧ ran ⁡ R ↾ A ⊆ B
19 11 18 impbii ⊢ dom ⁡ R ↾ A ⊆ A ∧ ran ⁡ R ↾ A ⊆ B ↔ R ↾ A ⊆ A × B
20 2 6 19 3bitri ⊢ R A ⊆ B ↔ R ↾ A ⊆ A × B