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 \land Rel dom A) \leftrightarrow A \subseteq (V \times V) \times V$

Proof

Step	Hyp	Ref	Expression
1		df-rel	$⊢ Rel dom A \leftrightarrow dom A \subseteq V \times V$
2	1	anbi2i	$⊢ (Rel A \land Rel dom A) \leftrightarrow (Rel A \land dom A \subseteq V \times V)$
3		relssdmrn	$⊢ Rel A \to A \subseteq dom A \times ran A$
4		ssv	$⊢ ran A \subseteq V$
5		xpss12	$⊢ (dom A \subseteq V \times V \land ran A \subseteq V) \to dom A \times ran A \subseteq (V \times V) \times V$
6	4 5	mpan2	$⊢ dom A \subseteq V \times V \to dom A \times ran A \subseteq (V \times V) \times V$
7	3 6	sylan9ss	$⊢ (Rel A \land dom A \subseteq V \times V) \to A \subseteq (V \times V) \times V$
8		xpss	$⊢ (V \times V) \times V \subseteq V \times V$
9		sstr	$⊢ (A \subseteq (V \times V) \times V \land (V \times V) \times V \subseteq V \times V) \to A \subseteq V \times V$
10	8 9	mpan2	$⊢ A \subseteq (V \times V) \times V \to A \subseteq V \times V$
11		df-rel	$⊢ Rel A \leftrightarrow A \subseteq V \times V$
12	10 11	sylibr	$⊢ A \subseteq (V \times V) \times V \to Rel A$
13		dmss	$⊢ A \subseteq (V \times V) \times V \to dom A \subseteq dom ((V \times V) \times V)$
14		vn0	$⊢ V \neq \emptyset$
15		dmxp	$⊢ V \neq \emptyset \to dom ((V \times V) \times V) = V \times V$
16	14 15	ax-mp	$⊢ dom ((V \times V) \times V) = V \times V$
17	13 16	sseqtrdi	$⊢ A \subseteq (V \times V) \times V \to dom A \subseteq V \times V$
18	12 17	jca	$⊢ A \subseteq (V \times V) \times V \to (Rel A \land dom A \subseteq V \times V)$
19	7 18	impbii	$⊢ (Rel A \land dom A \subseteq V \times V) \leftrightarrow A \subseteq (V \times V) \times V$
20	2 19	bitri	$⊢ (Rel A \land Rel dom A) \leftrightarrow A \subseteq (V \times V) \times V$

Metamath Proof Explorer

Theorem relrelss

Proof