dmtrclfv

Description: The domain of the transitive closure is equal to the domain of the relation. (Contributed by RP, 9-May-2020)

		Ref	Expression
	Assertion	dmtrclfv	$⊢ R \in V \to dom t+ (R) = dom R$

Proof

Step	Hyp	Ref	Expression
1		trclfvub	$⊢ R \in V \to t+ (R) \subseteq R \cup (dom R \times ran R)$
2		dmss	$⊢ t+ (R) \subseteq R \cup (dom R \times ran R) \to dom t+ (R) \subseteq dom (R \cup (dom R \times ran R))$
3	1 2	syl	$⊢ R \in V \to dom t+ (R) \subseteq dom (R \cup (dom R \times ran R))$
4		dmun	$⊢ dom (R \cup (dom R \times ran R)) = dom R \cup dom (dom R \times ran R)$
5		dm0rn0	$⊢ dom R = \emptyset \leftrightarrow ran R = \emptyset$
6		xpeq1	$⊢ dom R = \emptyset \to dom R \times ran R = \emptyset \times ran R$
7		0xp	$⊢ \emptyset \times ran R = \emptyset$
8	6 7	eqtrdi	$⊢ dom R = \emptyset \to dom R \times ran R = \emptyset$
9	8	dmeqd	$⊢ dom R = \emptyset \to dom (dom R \times ran R) = dom \emptyset$
10		dm0	$⊢ dom \emptyset = \emptyset$
11	10	a1i	$⊢ dom R = \emptyset \to dom \emptyset = \emptyset$
12		eqcom	$⊢ dom R = \emptyset \leftrightarrow \emptyset = dom R$
13	12	biimpi	$⊢ dom R = \emptyset \to \emptyset = dom R$
14	9 11 13	3eqtrd	$⊢ dom R = \emptyset \to dom (dom R \times ran R) = dom R$
15	5 14	sylbir	$⊢ ran R = \emptyset \to dom (dom R \times ran R) = dom R$
16		dmxp	$⊢ ran R \neq \emptyset \to dom (dom R \times ran R) = dom R$
17	15 16	pm2.61ine	$⊢ dom (dom R \times ran R) = dom R$
18	17	uneq2i	$⊢ dom R \cup dom (dom R \times ran R) = dom R \cup dom R$
19		unidm	$⊢ dom R \cup dom R = dom R$
20	4 18 19	3eqtri	$⊢ dom (R \cup (dom R \times ran R)) = dom R$
21	3 20	sseqtrdi	$⊢ R \in V \to dom t+ (R) \subseteq dom R$
22		trclfvlb	$⊢ R \in V \to R \subseteq t+ (R)$
23		dmss	$⊢ R \subseteq t+ (R) \to dom R \subseteq dom t+ (R)$
24	22 23	syl	$⊢ R \in V \to dom R \subseteq dom t+ (R)$
25	21 24	eqssd	$⊢ R \in V \to dom t+ (R) = dom R$

Metamath Proof Explorer

Theorem dmtrclfv

Proof