Theorem 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	Could not format assertion : No typesetting found for |- dom t++ R = dom R with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-ttrcl	Could not format t++ R = { <. x , y >. | E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) } : No typesetting found for |- t++ R = { <. x , y >. | E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) } with typecode |-
2	1	dmeqi	Could not format dom t++ R = dom { <. x , y >. | E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) } : No typesetting found for |- dom t++ R = dom { <. x , y >. | E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) } with typecode |-
3		dmopab	$$⊢\mathrm{dom}\left\{⟨x,y⟩|\exists n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\exists f\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=x\wedge f\left(n\right)=y\right)\wedge \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)\right)\right\}=\left\{x|\exists y\exists n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\exists f\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=x\wedge f\left(n\right)=y\right)\wedge \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)\right)\right\}$$
4	2 3	eqtri	Could not format dom t++ R = { x | E. y E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) } : No typesetting found for |- dom t++ R = { x | E. y E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) } with typecode |-
5		simpr2l	$$⊢\left(n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\wedge \left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=x\wedge f\left(n\right)=y\right)\wedge \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)\right)\right)\to f\left(\varnothing \right)=x$$
6		fveq2	$$⊢a=\varnothing \to f\left(a\right)=f\left(\varnothing \right)$$
7		suceq	$$⊢a=\varnothing \to \mathrm{suc}a=\mathrm{suc}\varnothing$$
8		df-1o	$$⊢1_{𝑜}=\mathrm{suc}\varnothing$$
9	7 8	eqtr4di	$$⊢a=\varnothing \to \mathrm{suc}a=1_{𝑜}$$
10	9	fveq2d	$$⊢a=\varnothing \to f\left(\mathrm{suc}a\right)=f\left(1_{𝑜}\right)$$
11	6 10	breq12d	$$⊢a=\varnothing \to \left(f\left(a\right)Rf\left(\mathrm{suc}a\right)\leftrightarrow f\left(\varnothing \right)Rf\left(1_{𝑜}\right)\right)$$
12		simpr3	$$⊢\left(n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\wedge \left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=x\wedge f\left(n\right)=y\right)\wedge \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)\right)\right)\to \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)$$
13		eldif	$$⊢n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\leftrightarrow \left(n\in \mathrm{\omega }\wedge \neg n\in 1_{𝑜}\right)$$
14		0ex	$$⊢\varnothing \in \mathrm{V}$$
15		nnord	$$⊢n\in \mathrm{\omega }\to \mathrm{Ord}n$$
16		ordelsuc	$$⊢\left(\varnothing \in \mathrm{V}\wedge \mathrm{Ord}n\right)\to \left(\varnothing \in n\leftrightarrow \mathrm{suc}\varnothing \subseteq n\right)$$
17	14 15 16	sylancr	$$⊢n\in \mathrm{\omega }\to \left(\varnothing \in n\leftrightarrow \mathrm{suc}\varnothing \subseteq n\right)$$
18	8	sseq1i	$$⊢1_{𝑜}\subseteq n\leftrightarrow \mathrm{suc}\varnothing \subseteq n$$
19		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
20	19	onordi	$$⊢\mathrm{Ord}{1}_{𝑜}$$
21		ordtri1	$$⊢\left(\mathrm{Ord}{1}_{𝑜}\wedge \mathrm{Ord}n\right)\to \left(1_{𝑜}\subseteq n\leftrightarrow \neg n\in 1_{𝑜}\right)$$
22	20 15 21	sylancr	$$⊢n\in \mathrm{\omega }\to \left(1_{𝑜}\subseteq n\leftrightarrow \neg n\in 1_{𝑜}\right)$$
23	18 22	bitr3id	$$⊢n\in \mathrm{\omega }\to \left(\mathrm{suc}\varnothing \subseteq n\leftrightarrow \neg n\in 1_{𝑜}\right)$$
24	17 23	bitr2d	$$⊢n\in \mathrm{\omega }\to \left(\neg n\in 1_{𝑜}\leftrightarrow \varnothing \in n\right)$$
25	24	biimpa	$$⊢\left(n\in \mathrm{\omega }\wedge \neg n\in 1_{𝑜}\right)\to \varnothing \in n$$
26	13 25	sylbi	$$⊢n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\to \varnothing \in n$$
27	26	adantr	$$⊢\left(n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\wedge \left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=x\wedge f\left(n\right)=y\right)\wedge \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)\right)\right)\to \varnothing \in n$$
28	11 12 27	rspcdva	$$⊢\left(n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\wedge \left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=x\wedge f\left(n\right)=y\right)\wedge \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)\right)\right)\to f\left(\varnothing \right)Rf\left(1_{𝑜}\right)$$
29	5 28	eqbrtrrd	$$⊢\left(n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\wedge \left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=x\wedge f\left(n\right)=y\right)\wedge \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)\right)\right)\to xRf\left(1_{𝑜}\right)$$
30		vex	$$⊢x\in \mathrm{V}$$
31		fvex	$$⊢f\left(1_{𝑜}\right)\in \mathrm{V}$$
32	30 31	breldm	$$⊢xRf\left(1_{𝑜}\right)\to x\in \mathrm{dom}R$$
33	29 32	syl	$$⊢\left(n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\wedge \left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=x\wedge f\left(n\right)=y\right)\wedge \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)\right)\right)\to x\in \mathrm{dom}R$$
34	33	ex	$$⊢n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\to \left(\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=x\wedge f\left(n\right)=y\right)\wedge \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)\right)\to x\in \mathrm{dom}R\right)$$
35	34	exlimdv	$$⊢n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\to \left(\exists f\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=x\wedge f\left(n\right)=y\right)\wedge \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)\right)\to x\in \mathrm{dom}R\right)$$
36	35	rexlimiv	$$⊢\exists n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\exists f\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=x\wedge f\left(n\right)=y\right)\wedge \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)\right)\to x\in \mathrm{dom}R$$
37	36	exlimiv	$$⊢\exists y\exists n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\exists f\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=x\wedge f\left(n\right)=y\right)\wedge \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)\right)\to x\in \mathrm{dom}R$$
38	37	abssi	$$⊢\left\{x|\exists y\exists n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\exists f\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=x\wedge f\left(n\right)=y\right)\wedge \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)\right)\right\}\subseteq \mathrm{dom}R$$
39	4 38	eqsstri	Could not format dom t++ R C_ dom R : No typesetting found for |- dom t++ R C_ dom R with typecode |-
40		dmresv	$$⊢\mathrm{dom}\left({R\upharpoonright }_{\mathrm{V}}\right)=\mathrm{dom}R$$
41		relres	$$⊢\mathrm{Rel}\left({R\upharpoonright }_{\mathrm{V}}\right)$$
42		ssttrcl	Could not format ( Rel ( R |` _V ) -> ( R |` _V ) C_ t++ ( R |` _V ) ) : No typesetting found for |- ( Rel ( R |` _V ) -> ( R |` _V ) C_ t++ ( R |` _V ) ) with typecode |-
43	41 42	ax-mp	Could not format ( R |` _V ) C_ t++ ( R |` _V ) : No typesetting found for |- ( R |` _V ) C_ t++ ( R |` _V ) with typecode |-
44		ttrclresv	Could not format t++ ( R |` _V ) = t++ R : No typesetting found for |- t++ ( R |` _V ) = t++ R with typecode |-
45	43 44	sseqtri	Could not format ( R |` _V ) C_ t++ R : No typesetting found for |- ( R |` _V ) C_ t++ R with typecode |-
46		dmss	Could not format ( ( R |` _V ) C_ t++ R -> dom ( R |` _V ) C_ dom t++ R ) : No typesetting found for |- ( ( R |` _V ) C_ t++ R -> dom ( R |` _V ) C_ dom t++ R ) with typecode |-
47	45 46	ax-mp	Could not format dom ( R |` _V ) C_ dom t++ R : No typesetting found for |- dom ( R |` _V ) C_ dom t++ R with typecode |-
48	40 47	eqsstrri	Could not format dom R C_ dom t++ R : No typesetting found for |- dom R C_ dom t++ R with typecode |-
49	39 48	eqssi	Could not format dom t++ R = dom R : No typesetting found for |- dom t++ R = dom R with typecode |-