Theorem cnvssrndm

Description: The converse is a subset of the cartesian product of range and domain. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Assertion	cnvssrndm	⊢ ◡ 𝐴 ⊆ ( ran 𝐴 × dom 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		relcnv	⊢ Rel ◡ 𝐴
2		relssdmrn	⊢ ( Rel ◡ 𝐴 → ◡ 𝐴 ⊆ ( dom ◡ 𝐴 × ran ◡ 𝐴 ) )
3	1 2	ax-mp	⊢ ◡ 𝐴 ⊆ ( dom ◡ 𝐴 × ran ◡ 𝐴 )
4		df-rn	⊢ ran 𝐴 = dom ◡ 𝐴
5		dfdm4	⊢ dom 𝐴 = ran ◡ 𝐴
6	4 5	xpeq12i	⊢ ( ran 𝐴 × dom 𝐴 ) = ( dom ◡ 𝐴 × ran ◡ 𝐴 )
7	3 6	sseqtrri	⊢ ◡ 𝐴 ⊆ ( ran 𝐴 × dom 𝐴 )