trclfv

Description: The transitive closure of a relation. (Contributed by RP, 28-Apr-2020)

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

Step	Hyp	Ref	Expression
1		elex	$⊢ R \in V \to R \in V$
2		trclexlem	$⊢ R \in V \to R \cup (dom R \times ran R) \in V$
3		trclubg	$⊢ R \in V \to ⋂ \{x \| (R \subseteq x \land x \circ x \subseteq x)\} \subseteq R \cup (dom R \times ran R)$
4	2 3	ssexd	$⊢ R \in V \to ⋂ \{x \| (R \subseteq x \land x \circ x \subseteq x)\} \in V$
5		trcleq1	$⊢ r = R \to ⋂ \{x \| (r \subseteq x \land x \circ x \subseteq x)\} = ⋂ \{x \| (R \subseteq x \land x \circ x \subseteq x)\}$
6		df-trcl	$⊢ t+ = (r \in V ⟼ ⋂ \{x \| (r \subseteq x \land x \circ x \subseteq x)\})$
7	5 6	fvmptg	$⊢ (R \in V \land ⋂ \{x \| (R \subseteq x \land x \circ x \subseteq x)\} \in V) \to t+ (R) = ⋂ \{x \| (R \subseteq x \land x \circ x \subseteq x)\}$
8	1 4 7	syl2anc2	$⊢ R \in V \to t+ (R) = ⋂ \{x \| (R \subseteq x \land x \circ x \subseteq x)\}$

Metamath Proof Explorer