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