trrelsuperrel2dg

Description: Concrete construction of a superclass of relation R which is a transitive relation. (Contributed by RP, 20-Jul-2020)

		Ref	Expression
	Hypothesis	trrelsuperrel2dg.s	$⊢ φ \to S = R \cup (dom R \times ran R)$
	Assertion	trrelsuperrel2dg	$⊢ φ \to (R \subseteq S \land S \circ S \subseteq S)$

Proof

Step	Hyp	Ref	Expression
1		trrelsuperrel2dg.s	$⊢ φ \to S = R \cup (dom R \times ran R)$
2		ssun1	$⊢ R \subseteq R \cup (dom R \times ran R)$
3	2 1	sseqtrrid	$⊢ φ \to R \subseteq S$
4		xptrrel	$⊢ (dom R \times ran R) \circ (dom R \times ran R) \subseteq dom R \times ran R$
5		ssun2	$⊢ dom R \times ran R \subseteq R \cup (dom R \times ran R)$
6	4 5	sstri	$⊢ (dom R \times ran R) \circ (dom R \times ran R) \subseteq R \cup (dom R \times ran R)$
7	6	a1i	$⊢ φ \to (dom R \times ran R) \circ (dom R \times ran R) \subseteq R \cup (dom R \times ran R)$
8	1 1	coeq12d	$⊢ φ \to S \circ S = (R \cup (dom R \times ran R)) \circ (R \cup (dom R \times ran R))$
9		coundir	$⊢ (R \cup (dom R \times ran R)) \circ (R \cup (dom R \times ran R)) = (R \circ (R \cup (dom R \times ran R))) \cup ((dom R \times ran R) \circ (R \cup (dom R \times ran R)))$
10		relcnv	$⊢ Rel {R^{-1}}^{-1}$
11		cocnvcnv1	$⊢ {R^{-1}}^{-1} \circ (R \cup (dom R \times ran R)) = R \circ (R \cup (dom R \times ran R))$
12		relssdmrn	$⊢ Rel {R^{-1}}^{-1} \to {R^{-1}}^{-1} \subseteq dom {R^{-1}}^{-1} \times ran {R^{-1}}^{-1}$
13		dmcnvcnv	$⊢ dom {R^{-1}}^{-1} = dom R$
14		rncnvcnv	$⊢ ran {R^{-1}}^{-1} = ran R$
15	13 14	xpeq12i	$⊢ dom {R^{-1}}^{-1} \times ran {R^{-1}}^{-1} = dom R \times ran R$
16	12 15	sseqtrdi	$⊢ Rel {R^{-1}}^{-1} \to {R^{-1}}^{-1} \subseteq dom R \times ran R$
17		coss1	$⊢ {R^{-1}}^{-1} \subseteq dom R \times ran R \to {R^{-1}}^{-1} \circ (R \cup (dom R \times ran R)) \subseteq (dom R \times ran R) \circ (R \cup (dom R \times ran R))$
18	16 17	syl	$⊢ Rel {R^{-1}}^{-1} \to {R^{-1}}^{-1} \circ (R \cup (dom R \times ran R)) \subseteq (dom R \times ran R) \circ (R \cup (dom R \times ran R))$
19	11 18	eqsstrrid	$⊢ Rel {R^{-1}}^{-1} \to R \circ (R \cup (dom R \times ran R)) \subseteq (dom R \times ran R) \circ (R \cup (dom R \times ran R))$
20		ssequn1	$⊢ R \circ (R \cup (dom R \times ran R)) \subseteq (dom R \times ran R) \circ (R \cup (dom R \times ran R)) \leftrightarrow (R \circ (R \cup (dom R \times ran R))) \cup ((dom R \times ran R) \circ (R \cup (dom R \times ran R))) = (dom R \times ran R) \circ (R \cup (dom R \times ran R))$
21	19 20	sylib	$⊢ Rel {R^{-1}}^{-1} \to (R \circ (R \cup (dom R \times ran R))) \cup ((dom R \times ran R) \circ (R \cup (dom R \times ran R))) = (dom R \times ran R) \circ (R \cup (dom R \times ran R))$
22	10 21	ax-mp	$⊢ (R \circ (R \cup (dom R \times ran R))) \cup ((dom R \times ran R) \circ (R \cup (dom R \times ran R))) = (dom R \times ran R) \circ (R \cup (dom R \times ran R))$
23	9 22	eqtri	$⊢ (R \cup (dom R \times ran R)) \circ (R \cup (dom R \times ran R)) = (dom R \times ran R) \circ (R \cup (dom R \times ran R))$
24		coundi	$⊢ (dom R \times ran R) \circ (R \cup (dom R \times ran R)) = ((dom R \times ran R) \circ R) \cup ((dom R \times ran R) \circ (dom R \times ran R))$
25		cocnvcnv2	$⊢ (dom R \times ran R) \circ {R^{-1}}^{-1} = (dom R \times ran R) \circ R$
26		coss2	$⊢ {R^{-1}}^{-1} \subseteq dom R \times ran R \to (dom R \times ran R) \circ {R^{-1}}^{-1} \subseteq (dom R \times ran R) \circ (dom R \times ran R)$
27	16 26	syl	$⊢ Rel {R^{-1}}^{-1} \to (dom R \times ran R) \circ {R^{-1}}^{-1} \subseteq (dom R \times ran R) \circ (dom R \times ran R)$
28	25 27	eqsstrrid	$⊢ Rel {R^{-1}}^{-1} \to (dom R \times ran R) \circ R \subseteq (dom R \times ran R) \circ (dom R \times ran R)$
29		ssequn1	$⊢ (dom R \times ran R) \circ R \subseteq (dom R \times ran R) \circ (dom R \times ran R) \leftrightarrow ((dom R \times ran R) \circ R) \cup ((dom R \times ran R) \circ (dom R \times ran R)) = (dom R \times ran R) \circ (dom R \times ran R)$
30	28 29	sylib	$⊢ Rel {R^{-1}}^{-1} \to ((dom R \times ran R) \circ R) \cup ((dom R \times ran R) \circ (dom R \times ran R)) = (dom R \times ran R) \circ (dom R \times ran R)$
31	10 30	ax-mp	$⊢ ((dom R \times ran R) \circ R) \cup ((dom R \times ran R) \circ (dom R \times ran R)) = (dom R \times ran R) \circ (dom R \times ran R)$
32	24 31	eqtri	$⊢ (dom R \times ran R) \circ (R \cup (dom R \times ran R)) = (dom R \times ran R) \circ (dom R \times ran R)$
33	23 32	eqtri	$⊢ (R \cup (dom R \times ran R)) \circ (R \cup (dom R \times ran R)) = (dom R \times ran R) \circ (dom R \times ran R)$
34	8 33	eqtrdi	$⊢ φ \to S \circ S = (dom R \times ran R) \circ (dom R \times ran R)$
35	7 34 1	3sstr4d	$⊢ φ \to S \circ S \subseteq S$
36	3 35	jca	$⊢ φ \to (R \subseteq S \land S \circ S \subseteq S)$

Metamath Proof Explorer

Theorem trrelsuperrel2dg

Proof