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 ⁡ A ∧ Rel ⁡ dom ⁡ A ↔ A ⊆ V × V × V

Proof

Step Hyp Ref Expression
1 df-rel ⊢ Rel ⁡ dom ⁡ A ↔ dom ⁡ A ⊆ V × V
2 1 anbi2i ⊢ Rel ⁡ A ∧ Rel ⁡ dom ⁡ A ↔ Rel ⁡ A ∧ dom ⁡ A ⊆ V × V
3 relssdmrn ⊢ Rel ⁡ A → A ⊆ dom ⁡ A × ran ⁡ A
4 ssv ⊢ ran ⁡ A ⊆ V
5 xpss12 ⊢ dom ⁡ A ⊆ V × V ∧ ran ⁡ A ⊆ V → dom ⁡ A × ran ⁡ A ⊆ V × V × V
6 4 5 mpan2 ⊢ dom ⁡ A ⊆ V × V → dom ⁡ A × ran ⁡ A ⊆ V × V × V
7 3 6 sylan9ss ⊢ Rel ⁡ A ∧ dom ⁡ A ⊆ V × V → A ⊆ V × V × V
8 xpss ⊢ V × V × V ⊆ V × V
9 sstr ⊢ A ⊆ V × V × V ∧ V × V × V ⊆ V × V → A ⊆ V × V
10 8 9 mpan2 ⊢ A ⊆ V × V × V → A ⊆ V × V
11 df-rel ⊢ Rel ⁡ A ↔ A ⊆ V × V
12 10 11 sylibr ⊢ A ⊆ V × V × V → Rel ⁡ A
13 dmss ⊢ A ⊆ V × V × V → dom ⁡ A ⊆ 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 ⊢ A ⊆ V × V × V → dom ⁡ A ⊆ V × V
18 12 17 jca ⊢ A ⊆ V × V × V → Rel ⁡ A ∧ dom ⁡ A ⊆ V × V
19 7 18 impbii ⊢ Rel ⁡ A ∧ dom ⁡ A ⊆ V × V ↔ A ⊆ V × V × V
20 2 19 bitri ⊢ Rel ⁡ A ∧ Rel ⁡ dom ⁡ A ↔ A ⊆ V × V × V