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

Metamath Proof Explorer

Theorem cnvref4

Description: Two ways to say that a relation is a subclass. (Contributed by Peter Mazsa, 11-Apr-2023)

Ref Expression
Assertion cnvref4 ( Rel 𝑅 → ( ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ ( 𝑆 ∩ ( dom 𝑅 × ran 𝑅 ) ) ↔ 𝑅 ⊆ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 dfrel6 ⊢ ( Rel 𝑅 ↔ ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) = 𝑅 )
2 1 biimpi ⊢ ( Rel 𝑅 → ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) = 𝑅 )
3 2 dmeqd ⊢ ( Rel 𝑅 → dom ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) = dom 𝑅 )
4 2 rneqd ⊢ ( Rel 𝑅 → ran ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) = ran 𝑅 )
5 3 4 xpeq12d ⊢ ( Rel 𝑅 → ( dom ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) × ran ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ) = ( dom 𝑅 × ran 𝑅 ) )
6 5 ineq2d ⊢ ( Rel 𝑅 → ( 𝑆 ∩ ( dom ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) × ran ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ) ) = ( 𝑆 ∩ ( dom 𝑅 × ran 𝑅 ) ) )
7 6 sseq2d ⊢ ( Rel 𝑅 → ( ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ ( 𝑆 ∩ ( dom ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) × ran ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ) ) ↔ ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ ( 𝑆 ∩ ( dom 𝑅 × ran 𝑅 ) ) ) )
8 relxp ⊢ Rel ( dom 𝑅 × ran 𝑅 )
9 relin2 ⊢ ( Rel ( dom 𝑅 × ran 𝑅 ) → Rel ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) )
10 relssinxpdmrn ⊢ ( Rel ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) → ( ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ ( 𝑆 ∩ ( dom ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) × ran ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ) ) ↔ ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ 𝑆 ) )
11 8 9 10 mp2b ⊢ ( ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ ( 𝑆 ∩ ( dom ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) × ran ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ) ) ↔ ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ 𝑆 )
12 2 sseq1d ⊢ ( Rel 𝑅 → ( ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ 𝑆 ↔ 𝑅 ⊆ 𝑆 ) )
13 11 12 bitrid ⊢ ( Rel 𝑅 → ( ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ ( 𝑆 ∩ ( dom ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) × ran ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ) ) ↔ 𝑅 ⊆ 𝑆 ) )
14 7 13 bitr3d ⊢ ( Rel 𝑅 → ( ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ ( 𝑆 ∩ ( dom 𝑅 × ran 𝑅 ) ) ↔ 𝑅 ⊆ 𝑆 ) )