dmtrcl

Description: The domain of the transitive closure is equal to the domain of its base relation. (Contributed by RP, 1-Nov-2020)

		Ref	Expression
	Assertion	dmtrcl	$⊢ X \in V \to dom ⋂ \{x \| (X \subseteq x \land x \circ x \subseteq x)\} = dom X$

Step	Hyp	Ref	Expression
1		trclubg	$⊢ X \in V \to ⋂ \{x \| (X \subseteq x \land x \circ x \subseteq x)\} \subseteq X \cup (dom X \times ran X)$
2		dmss	$⊢ ⋂ \{x \| (X \subseteq x \land x \circ x \subseteq x)\} \subseteq X \cup (dom X \times ran X) \to dom ⋂ \{x \| (X \subseteq x \land x \circ x \subseteq x)\} \subseteq dom (X \cup (dom X \times ran X))$
3	1 2	syl	$⊢ X \in V \to dom ⋂ \{x \| (X \subseteq x \land x \circ x \subseteq x)\} \subseteq dom (X \cup (dom X \times ran X))$
4		dmun	$⊢ dom (X \cup (dom X \times ran X)) = dom X \cup dom (dom X \times ran X)$
5		dmxpss	$⊢ dom (dom X \times ran X) \subseteq dom X$
6		ssequn2	$⊢ dom (dom X \times ran X) \subseteq dom X \leftrightarrow dom X \cup dom (dom X \times ran X) = dom X$
7	5 6	mpbi	$⊢ dom X \cup dom (dom X \times ran X) = dom X$
8	4 7	eqtri	$⊢ dom (X \cup (dom X \times ran X)) = dom X$
9	3 8	sseqtrdi	$⊢ X \in V \to dom ⋂ \{x \| (X \subseteq x \land x \circ x \subseteq x)\} \subseteq dom X$
10		ssmin	$⊢ X \subseteq ⋂ \{x \| (X \subseteq x \land x \circ x \subseteq x)\}$
11		dmss	$⊢ X \subseteq ⋂ \{x \| (X \subseteq x \land x \circ x \subseteq x)\} \to dom X \subseteq dom ⋂ \{x \| (X \subseteq x \land x \circ x \subseteq x)\}$
12	10 11	mp1i	$⊢ X \in V \to dom X \subseteq dom ⋂ \{x \| (X \subseteq x \land x \circ x \subseteq x)\}$
13	9 12	eqssd	$⊢ X \in V \to dom ⋂ \{x \| (X \subseteq x \land x \circ x \subseteq x)\} = dom X$

Metamath Proof Explorer