Theorem brttrcl

Description: Characterization of elements of the transitive closure of a relation. (Contributed by Scott Fenton, 18-Aug-2024)

	Ref	Expression
Assertion	brttrcl	Could not format assertion : No typesetting found for |- ( A t++ R B <-> E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = A /\ ( f ` n ) = B ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		relttrcl	Could not format Rel t++ R : No typesetting found for |- Rel t++ R with typecode |-
2	1	brrelex12i	Could not format ( A t++ R B -> ( A e. _V /\ B e. _V ) ) : No typesetting found for |- ( A t++ R B -> ( A e. _V /\ B e. _V ) ) with typecode |-
3		fvex	$$⊢f\left(\varnothing \right)\in \mathrm{V}$$
4		eleq1	$$⊢f\left(\varnothing \right)=A\to \left(f\left(\varnothing \right)\in \mathrm{V}\leftrightarrow A\in \mathrm{V}\right)$$
5	3 4	mpbii	$$⊢f\left(\varnothing \right)=A\to A\in \mathrm{V}$$
6		fvex	$$⊢f\left(n\right)\in \mathrm{V}$$
7		eleq1	$$⊢f\left(n\right)=B\to \left(f\left(n\right)\in \mathrm{V}\leftrightarrow B\in \mathrm{V}\right)$$
8	6 7	mpbii	$$⊢f\left(n\right)=B\to B\in \mathrm{V}$$
9	5 8	anim12i	$$⊢\left(f\left(\varnothing \right)=A\wedge f\left(n\right)=B\right)\to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$
10	9	3ad2ant2	$$⊢\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=A\wedge f\left(n\right)=B\right)\wedge \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)\right)\to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$
11	10	exlimiv	$$⊢\exists f\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=A\wedge f\left(n\right)=B\right)\wedge \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)\right)\to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$
12	11	rexlimivw	$$⊢\exists n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\exists f\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=A\wedge f\left(n\right)=B\right)\wedge \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)\right)\to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$
13		eqeq2	$$⊢x=A\to \left(f\left(\varnothing \right)=x\leftrightarrow f\left(\varnothing \right)=A\right)$$
14	13	anbi1d	$$⊢x=A\to \left(\left(f\left(\varnothing \right)=x\wedge f\left(n\right)=y\right)\leftrightarrow \left(f\left(\varnothing \right)=A\wedge f\left(n\right)=y\right)\right)$$
15	14	3anbi2d	$$⊢x=A\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)\leftrightarrow \left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=A\wedge f\left(n\right)=y\right)\wedge \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)\right)\right)$$
16	15	exbidv	$$⊢x=A\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)\leftrightarrow \exists f\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=A\wedge f\left(n\right)=y\right)\wedge \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)\right)\right)$$
17	16	rexbidv	$$⊢x=A\to \left(\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)\leftrightarrow \exists n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\exists f\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=A\wedge f\left(n\right)=y\right)\wedge \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)\right)\right)$$
18		eqeq2	$$⊢y=B\to \left(f\left(n\right)=y\leftrightarrow f\left(n\right)=B\right)$$
19	18	anbi2d	$$⊢y=B\to \left(\left(f\left(\varnothing \right)=A\wedge f\left(n\right)=y\right)\leftrightarrow \left(f\left(\varnothing \right)=A\wedge f\left(n\right)=B\right)\right)$$
20	19	3anbi2d	$$⊢y=B\to \left(\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=A\wedge f\left(n\right)=y\right)\wedge \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)\right)\leftrightarrow \left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=A\wedge f\left(n\right)=B\right)\wedge \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)\right)\right)$$
21	20	exbidv	$$⊢y=B\to \left(\exists f\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=A\wedge f\left(n\right)=y\right)\wedge \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)\right)\leftrightarrow \exists f\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=A\wedge f\left(n\right)=B\right)\wedge \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)\right)\right)$$
22	21	rexbidv	$$⊢y=B\to \left(\exists n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\exists f\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=A\wedge f\left(n\right)=y\right)\wedge \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)\right)\leftrightarrow \exists n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\exists f\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=A\wedge f\left(n\right)=B\right)\wedge \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)\right)\right)$$
23		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 |-
24	17 22 23	brabg	Could not format ( ( A e. _V /\ B e. _V ) -> ( A t++ R B <-> E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = A /\ ( f ` n ) = B ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) ) ) : No typesetting found for |- ( ( A e. _V /\ B e. _V ) -> ( A t++ R B <-> E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = A /\ ( f ` n ) = B ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) ) ) with typecode |-
25	2 12 24	pm5.21nii	Could not format ( A t++ R B <-> E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = A /\ ( f ` n ) = B ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) ) : No typesetting found for |- ( A t++ R B <-> E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = A /\ ( f ` n ) = B ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) ) with typecode |-