Theorem relrelss

Description: Two ways to describe the structure of a two-place operation. (Contributed by NM, 17-Dec-2008)

	Ref	Expression
Assertion	relrelss	⊢ ( ( Rel 𝐴 ∧ Rel dom 𝐴 ) ↔ 𝐴 ⊆ ( ( V × V ) × V ) )

Proof

Step	Hyp	Ref	Expression
1		df-rel	⊢ ( Rel dom 𝐴 ↔ dom 𝐴 ⊆ ( V × V ) )
2	1	anbi2i	⊢ ( ( Rel 𝐴 ∧ Rel dom 𝐴 ) ↔ ( Rel 𝐴 ∧ dom 𝐴 ⊆ ( V × V ) ) )
3		relssdmrn	⊢ ( Rel 𝐴 → 𝐴 ⊆ ( dom 𝐴 × ran 𝐴 ) )
4		ssv	⊢ ran 𝐴 ⊆ V
5		xpss12	⊢ ( ( dom 𝐴 ⊆ ( V × V ) ∧ ran 𝐴 ⊆ V ) → ( dom 𝐴 × ran 𝐴 ) ⊆ ( ( V × V ) × V ) )
6	4 5	mpan2	⊢ ( dom 𝐴 ⊆ ( V × V ) → ( dom 𝐴 × ran 𝐴 ) ⊆ ( ( V × V ) × V ) )
7	3 6	sylan9ss	⊢ ( ( Rel 𝐴 ∧ dom 𝐴 ⊆ ( V × V ) ) → 𝐴 ⊆ ( ( V × V ) × V ) )
8		xpss	⊢ ( ( V × V ) × V ) ⊆ ( V × V )
9		sstr	⊢ ( ( 𝐴 ⊆ ( ( V × V ) × V ) ∧ ( ( V × V ) × V ) ⊆ ( V × V ) ) → 𝐴 ⊆ ( V × V ) )
10	8 9	mpan2	⊢ ( 𝐴 ⊆ ( ( V × V ) × V ) → 𝐴 ⊆ ( V × V ) )
11		df-rel	⊢ ( Rel 𝐴 ↔ 𝐴 ⊆ ( V × V ) )
12	10 11	sylibr	⊢ ( 𝐴 ⊆ ( ( V × V ) × V ) → Rel 𝐴 )
13		dmss	⊢ ( 𝐴 ⊆ ( ( V × V ) × V ) → dom 𝐴 ⊆ dom ( ( V × V ) × V ) )
14		vn0	⊢ V ≠ ∅
15		dmxp	⊢ ( V ≠ ∅ → dom ( ( V × V ) × V ) = ( V × V ) )
16	14 15	ax-mp	⊢ dom ( ( V × V ) × V ) = ( V × V )
17	13 16	sseqtrdi	⊢ ( 𝐴 ⊆ ( ( V × V ) × V ) → dom 𝐴 ⊆ ( V × V ) )
18	12 17	jca	⊢ ( 𝐴 ⊆ ( ( V × V ) × V ) → ( Rel 𝐴 ∧ dom 𝐴 ⊆ ( V × V ) ) )
19	7 18	impbii	⊢ ( ( Rel 𝐴 ∧ dom 𝐴 ⊆ ( V × V ) ) ↔ 𝐴 ⊆ ( ( V × V ) × V ) )
20	2 19	bitri	⊢ ( ( Rel 𝐴 ∧ Rel dom 𝐴 ) ↔ 𝐴 ⊆ ( ( V × V ) × V ) )