This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑅 “ 𝐴 ) ⊆ 𝐵 ↔ ( 𝑅 ↾ 𝐴 ) ⊆ ( 𝐴 × 𝐵 ) )

Proof

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