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

Metamath Proof Explorer

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