trclubgNEW

Description: If a relation exists then the transitive closure has an upper bound. (Contributed by RP, 24-Jul-2020)

		Ref	Expression
	Hypothesis	trclubgNEW.rex	$⊢ φ \to R \in V$
	Assertion	trclubgNEW	$⊢ φ \to ⋂ \{x \| (R \subseteq x \land x \circ x \subseteq x)\} \subseteq R \cup (dom R \times ran R)$

Proof

Step	Hyp	Ref	Expression
1		trclubgNEW.rex	$⊢ φ \to R \in V$
2	1	dmexd	$⊢ φ \to dom R \in V$
3		rnexg	$⊢ R \in V \to ran R \in V$
4	1 3	syl	$⊢ φ \to ran R \in V$
5	2 4	xpexd	$⊢ φ \to dom R \times ran R \in V$
6	1 5	unexd	$⊢ φ \to R \cup (dom R \times ran R) \in V$
7		id	$⊢ x = R \cup (dom R \times ran R) \to x = R \cup (dom R \times ran R)$
8	7 7	coeq12d	$⊢ x = R \cup (dom R \times ran R) \to x \circ x = (R \cup (dom R \times ran R)) \circ (R \cup (dom R \times ran R))$
9	8 7	sseq12d	$⊢ x = R \cup (dom R \times ran R) \to (x \circ x \subseteq x \leftrightarrow (R \cup (dom R \times ran R)) \circ (R \cup (dom R \times ran R)) \subseteq R \cup (dom R \times ran R))$
10		ssun1	$⊢ R \subseteq R \cup (dom R \times ran R)$
11	10	a1i	$⊢ φ \to R \subseteq R \cup (dom R \times ran R)$
12		cnvssrndm	$⊢ R^{-1} \subseteq ran R \times dom R$
13		coundi	$⊢ (R \cup (dom R \times ran R)) \circ (R \cup (dom R \times ran R)) = ((R \cup (dom R \times ran R)) \circ R) \cup ((R \cup (dom R \times ran R)) \circ (dom R \times ran R))$
14		cnvss	$⊢ R^{-1} \subseteq ran R \times dom R \to {R^{-1}}^{-1} \subseteq {(ran R \times dom R)}^{-1}$
15		coss2	$⊢ {R^{-1}}^{-1} \subseteq {(ran R \times dom R)}^{-1} \to (R \cup (dom R \times ran R)) \circ {R^{-1}}^{-1} \subseteq (R \cup (dom R \times ran R)) \circ {(ran R \times dom R)}^{-1}$
16	14 15	syl	$⊢ R^{-1} \subseteq ran R \times dom R \to (R \cup (dom R \times ran R)) \circ {R^{-1}}^{-1} \subseteq (R \cup (dom R \times ran R)) \circ {(ran R \times dom R)}^{-1}$
17		cocnvcnv2	$⊢ (R \cup (dom R \times ran R)) \circ {R^{-1}}^{-1} = (R \cup (dom R \times ran R)) \circ R$
18		cnvxp	$⊢ {(ran R \times dom R)}^{-1} = dom R \times ran R$
19	18	coeq2i	$⊢ (R \cup (dom R \times ran R)) \circ {(ran R \times dom R)}^{-1} = (R \cup (dom R \times ran R)) \circ (dom R \times ran R)$
20	16 17 19	3sstr3g	$⊢ R^{-1} \subseteq ran R \times dom R \to (R \cup (dom R \times ran R)) \circ R \subseteq (R \cup (dom R \times ran R)) \circ (dom R \times ran R)$
21		ssequn1	$⊢ (R \cup (dom R \times ran R)) \circ R \subseteq (R \cup (dom R \times ran R)) \circ (dom R \times ran R) \leftrightarrow ((R \cup (dom R \times ran R)) \circ R) \cup ((R \cup (dom R \times ran R)) \circ (dom R \times ran R)) = (R \cup (dom R \times ran R)) \circ (dom R \times ran R)$
22	20 21	sylib	$⊢ R^{-1} \subseteq ran R \times dom R \to ((R \cup (dom R \times ran R)) \circ R) \cup ((R \cup (dom R \times ran R)) \circ (dom R \times ran R)) = (R \cup (dom R \times ran R)) \circ (dom R \times ran R)$
23		coundir	$⊢ (R \cup (dom R \times ran R)) \circ (dom R \times ran R) = (R \circ (dom R \times ran R)) \cup ((dom R \times ran R) \circ (dom R \times ran R))$
24		coss1	$⊢ {R^{-1}}^{-1} \subseteq {(ran R \times dom R)}^{-1} \to {R^{-1}}^{-1} \circ (dom R \times ran R) \subseteq {(ran R \times dom R)}^{-1} \circ (dom R \times ran R)$
25	14 24	syl	$⊢ R^{-1} \subseteq ran R \times dom R \to {R^{-1}}^{-1} \circ (dom R \times ran R) \subseteq {(ran R \times dom R)}^{-1} \circ (dom R \times ran R)$
26		cocnvcnv1	$⊢ {R^{-1}}^{-1} \circ (dom R \times ran R) = R \circ (dom R \times ran R)$
27	18	coeq1i	$⊢ {(ran R \times dom R)}^{-1} \circ (dom R \times ran R) = (dom R \times ran R) \circ (dom R \times ran R)$
28	25 26 27	3sstr3g	$⊢ R^{-1} \subseteq ran R \times dom R \to R \circ (dom R \times ran R) \subseteq (dom R \times ran R) \circ (dom R \times ran R)$
29		ssequn1	$⊢ R \circ (dom R \times ran R) \subseteq (dom R \times ran R) \circ (dom R \times ran R) \leftrightarrow (R \circ (dom R \times ran 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	$⊢ R^{-1} \subseteq ran R \times dom R \to (R \circ (dom R \times ran 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		xptrrel	$⊢ (dom R \times ran R) \circ (dom R \times ran R) \subseteq dom R \times ran R$
32		ssun2	$⊢ dom R \times ran R \subseteq R \cup (dom R \times ran R)$
33	31 32	sstri	$⊢ (dom R \times ran R) \circ (dom R \times ran R) \subseteq R \cup (dom R \times ran R)$
34	33	a1i	$⊢ R^{-1} \subseteq ran R \times dom R \to (dom R \times ran R) \circ (dom R \times ran R) \subseteq R \cup (dom R \times ran R)$
35	30 34	eqsstrd	$⊢ R^{-1} \subseteq ran R \times dom R \to (R \circ (dom R \times ran R)) \cup ((dom R \times ran R) \circ (dom R \times ran R)) \subseteq R \cup (dom R \times ran R)$
36	23 35	eqsstrid	$⊢ R^{-1} \subseteq ran R \times dom R \to (R \cup (dom R \times ran R)) \circ (dom R \times ran R) \subseteq R \cup (dom R \times ran R)$
37	22 36	eqsstrd	$⊢ R^{-1} \subseteq ran R \times dom R \to ((R \cup (dom R \times ran R)) \circ R) \cup ((R \cup (dom R \times ran R)) \circ (dom R \times ran R)) \subseteq R \cup (dom R \times ran R)$
38	13 37	eqsstrid	$⊢ R^{-1} \subseteq ran R \times dom R \to (R \cup (dom R \times ran R)) \circ (R \cup (dom R \times ran R)) \subseteq R \cup (dom R \times ran R)$
39	12 38	mp1i	$⊢ φ \to (R \cup (dom R \times ran R)) \circ (R \cup (dom R \times ran R)) \subseteq R \cup (dom R \times ran R)$
40	6 9 11 39	clublem	$⊢ φ \to ⋂ \{x \| (R \subseteq x \land x \circ x \subseteq x)\} \subseteq R \cup (dom R \times ran R)$

Metamath Proof Explorer

Theorem trclubgNEW

Proof