Theorem ttrclse

Description: If R is set-like over A , then the transitive closure of the restriction of R to A is set-like over A .

This theorem requires the axioms of infinity and replacement for its proof. (Contributed by Scott Fenton, 31-Oct-2024)

	Ref	Expression
Assertion	ttrclse	Could not format assertion : No typesetting found for |- ( R Se A -> t++ ( R |` A ) Se A ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		brttrcl2	Could not format ( y t++ ( R |` A ) x <-> E. n e. _om E. f ( f Fn suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc n ) = x ) /\ A. a e. suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) ) : No typesetting found for |- ( y t++ ( R |` A ) x <-> E. n e. _om E. f ( f Fn suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc n ) = x ) /\ A. a e. suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) ) with typecode |-
2		eqid	$$⊢\mathrm{rec}\left(\left(b\in \mathrm{V}⟼\bigcup _{w\in b}Pred\left(R,A,w\right)\right),Pred\left(R,A,x\right)\right)=\mathrm{rec}\left(\left(b\in \mathrm{V}⟼\bigcup _{w\in b}Pred\left(R,A,w\right)\right),Pred\left(R,A,x\right)\right)$$
3	2	ttrclselem2	$$⊢\left(n\in \mathrm{\omega }\wedge R\mathrm{Se}A\wedge x\in A\right)\to \left(\exists f\left(fFn\mathrm{suc}\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=y\wedge f\left(\mathrm{suc}n\right)=x\right)\wedge \forall a\in \mathrm{suc}nf\left(a\right)\left({R\upharpoonright }_A\right)f\left(\mathrm{suc}a\right)\right)\leftrightarrow y\in \mathrm{rec}\left(\left(b\in \mathrm{V}⟼\bigcup _{w\in b}Pred\left(R,A,w\right)\right),Pred\left(R,A,x\right)\right)\left(n\right)\right)$$
4	3	3expb	$$⊢\left(n\in \mathrm{\omega }\wedge \left(R\mathrm{Se}A\wedge x\in A\right)\right)\to \left(\exists f\left(fFn\mathrm{suc}\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=y\wedge f\left(\mathrm{suc}n\right)=x\right)\wedge \forall a\in \mathrm{suc}nf\left(a\right)\left({R\upharpoonright }_A\right)f\left(\mathrm{suc}a\right)\right)\leftrightarrow y\in \mathrm{rec}\left(\left(b\in \mathrm{V}⟼\bigcup _{w\in b}Pred\left(R,A,w\right)\right),Pred\left(R,A,x\right)\right)\left(n\right)\right)$$
5	4	ancoms	$$⊢\left(\left(R\mathrm{Se}A\wedge x\in A\right)\wedge n\in \mathrm{\omega }\right)\to \left(\exists f\left(fFn\mathrm{suc}\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=y\wedge f\left(\mathrm{suc}n\right)=x\right)\wedge \forall a\in \mathrm{suc}nf\left(a\right)\left({R\upharpoonright }_A\right)f\left(\mathrm{suc}a\right)\right)\leftrightarrow y\in \mathrm{rec}\left(\left(b\in \mathrm{V}⟼\bigcup _{w\in b}Pred\left(R,A,w\right)\right),Pred\left(R,A,x\right)\right)\left(n\right)\right)$$
6	5	rexbidva	$$⊢\left(R\mathrm{Se}A\wedge x\in A\right)\to \left(\exists n\in \mathrm{\omega }\exists f\left(fFn\mathrm{suc}\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=y\wedge f\left(\mathrm{suc}n\right)=x\right)\wedge \forall a\in \mathrm{suc}nf\left(a\right)\left({R\upharpoonright }_A\right)f\left(\mathrm{suc}a\right)\right)\leftrightarrow \exists n\in \mathrm{\omega }y\in \mathrm{rec}\left(\left(b\in \mathrm{V}⟼\bigcup _{w\in b}Pred\left(R,A,w\right)\right),Pred\left(R,A,x\right)\right)\left(n\right)\right)$$
7	1 6	bitrid	Could not format ( ( R Se A /\ x e. A ) -> ( y t++ ( R |` A ) x <-> E. n e. _om y e. ( rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , x ) ) ` n ) ) ) : No typesetting found for |- ( ( R Se A /\ x e. A ) -> ( y t++ ( R |` A ) x <-> E. n e. _om y e. ( rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , x ) ) ` n ) ) ) with typecode |-
8		vex	$$⊢y\in \mathrm{V}$$
9	8	elpred	Could not format ( x e. _V -> ( y e. Pred ( t++ ( R |` A ) , A , x ) <-> ( y e. A /\ y t++ ( R |` A ) x ) ) ) : No typesetting found for |- ( x e. _V -> ( y e. Pred ( t++ ( R |` A ) , A , x ) <-> ( y e. A /\ y t++ ( R |` A ) x ) ) ) with typecode |-
10	9	elv	Could not format ( y e. Pred ( t++ ( R |` A ) , A , x ) <-> ( y e. A /\ y t++ ( R |` A ) x ) ) : No typesetting found for |- ( y e. Pred ( t++ ( R |` A ) , A , x ) <-> ( y e. A /\ y t++ ( R |` A ) x ) ) with typecode |-
11		resdmss	$$⊢\mathrm{dom}\left({R\upharpoonright }_A\right)\subseteq A$$
12		vex	$$⊢x\in \mathrm{V}$$
13	8 12	breldm	Could not format ( y t++ ( R |` A ) x -> y e. dom t++ ( R |` A ) ) : No typesetting found for |- ( y t++ ( R |` A ) x -> y e. dom t++ ( R |` A ) ) with typecode |-
14		dmttrcl	Could not format dom t++ ( R |` A ) = dom ( R |` A ) : No typesetting found for |- dom t++ ( R |` A ) = dom ( R |` A ) with typecode |-
15	13 14	eleqtrdi	Could not format ( y t++ ( R |` A ) x -> y e. dom ( R |` A ) ) : No typesetting found for |- ( y t++ ( R |` A ) x -> y e. dom ( R |` A ) ) with typecode |-
16	11 15	sselid	Could not format ( y t++ ( R |` A ) x -> y e. A ) : No typesetting found for |- ( y t++ ( R |` A ) x -> y e. A ) with typecode |-
17	16	pm4.71ri	Could not format ( y t++ ( R |` A ) x <-> ( y e. A /\ y t++ ( R |` A ) x ) ) : No typesetting found for |- ( y t++ ( R |` A ) x <-> ( y e. A /\ y t++ ( R |` A ) x ) ) with typecode |-
18	10 17	bitr4i	Could not format ( y e. Pred ( t++ ( R |` A ) , A , x ) <-> y t++ ( R |` A ) x ) : No typesetting found for |- ( y e. Pred ( t++ ( R |` A ) , A , x ) <-> y t++ ( R |` A ) x ) with typecode |-
19		rdgfun	$$⊢\mathrm{Fun}\mathrm{rec}\left(\left(b\in \mathrm{V}⟼\bigcup _{w\in b}Pred\left(R,A,w\right)\right),Pred\left(R,A,x\right)\right)$$
20		eluniima	$$⊢\mathrm{Fun}\mathrm{rec}\left(\left(b\in \mathrm{V}⟼\bigcup _{w\in b}Pred\left(R,A,w\right)\right),Pred\left(R,A,x\right)\right)\to \left(y\in \bigcup \mathrm{rec}\left(\left(b\in \mathrm{V}⟼\bigcup _{w\in b}Pred\left(R,A,w\right)\right),Pred\left(R,A,x\right)\right)\left[\mathrm{\omega }\right]\leftrightarrow \exists n\in \mathrm{\omega }y\in \mathrm{rec}\left(\left(b\in \mathrm{V}⟼\bigcup _{w\in b}Pred\left(R,A,w\right)\right),Pred\left(R,A,x\right)\right)\left(n\right)\right)$$
21	19 20	ax-mp	$$⊢y\in \bigcup \mathrm{rec}\left(\left(b\in \mathrm{V}⟼\bigcup _{w\in b}Pred\left(R,A,w\right)\right),Pred\left(R,A,x\right)\right)\left[\mathrm{\omega }\right]\leftrightarrow \exists n\in \mathrm{\omega }y\in \mathrm{rec}\left(\left(b\in \mathrm{V}⟼\bigcup _{w\in b}Pred\left(R,A,w\right)\right),Pred\left(R,A,x\right)\right)\left(n\right)$$
22	7 18 21	3bitr4g	Could not format ( ( R Se A /\ x e. A ) -> ( y e. Pred ( t++ ( R |` A ) , A , x ) <-> y e. U. ( rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , x ) ) " _om ) ) ) : No typesetting found for |- ( ( R Se A /\ x e. A ) -> ( y e. Pred ( t++ ( R |` A ) , A , x ) <-> y e. U. ( rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , x ) ) " _om ) ) ) with typecode |-
23	22	eqrdv	Could not format ( ( R Se A /\ x e. A ) -> Pred ( t++ ( R |` A ) , A , x ) = U. ( rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , x ) ) " _om ) ) : No typesetting found for |- ( ( R Se A /\ x e. A ) -> Pred ( t++ ( R |` A ) , A , x ) = U. ( rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , x ) ) " _om ) ) with typecode |-
24		omex	$$⊢\mathrm{\omega }\in \mathrm{V}$$
25	24	funimaex	$$⊢\mathrm{Fun}\mathrm{rec}\left(\left(b\in \mathrm{V}⟼\bigcup _{w\in b}Pred\left(R,A,w\right)\right),Pred\left(R,A,x\right)\right)\to \mathrm{rec}\left(\left(b\in \mathrm{V}⟼\bigcup _{w\in b}Pred\left(R,A,w\right)\right),Pred\left(R,A,x\right)\right)\left[\mathrm{\omega }\right]\in \mathrm{V}$$
26	19 25	ax-mp	$$⊢\mathrm{rec}\left(\left(b\in \mathrm{V}⟼\bigcup _{w\in b}Pred\left(R,A,w\right)\right),Pred\left(R,A,x\right)\right)\left[\mathrm{\omega }\right]\in \mathrm{V}$$
27	26	uniex	$$⊢\bigcup \mathrm{rec}\left(\left(b\in \mathrm{V}⟼\bigcup _{w\in b}Pred\left(R,A,w\right)\right),Pred\left(R,A,x\right)\right)\left[\mathrm{\omega }\right]\in \mathrm{V}$$
28	23 27	eqeltrdi	Could not format ( ( R Se A /\ x e. A ) -> Pred ( t++ ( R |` A ) , A , x ) e. _V ) : No typesetting found for |- ( ( R Se A /\ x e. A ) -> Pred ( t++ ( R |` A ) , A , x ) e. _V ) with typecode |-
29	28	ralrimiva	Could not format ( R Se A -> A. x e. A Pred ( t++ ( R |` A ) , A , x ) e. _V ) : No typesetting found for |- ( R Se A -> A. x e. A Pred ( t++ ( R |` A ) , A , x ) e. _V ) with typecode |-
30		dfse3	Could not format ( t++ ( R |` A ) Se A <-> A. x e. A Pred ( t++ ( R |` A ) , A , x ) e. _V ) : No typesetting found for |- ( t++ ( R |` A ) Se A <-> A. x e. A Pred ( t++ ( R |` A ) , A , x ) e. _V ) with typecode |-
31	29 30	sylibr	Could not format ( R Se A -> t++ ( R |` A ) Se A ) : No typesetting found for |- ( R Se A -> t++ ( R |` A ) Se A ) with typecode |-