Theorem elttcirr

Description: Irreflexivity of A e. TC+ B relationship. This is a consequence of Regularity, but it does not require Transitive Containment. We use the alternative expression dfttc4 to construct a set in which A is both e. -minimal and not e. -minimal. (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Assertion	elttcirr	Could not format assertion : No typesetting found for |- -. A e. TC+ A with typecode |-

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢y\in \mathrm{V}$$
2		inss2	$$⊢A\cap y\subseteq y$$
3		ssn0	$$⊢\left(A\cap y\subseteq y\wedge A\cap y\ne \varnothing \right)\to y\ne \varnothing$$
4	2 3	mpan	$$⊢A\cap y\ne \varnothing \to y\ne \varnothing$$
5		zfreg	$$⊢\left(y\in \mathrm{V}\wedge y\ne \varnothing \right)\to \exists x\in yx\cap y=\varnothing$$
6	1 4 5	sylancr	$$⊢A\cap y\ne \varnothing \to \exists x\in yx\cap y=\varnothing$$
7		ineq1	$$⊢w=x\to w\cap y=x\cap y$$
8	7	eqeq1d	$$⊢w=x\to \left(w\cap y=\varnothing \leftrightarrow x\cap y=\varnothing \right)$$
9		ineq1	$$⊢x=A\to x\cap y=A\cap y$$
10	9	eqeq1d	$$⊢x=A\to \left(x\cap y=\varnothing \leftrightarrow A\cap y=\varnothing \right)$$
11	8 10	rexraleqim	$$⊢\left(\exists x\in yx\cap y=\varnothing \wedge \forall w\in y\left(w\cap y=\varnothing \to w=A\right)\right)\to A\cap y=\varnothing$$
12	6 11	sylan	$$⊢\left(A\cap y\ne \varnothing \wedge \forall w\in y\left(w\cap y=\varnothing \to w=A\right)\right)\to A\cap y=\varnothing$$
13		neneq	$$⊢A\cap y\ne \varnothing \to \neg A\cap y=\varnothing$$
14	13	adantr	$$⊢\left(A\cap y\ne \varnothing \wedge \forall w\in y\left(w\cap y=\varnothing \to w=A\right)\right)\to \neg A\cap y=\varnothing$$
15	12 14	pm2.65i	$$⊢\neg \left(A\cap y\ne \varnothing \wedge \forall w\in y\left(w\cap y=\varnothing \to w=A\right)\right)$$
16	15	nex	$$⊢\neg \exists y\left(A\cap y\ne \varnothing \wedge \forall w\in y\left(w\cap y=\varnothing \to w=A\right)\right)$$
17		eqeq2	$$⊢x=A\to \left(w=x\leftrightarrow w=A\right)$$
18	17	imbi2d	$$⊢x=A\to \left(\left(w\cap y=\varnothing \to w=x\right)\leftrightarrow \left(w\cap y=\varnothing \to w=A\right)\right)$$
19	18	ralbidv	$$⊢x=A\to \left(\forall w\in y\left(w\cap y=\varnothing \to w=x\right)\leftrightarrow \forall w\in y\left(w\cap y=\varnothing \to w=A\right)\right)$$
20	19	anbi2d	$$⊢x=A\to \left(\left(A\cap y\ne \varnothing \wedge \forall w\in y\left(w\cap y=\varnothing \to w=x\right)\right)\leftrightarrow \left(A\cap y\ne \varnothing \wedge \forall w\in y\left(w\cap y=\varnothing \to w=A\right)\right)\right)$$
21	20	exbidv	$$⊢x=A\to \left(\exists y\left(A\cap y\ne \varnothing \wedge \forall w\in y\left(w\cap y=\varnothing \to w=x\right)\right)\leftrightarrow \exists y\left(A\cap y\ne \varnothing \wedge \forall w\in y\left(w\cap y=\varnothing \to w=A\right)\right)\right)$$
22		dfttc4	Could not format TC+ A = { x | E. y ( ( A i^i y ) =/= (/) /\ A. w e. y ( ( w i^i y ) = (/) -> w = x ) ) } : No typesetting found for |- TC+ A = { x | E. y ( ( A i^i y ) =/= (/) /\ A. w e. y ( ( w i^i y ) = (/) -> w = x ) ) } with typecode |-
23	21 22	elab2g	Could not format ( A e. TC+ A -> ( A e. TC+ A <-> E. y ( ( A i^i y ) =/= (/) /\ A. w e. y ( ( w i^i y ) = (/) -> w = A ) ) ) ) : No typesetting found for |- ( A e. TC+ A -> ( A e. TC+ A <-> E. y ( ( A i^i y ) =/= (/) /\ A. w e. y ( ( w i^i y ) = (/) -> w = A ) ) ) ) with typecode |-
24	23	ibi	Could not format ( A e. TC+ A -> E. y ( ( A i^i y ) =/= (/) /\ A. w e. y ( ( w i^i y ) = (/) -> w = A ) ) ) : No typesetting found for |- ( A e. TC+ A -> E. y ( ( A i^i y ) =/= (/) /\ A. w e. y ( ( w i^i y ) = (/) -> w = A ) ) ) with typecode |-
25	16 24	mto	Could not format -. A e. TC+ A : No typesetting found for |- -. A e. TC+ A with typecode |-