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 𝑅 ) ) ↔ 𝑅 ⊆ 𝑆 ) )