Metamath Proof Explorer


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 𝐴 )