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		unexg	$⊢ (R \in V \land dom R \times ran R \in V) \to R \cup (dom R \times ran R) \in V$
7	1 5 6	syl2anc	$⊢ φ \to R \cup (dom R \times ran R) \in V$
8		id	$⊢ x = R \cup (dom R \times ran R) \to x = R \cup (dom R \times ran R)$
9	8 8	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))$
10	9 8	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))$
11		ssun1	$⊢ R \subseteq R \cup (dom R \times ran R)$
12	11	a1i	$⊢ φ \to R \subseteq R \cup (dom R \times ran R)$
13		cnvssrndm	$⊢ R^{-1} \subseteq ran R \times dom R$
14		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))$
15		cnvss	$⊢ R^{-1} \subseteq ran R \times dom R \to {R^{-1}}^{-1} \subseteq {(ran R \times dom R)}^{-1}$
16		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}$
17	15 16	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}$
18		cocnvcnv2	$⊢ (R \cup (dom R \times ran R)) \circ {R^{-1}}^{-1} = (R \cup (dom R \times ran R)) \circ R$
19		cnvxp	$⊢ {(ran R \times dom R)}^{-1} = dom R \times ran R$
20	19	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)$
21	17 18 20	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)$
22		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)$
23	21 22	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)$
24		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))$
25		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)$
26	15 25	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)$
27		cocnvcnv1	$⊢ {R^{-1}}^{-1} \circ (dom R \times ran R) = R \circ (dom R \times ran R)$
28	19	coeq1i	$⊢ {(ran R \times dom R)}^{-1} \circ (dom R \times ran R) = (dom R \times ran R) \circ (dom R \times ran R)$
29	26 27 28	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)$
30		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)$
31	29 30	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)$
32		xptrrel	$⊢ (dom R \times ran R) \circ (dom R \times ran R) \subseteq dom R \times ran R$
33		ssun2	$⊢ dom R \times ran R \subseteq R \cup (dom R \times ran R)$
34	32 33	sstri	$⊢ (dom R \times ran R) \circ (dom R \times ran R) \subseteq R \cup (dom R \times ran R)$
35	34	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)$
36	31 35	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)$
37	24 36	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)$
38	23 37	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)$
39	14 38	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)$
40	13 39	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)$
41	7 10 12 40	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