dmttrcl

Description: The domain of a transitive closure is the same as the domain of the original class. (Contributed by Scott Fenton, 26-Oct-2024)

		Ref	Expression
	Assertion	dmttrcl	$⊢ dom t++ R = dom R$

Proof

Step	Hyp	Ref	Expression
1		df-ttrcl	$⊢ t++ R = \{⟨x, y⟩ \| \exists n \in (ω ∖ 1_{𝑜}) \exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall a \in n f (a) R f (suc a))\}$
2	1	dmeqi	$⊢ dom t++ R = dom \{⟨x, y⟩ \| \exists n \in (ω ∖ 1_{𝑜}) \exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall a \in n f (a) R f (suc a))\}$
3		dmopab	$⊢ dom \{⟨x, y⟩ \| \exists n \in (ω ∖ 1_{𝑜}) \exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall a \in n f (a) R f (suc a))\} = \{x \| \exists y \exists n \in (ω ∖ 1_{𝑜}) \exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall a \in n f (a) R f (suc a))\}$
4	2 3	eqtri	$⊢ dom t++ R = \{x \| \exists y \exists n \in (ω ∖ 1_{𝑜}) \exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall a \in n f (a) R f (suc a))\}$
5		simpr2l	$⊢ (n \in (ω ∖ 1_{𝑜}) \land (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall a \in n f (a) R f (suc a))) \to f (\emptyset) = x$
6		fveq2	$⊢ a = \emptyset \to f (a) = f (\emptyset)$
7		suceq	$⊢ a = \emptyset \to suc a = suc \emptyset$
8		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
9	7 8	eqtr4di	$⊢ a = \emptyset \to suc a = 1_{𝑜}$
10	9	fveq2d	$⊢ a = \emptyset \to f (suc a) = f (1_{𝑜})$
11	6 10	breq12d	$⊢ a = \emptyset \to (f (a) R f (suc a) \leftrightarrow f (\emptyset) R f (1_{𝑜}))$
12		simpr3	$⊢ (n \in (ω ∖ 1_{𝑜}) \land (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall a \in n f (a) R f (suc a))) \to \forall a \in n f (a) R f (suc a)$
13		eldif	$⊢ n \in (ω ∖ 1_{𝑜}) \leftrightarrow (n \in ω \land \neg n \in 1_{𝑜})$
14		0ex	$⊢ \emptyset \in V$
15		nnord	$⊢ n \in ω \to Ord n$
16		ordelsuc	$⊢ (\emptyset \in V \land Ord n) \to (\emptyset \in n \leftrightarrow suc \emptyset \subseteq n)$
17	14 15 16	sylancr	$⊢ n \in ω \to (\emptyset \in n \leftrightarrow suc \emptyset \subseteq n)$
18	8	sseq1i	$⊢ 1_{𝑜} \subseteq n \leftrightarrow suc \emptyset \subseteq n$
19		1on	$⊢ 1_{𝑜} \in On$
20	19	onordi	$⊢ Ord 1_{𝑜}$
21		ordtri1	$⊢ (Ord 1_{𝑜} \land Ord n) \to (1_{𝑜} \subseteq n \leftrightarrow \neg n \in 1_{𝑜})$
22	20 15 21	sylancr	$⊢ n \in ω \to (1_{𝑜} \subseteq n \leftrightarrow \neg n \in 1_{𝑜})$
23	18 22	bitr3id	$⊢ n \in ω \to (suc \emptyset \subseteq n \leftrightarrow \neg n \in 1_{𝑜})$
24	17 23	bitr2d	$⊢ n \in ω \to (\neg n \in 1_{𝑜} \leftrightarrow \emptyset \in n)$
25	24	biimpa	$⊢ (n \in ω \land \neg n \in 1_{𝑜}) \to \emptyset \in n$
26	13 25	sylbi	$⊢ n \in (ω ∖ 1_{𝑜}) \to \emptyset \in n$
27	26	adantr	$⊢ (n \in (ω ∖ 1_{𝑜}) \land (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall a \in n f (a) R f (suc a))) \to \emptyset \in n$
28	11 12 27	rspcdva	$⊢ (n \in (ω ∖ 1_{𝑜}) \land (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall a \in n f (a) R f (suc a))) \to f (\emptyset) R f (1_{𝑜})$
29	5 28	eqbrtrrd	$⊢ (n \in (ω ∖ 1_{𝑜}) \land (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall a \in n f (a) R f (suc a))) \to x R f (1_{𝑜})$
30		vex	$⊢ x \in V$
31		fvex	$⊢ f (1_{𝑜}) \in V$
32	30 31	breldm	$⊢ x R f (1_{𝑜}) \to x \in dom R$
33	29 32	syl	$⊢ (n \in (ω ∖ 1_{𝑜}) \land (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall a \in n f (a) R f (suc a))) \to x \in dom R$
34	33	ex	$⊢ n \in (ω ∖ 1_{𝑜}) \to ((f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall a \in n f (a) R f (suc a)) \to x \in dom R)$
35	34	exlimdv	$⊢ n \in (ω ∖ 1_{𝑜}) \to (\exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall a \in n f (a) R f (suc a)) \to x \in dom R)$
36	35	rexlimiv	$⊢ \exists n \in (ω ∖ 1_{𝑜}) \exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall a \in n f (a) R f (suc a)) \to x \in dom R$
37	36	exlimiv	$⊢ \exists y \exists n \in (ω ∖ 1_{𝑜}) \exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall a \in n f (a) R f (suc a)) \to x \in dom R$
38	37	abssi	$⊢ \{x \| \exists y \exists n \in (ω ∖ 1_{𝑜}) \exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall a \in n f (a) R f (suc a))\} \subseteq dom R$
39	4 38	eqsstri	$⊢ dom t++ R \subseteq dom R$
40		dmresv	$⊢ dom ({R ↾}_{V}) = dom R$
41		relres	$⊢ Rel ({R ↾}_{V})$
42		ssttrcl	$⊢ Rel ({R ↾}_{V}) \to {R ↾}_{V} \subseteq t++ ({R ↾}_{V})$
43	41 42	ax-mp	$⊢ {R ↾}_{V} \subseteq t++ ({R ↾}_{V})$
44		ttrclresv	$⊢ t++ ({R ↾}_{V}) = t++ R$
45	43 44	sseqtri	$⊢ {R ↾}_{V} \subseteq t++ R$
46		dmss	$⊢ {R ↾}_{V} \subseteq t++ R \to dom ({R ↾}_{V}) \subseteq dom t++ R$
47	45 46	ax-mp	$⊢ dom ({R ↾}_{V}) \subseteq dom t++ R$
48	40 47	eqsstrri	$⊢ dom R \subseteq dom t++ R$
49	39 48	eqssi	$⊢ dom t++ R = dom R$

Metamath Proof Explorer

Theorem dmttrcl

Proof