Theorem dfttc4

Description: An alternative expression for the transitive closure of a class, assuming Regularity. A set x is contained in the transitive closure of A iff we can construct an e. -chain from x to an element of A . This weak definition is primarily useful for proving elttcirr . (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Assertion	dfttc4	Could not format assertion : No typesetting found for |- TC+ A = { x | E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) } with typecode |-

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\left\{x|\exists y\left(A\cap y\ne \varnothing \wedge \forall z\in y\left(z\cap y=\varnothing \to z=x\right)\right)\right\}=\left\{x|\exists y\left(A\cap y\ne \varnothing \wedge \forall z\in y\left(z\cap y=\varnothing \to z=x\right)\right)\right\}$$
2	1	dfttc4lem2	$$⊢\left(A\subseteq \left\{x|\exists y\left(A\cap y\ne \varnothing \wedge \forall z\in y\left(z\cap y=\varnothing \to z=x\right)\right)\right\}\wedge \mathrm{Tr}\left\{x|\exists y\left(A\cap y\ne \varnothing \wedge \forall z\in y\left(z\cap y=\varnothing \to z=x\right)\right)\right\}\right)$$
3		ttcmin	Could not format ( ( A C_ { x | E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) } /\ Tr { x | E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) } ) -> TC+ A C_ { x | E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) } ) : No typesetting found for |- ( ( A C_ { x | E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) } /\ Tr { x | E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) } ) -> TC+ A C_ { x | E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) } ) with typecode |-
4	2 3	ax-mp	Could not format TC+ A C_ { x | E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) } : No typesetting found for |- TC+ A C_ { x | E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) } with typecode |-
5		vex	$$⊢w\in \mathrm{V}$$
6		equequ2	$$⊢x=w\to \left(z=x\leftrightarrow z=w\right)$$
7	6	imbi2d	$$⊢x=w\to \left(\left(z\cap y=\varnothing \to z=x\right)\leftrightarrow \left(z\cap y=\varnothing \to z=w\right)\right)$$
8	7	ralbidv	$$⊢x=w\to \left(\forall z\in y\left(z\cap y=\varnothing \to z=x\right)\leftrightarrow \forall z\in y\left(z\cap y=\varnothing \to z=w\right)\right)$$
9	8	anbi2d	$$⊢x=w\to \left(\left(A\cap y\ne \varnothing \wedge \forall z\in y\left(z\cap y=\varnothing \to z=x\right)\right)\leftrightarrow \left(A\cap y\ne \varnothing \wedge \forall z\in y\left(z\cap y=\varnothing \to z=w\right)\right)\right)$$
10	9	exbidv	$$⊢x=w\to \left(\exists y\left(A\cap y\ne \varnothing \wedge \forall z\in y\left(z\cap y=\varnothing \to z=x\right)\right)\leftrightarrow \exists y\left(A\cap y\ne \varnothing \wedge \forall z\in y\left(z\cap y=\varnothing \to z=w\right)\right)\right)$$
11	5 10	elab	$$⊢w\in \left\{x|\exists y\left(A\cap y\ne \varnothing \wedge \forall z\in y\left(z\cap y=\varnothing \to z=x\right)\right)\right\}\leftrightarrow \exists y\left(A\cap y\ne \varnothing \wedge \forall z\in y\left(z\cap y=\varnothing \to z=w\right)\right)$$
12		vex	$$⊢y\in \mathrm{V}$$
13	12	inex2	Could not format ( TC+ A i^i y ) e. _V : No typesetting found for |- ( TC+ A i^i y ) e. _V with typecode |-
14		ttcid	Could not format A C_ TC+ A : No typesetting found for |- A C_ TC+ A with typecode |-
15		ssrin	Could not format ( A C_ TC+ A -> ( A i^i y ) C_ ( TC+ A i^i y ) ) : No typesetting found for |- ( A C_ TC+ A -> ( A i^i y ) C_ ( TC+ A i^i y ) ) with typecode |-
16	14 15	ax-mp	Could not format ( A i^i y ) C_ ( TC+ A i^i y ) : No typesetting found for |- ( A i^i y ) C_ ( TC+ A i^i y ) with typecode |-
17		ssn0	Could not format ( ( ( A i^i y ) C_ ( TC+ A i^i y ) /\ ( A i^i y ) =/= (/) ) -> ( TC+ A i^i y ) =/= (/) ) : No typesetting found for |- ( ( ( A i^i y ) C_ ( TC+ A i^i y ) /\ ( A i^i y ) =/= (/) ) -> ( TC+ A i^i y ) =/= (/) ) with typecode |-
18	16 17	mpan	Could not format ( ( A i^i y ) =/= (/) -> ( TC+ A i^i y ) =/= (/) ) : No typesetting found for |- ( ( A i^i y ) =/= (/) -> ( TC+ A i^i y ) =/= (/) ) with typecode |-
19		zfreg	Could not format ( ( ( TC+ A i^i y ) e. _V /\ ( TC+ A i^i y ) =/= (/) ) -> E. x e. ( TC+ A i^i y ) ( x i^i ( TC+ A i^i y ) ) = (/) ) : No typesetting found for |- ( ( ( TC+ A i^i y ) e. _V /\ ( TC+ A i^i y ) =/= (/) ) -> E. x e. ( TC+ A i^i y ) ( x i^i ( TC+ A i^i y ) ) = (/) ) with typecode |-
20	13 18 19	sylancr	Could not format ( ( A i^i y ) =/= (/) -> E. x e. ( TC+ A i^i y ) ( x i^i ( TC+ A i^i y ) ) = (/) ) : No typesetting found for |- ( ( A i^i y ) =/= (/) -> E. x e. ( TC+ A i^i y ) ( x i^i ( TC+ A i^i y ) ) = (/) ) with typecode |-
21		simpl	Could not format ( ( x e. ( TC+ A i^i y ) /\ ( x i^i ( TC+ A i^i y ) ) = (/) ) -> x e. ( TC+ A i^i y ) ) : No typesetting found for |- ( ( x e. ( TC+ A i^i y ) /\ ( x i^i ( TC+ A i^i y ) ) = (/) ) -> x e. ( TC+ A i^i y ) ) with typecode |-
22	21	elin2d	Could not format ( ( x e. ( TC+ A i^i y ) /\ ( x i^i ( TC+ A i^i y ) ) = (/) ) -> x e. y ) : No typesetting found for |- ( ( x e. ( TC+ A i^i y ) /\ ( x i^i ( TC+ A i^i y ) ) = (/) ) -> x e. y ) with typecode |-
23		inass	Could not format ( ( x i^i TC+ A ) i^i y ) = ( x i^i ( TC+ A i^i y ) ) : No typesetting found for |- ( ( x i^i TC+ A ) i^i y ) = ( x i^i ( TC+ A i^i y ) ) with typecode |-
24		elinel1	Could not format ( x e. ( TC+ A i^i y ) -> x e. TC+ A ) : No typesetting found for |- ( x e. ( TC+ A i^i y ) -> x e. TC+ A ) with typecode |-
25		ttctr2	Could not format ( x e. TC+ A -> x C_ TC+ A ) : No typesetting found for |- ( x e. TC+ A -> x C_ TC+ A ) with typecode |-
26	24 25	syl	Could not format ( x e. ( TC+ A i^i y ) -> x C_ TC+ A ) : No typesetting found for |- ( x e. ( TC+ A i^i y ) -> x C_ TC+ A ) with typecode |-
27		dfss2	Could not format ( x C_ TC+ A <-> ( x i^i TC+ A ) = x ) : No typesetting found for |- ( x C_ TC+ A <-> ( x i^i TC+ A ) = x ) with typecode |-
28	26 27	sylib	Could not format ( x e. ( TC+ A i^i y ) -> ( x i^i TC+ A ) = x ) : No typesetting found for |- ( x e. ( TC+ A i^i y ) -> ( x i^i TC+ A ) = x ) with typecode |-
29	28	ineq1d	Could not format ( x e. ( TC+ A i^i y ) -> ( ( x i^i TC+ A ) i^i y ) = ( x i^i y ) ) : No typesetting found for |- ( x e. ( TC+ A i^i y ) -> ( ( x i^i TC+ A ) i^i y ) = ( x i^i y ) ) with typecode |-
30	23 29	eqtr3id	Could not format ( x e. ( TC+ A i^i y ) -> ( x i^i ( TC+ A i^i y ) ) = ( x i^i y ) ) : No typesetting found for |- ( x e. ( TC+ A i^i y ) -> ( x i^i ( TC+ A i^i y ) ) = ( x i^i y ) ) with typecode |-
31	30	eqeq1d	Could not format ( x e. ( TC+ A i^i y ) -> ( ( x i^i ( TC+ A i^i y ) ) = (/) <-> ( x i^i y ) = (/) ) ) : No typesetting found for |- ( x e. ( TC+ A i^i y ) -> ( ( x i^i ( TC+ A i^i y ) ) = (/) <-> ( x i^i y ) = (/) ) ) with typecode |-
32	31	biimpa	Could not format ( ( x e. ( TC+ A i^i y ) /\ ( x i^i ( TC+ A i^i y ) ) = (/) ) -> ( x i^i y ) = (/) ) : No typesetting found for |- ( ( x e. ( TC+ A i^i y ) /\ ( x i^i ( TC+ A i^i y ) ) = (/) ) -> ( x i^i y ) = (/) ) with typecode |-
33		ineq1	$$⊢z=x\to z\cap y=x\cap y$$
34	33	eqeq1d	$$⊢z=x\to \left(z\cap y=\varnothing \leftrightarrow x\cap y=\varnothing \right)$$
35		equequ1	$$⊢z=x\to \left(z=w\leftrightarrow x=w\right)$$
36	34 35	imbi12d	$$⊢z=x\to \left(\left(z\cap y=\varnothing \to z=w\right)\leftrightarrow \left(x\cap y=\varnothing \to x=w\right)\right)$$
37	36	rspcv	$$⊢x\in y\to \left(\forall z\in y\left(z\cap y=\varnothing \to z=w\right)\to \left(x\cap y=\varnothing \to x=w\right)\right)$$
38	37	com23	$$⊢x\in y\to \left(x\cap y=\varnothing \to \left(\forall z\in y\left(z\cap y=\varnothing \to z=w\right)\to x=w\right)\right)$$
39	22 32 38	sylc	Could not format ( ( x e. ( TC+ A i^i y ) /\ ( x i^i ( TC+ A i^i y ) ) = (/) ) -> ( A. z e. y ( ( z i^i y ) = (/) -> z = w ) -> x = w ) ) : No typesetting found for |- ( ( x e. ( TC+ A i^i y ) /\ ( x i^i ( TC+ A i^i y ) ) = (/) ) -> ( A. z e. y ( ( z i^i y ) = (/) -> z = w ) -> x = w ) ) with typecode |-
40	39	com12	Could not format ( A. z e. y ( ( z i^i y ) = (/) -> z = w ) -> ( ( x e. ( TC+ A i^i y ) /\ ( x i^i ( TC+ A i^i y ) ) = (/) ) -> x = w ) ) : No typesetting found for |- ( A. z e. y ( ( z i^i y ) = (/) -> z = w ) -> ( ( x e. ( TC+ A i^i y ) /\ ( x i^i ( TC+ A i^i y ) ) = (/) ) -> x = w ) ) with typecode |-
41		eleq1w	Could not format ( x = w -> ( x e. ( TC+ A i^i y ) <-> w e. ( TC+ A i^i y ) ) ) : No typesetting found for |- ( x = w -> ( x e. ( TC+ A i^i y ) <-> w e. ( TC+ A i^i y ) ) ) with typecode |-
42	41	biimpcd	Could not format ( x e. ( TC+ A i^i y ) -> ( x = w -> w e. ( TC+ A i^i y ) ) ) : No typesetting found for |- ( x e. ( TC+ A i^i y ) -> ( x = w -> w e. ( TC+ A i^i y ) ) ) with typecode |-
43	42	adantr	Could not format ( ( x e. ( TC+ A i^i y ) /\ ( x i^i ( TC+ A i^i y ) ) = (/) ) -> ( x = w -> w e. ( TC+ A i^i y ) ) ) : No typesetting found for |- ( ( x e. ( TC+ A i^i y ) /\ ( x i^i ( TC+ A i^i y ) ) = (/) ) -> ( x = w -> w e. ( TC+ A i^i y ) ) ) with typecode |-
44	40 43	sylcom	Could not format ( A. z e. y ( ( z i^i y ) = (/) -> z = w ) -> ( ( x e. ( TC+ A i^i y ) /\ ( x i^i ( TC+ A i^i y ) ) = (/) ) -> w e. ( TC+ A i^i y ) ) ) : No typesetting found for |- ( A. z e. y ( ( z i^i y ) = (/) -> z = w ) -> ( ( x e. ( TC+ A i^i y ) /\ ( x i^i ( TC+ A i^i y ) ) = (/) ) -> w e. ( TC+ A i^i y ) ) ) with typecode |-
45	44	imp	Could not format ( ( A. z e. y ( ( z i^i y ) = (/) -> z = w ) /\ ( x e. ( TC+ A i^i y ) /\ ( x i^i ( TC+ A i^i y ) ) = (/) ) ) -> w e. ( TC+ A i^i y ) ) : No typesetting found for |- ( ( A. z e. y ( ( z i^i y ) = (/) -> z = w ) /\ ( x e. ( TC+ A i^i y ) /\ ( x i^i ( TC+ A i^i y ) ) = (/) ) ) -> w e. ( TC+ A i^i y ) ) with typecode |-
46	45	rexlimdvaa	Could not format ( A. z e. y ( ( z i^i y ) = (/) -> z = w ) -> ( E. x e. ( TC+ A i^i y ) ( x i^i ( TC+ A i^i y ) ) = (/) -> w e. ( TC+ A i^i y ) ) ) : No typesetting found for |- ( A. z e. y ( ( z i^i y ) = (/) -> z = w ) -> ( E. x e. ( TC+ A i^i y ) ( x i^i ( TC+ A i^i y ) ) = (/) -> w e. ( TC+ A i^i y ) ) ) with typecode |-
47	20 46	mpan9	Could not format ( ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = w ) ) -> w e. ( TC+ A i^i y ) ) : No typesetting found for |- ( ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = w ) ) -> w e. ( TC+ A i^i y ) ) with typecode |-
48	47	elin1d	Could not format ( ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = w ) ) -> w e. TC+ A ) : No typesetting found for |- ( ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = w ) ) -> w e. TC+ A ) with typecode |-
49	48	exlimiv	Could not format ( E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = w ) ) -> w e. TC+ A ) : No typesetting found for |- ( E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = w ) ) -> w e. TC+ A ) with typecode |-
50	11 49	sylbi	Could not format ( w e. { x | E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) } -> w e. TC+ A ) : No typesetting found for |- ( w e. { x | E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) } -> w e. TC+ A ) with typecode |-
51	50	ssriv	Could not format { x | E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) } C_ TC+ A : No typesetting found for |- { x | E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) } C_ TC+ A with typecode |-
52	4 51	eqssi	Could not format TC+ A = { x | E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) } : No typesetting found for |- TC+ A = { x | E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) } with typecode |-