dfttrcl2

Description: When R is a set and a relation, then its transitive closure can be defined by an intersection. (Contributed by Scott Fenton, 26-Oct-2024)

		Ref	Expression
	Assertion	dfttrcl2	$⊢ (R \in V \land Rel R) \to t++ R = ⋂ \{z \| (R \subseteq z \land z \circ z \subseteq z)\}$

Proof

Step	Hyp	Ref	Expression
1		ssintab	$⊢ t++ R \subseteq ⋂ \{z \| (R \subseteq z \land z \circ z \subseteq z)\} \leftrightarrow \forall z ((R \subseteq z \land z \circ z \subseteq z) \to t++ R \subseteq z)$
2		ttrclss	$⊢ (R \subseteq z \land z \circ z \subseteq z) \to t++ R \subseteq z$
3	1 2	mpgbir	$⊢ t++ R \subseteq ⋂ \{z \| (R \subseteq z \land z \circ z \subseteq z)\}$
4	3	a1i	$⊢ (R \in V \land Rel R) \to t++ R \subseteq ⋂ \{z \| (R \subseteq z \land z \circ z \subseteq z)\}$
5		rabab	$⊢ \{z \in V \| (R \subseteq z \land z \circ z \subseteq z)\} = \{z \| (R \subseteq z \land z \circ z \subseteq z)\}$
6	5	inteqi	$⊢ ⋂ \{z \in V \| (R \subseteq z \land z \circ z \subseteq z)\} = ⋂ \{z \| (R \subseteq z \land z \circ z \subseteq z)\}$
7		ttrclexg	$⊢ R \in V \to t++ R \in V$
8		ssttrcl	$⊢ Rel R \to R \subseteq t++ R$
9		ttrcltr	$⊢ t++ R \circ t++ R \subseteq t++ R$
10	8 9	jctir	$⊢ Rel R \to (R \subseteq t++ R \land t++ R \circ t++ R \subseteq t++ R)$
11		sseq2	$⊢ z = t++ R \to (R \subseteq z \leftrightarrow R \subseteq t++ R)$
12		coeq1	$⊢ z = t++ R \to z \circ z = t++ R \circ z$
13		coeq2	$⊢ z = t++ R \to t++ R \circ z = t++ R \circ t++ R$
14	12 13	eqtrd	$⊢ z = t++ R \to z \circ z = t++ R \circ t++ R$
15		id	$⊢ z = t++ R \to z = t++ R$
16	14 15	sseq12d	$⊢ z = t++ R \to (z \circ z \subseteq z \leftrightarrow t++ R \circ t++ R \subseteq t++ R)$
17	11 16	anbi12d	$⊢ z = t++ R \to ((R \subseteq z \land z \circ z \subseteq z) \leftrightarrow (R \subseteq t++ R \land t++ R \circ t++ R \subseteq t++ R))$
18	17	intminss	$⊢ (t++ R \in V \land (R \subseteq t++ R \land t++ R \circ t++ R \subseteq t++ R)) \to ⋂ \{z \in V \| (R \subseteq z \land z \circ z \subseteq z)\} \subseteq t++ R$
19	7 10 18	syl2an	$⊢ (R \in V \land Rel R) \to ⋂ \{z \in V \| (R \subseteq z \land z \circ z \subseteq z)\} \subseteq t++ R$
20	6 19	eqsstrrid	$⊢ (R \in V \land Rel R) \to ⋂ \{z \| (R \subseteq z \land z \circ z \subseteq z)\} \subseteq t++ R$
21	4 20	eqssd	$⊢ (R \in V \land Rel R) \to t++ R = ⋂ \{z \| (R \subseteq z \land z \circ z \subseteq z)\}$

Metamath Proof Explorer

Theorem dfttrcl2

Proof