Theorem dfttrcl2

Description: When R is a set and a relationship, then its transitive closure can be defined by an intersection. (Contributed by Scott Fenton, 26-Oct-2024)

	Ref	Expression
Assertion	dfttrcl2	Could not format assertion : No typesetting found for |- ( ( R e. V /\ Rel R ) -> t++ R = |^| { z | ( R C_ z /\ ( z o. z ) C_ z ) } ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		ssintab	Could not format ( t++ R C_ |^| { z | ( R C_ z /\ ( z o. z ) C_ z ) } <-> A. z ( ( R C_ z /\ ( z o. z ) C_ z ) -> t++ R C_ z ) ) : No typesetting found for |- ( t++ R C_ |^| { z | ( R C_ z /\ ( z o. z ) C_ z ) } <-> A. z ( ( R C_ z /\ ( z o. z ) C_ z ) -> t++ R C_ z ) ) with typecode |-
2		ttrclss	Could not format ( ( R C_ z /\ ( z o. z ) C_ z ) -> t++ R C_ z ) : No typesetting found for |- ( ( R C_ z /\ ( z o. z ) C_ z ) -> t++ R C_ z ) with typecode |-
3	1 2	mpgbir	Could not format t++ R C_ |^| { z | ( R C_ z /\ ( z o. z ) C_ z ) } : No typesetting found for |- t++ R C_ |^| { z | ( R C_ z /\ ( z o. z ) C_ z ) } with typecode |-
4	3	a1i	Could not format ( ( R e. V /\ Rel R ) -> t++ R C_ |^| { z | ( R C_ z /\ ( z o. z ) C_ z ) } ) : No typesetting found for |- ( ( R e. V /\ Rel R ) -> t++ R C_ |^| { z | ( R C_ z /\ ( z o. z ) C_ z ) } ) with typecode |-
5		rabab	$$⊢\left\{z\in \mathrm{V}|\left(R\subseteq z\wedge z\circ z\subseteq z\right)\right\}=\left\{z|\left(R\subseteq z\wedge z\circ z\subseteq z\right)\right\}$$
6	5	inteqi	$$⊢\bigcap \left\{z\in \mathrm{V}|\left(R\subseteq z\wedge z\circ z\subseteq z\right)\right\}=\bigcap \left\{z|\left(R\subseteq z\wedge z\circ z\subseteq z\right)\right\}$$
7		ttrclexg	Could not format ( R e. V -> t++ R e. _V ) : No typesetting found for |- ( R e. V -> t++ R e. _V ) with typecode |-
8		ssttrcl	Could not format ( Rel R -> R C_ t++ R ) : No typesetting found for |- ( Rel R -> R C_ t++ R ) with typecode |-
9		ttrcltr	Could not format ( t++ R o. t++ R ) C_ t++ R : No typesetting found for |- ( t++ R o. t++ R ) C_ t++ R with typecode |-
10	8 9	jctir	Could not format ( Rel R -> ( R C_ t++ R /\ ( t++ R o. t++ R ) C_ t++ R ) ) : No typesetting found for |- ( Rel R -> ( R C_ t++ R /\ ( t++ R o. t++ R ) C_ t++ R ) ) with typecode |-
11		sseq2	Could not format ( z = t++ R -> ( R C_ z <-> R C_ t++ R ) ) : No typesetting found for |- ( z = t++ R -> ( R C_ z <-> R C_ t++ R ) ) with typecode |-
12		coeq1	Could not format ( z = t++ R -> ( z o. z ) = ( t++ R o. z ) ) : No typesetting found for |- ( z = t++ R -> ( z o. z ) = ( t++ R o. z ) ) with typecode |-
13		coeq2	Could not format ( z = t++ R -> ( t++ R o. z ) = ( t++ R o. t++ R ) ) : No typesetting found for |- ( z = t++ R -> ( t++ R o. z ) = ( t++ R o. t++ R ) ) with typecode |-
14	12 13	eqtrd	Could not format ( z = t++ R -> ( z o. z ) = ( t++ R o. t++ R ) ) : No typesetting found for |- ( z = t++ R -> ( z o. z ) = ( t++ R o. t++ R ) ) with typecode |-
15		id	Could not format ( z = t++ R -> z = t++ R ) : No typesetting found for |- ( z = t++ R -> z = t++ R ) with typecode |-
16	14 15	sseq12d	Could not format ( z = t++ R -> ( ( z o. z ) C_ z <-> ( t++ R o. t++ R ) C_ t++ R ) ) : No typesetting found for |- ( z = t++ R -> ( ( z o. z ) C_ z <-> ( t++ R o. t++ R ) C_ t++ R ) ) with typecode |-
17	11 16	anbi12d	Could not format ( z = t++ R -> ( ( R C_ z /\ ( z o. z ) C_ z ) <-> ( R C_ t++ R /\ ( t++ R o. t++ R ) C_ t++ R ) ) ) : No typesetting found for |- ( z = t++ R -> ( ( R C_ z /\ ( z o. z ) C_ z ) <-> ( R C_ t++ R /\ ( t++ R o. t++ R ) C_ t++ R ) ) ) with typecode |-
18	17	intminss	Could not format ( ( t++ R e. _V /\ ( R C_ t++ R /\ ( t++ R o. t++ R ) C_ t++ R ) ) -> |^| { z e. _V | ( R C_ z /\ ( z o. z ) C_ z ) } C_ t++ R ) : No typesetting found for |- ( ( t++ R e. _V /\ ( R C_ t++ R /\ ( t++ R o. t++ R ) C_ t++ R ) ) -> |^| { z e. _V | ( R C_ z /\ ( z o. z ) C_ z ) } C_ t++ R ) with typecode |-
19	7 10 18	syl2an	Could not format ( ( R e. V /\ Rel R ) -> |^| { z e. _V | ( R C_ z /\ ( z o. z ) C_ z ) } C_ t++ R ) : No typesetting found for |- ( ( R e. V /\ Rel R ) -> |^| { z e. _V | ( R C_ z /\ ( z o. z ) C_ z ) } C_ t++ R ) with typecode |-
20	6 19	eqsstrrid	Could not format ( ( R e. V /\ Rel R ) -> |^| { z | ( R C_ z /\ ( z o. z ) C_ z ) } C_ t++ R ) : No typesetting found for |- ( ( R e. V /\ Rel R ) -> |^| { z | ( R C_ z /\ ( z o. z ) C_ z ) } C_ t++ R ) with typecode |-
21	4 20	eqssd	Could not format ( ( R e. V /\ Rel R ) -> t++ R = |^| { z | ( R C_ z /\ ( z o. z ) C_ z ) } ) : No typesetting found for |- ( ( R e. V /\ Rel R ) -> t++ R = |^| { z | ( R C_ z /\ ( z o. z ) C_ z ) } ) with typecode |-