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	⊢ ¬ 𝐴 ∈ TC+ 𝐴

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑦 ∈ V
2		inss2	⊢ ( 𝐴 ∩ 𝑦 ) ⊆ 𝑦
3		ssn0	⊢ ( ( ( 𝐴 ∩ 𝑦 ) ⊆ 𝑦 ∧ ( 𝐴 ∩ 𝑦 ) ≠ ∅ ) → 𝑦 ≠ ∅ )
4	2 3	mpan	⊢ ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ → 𝑦 ≠ ∅ )
5		zfreg	⊢ ( ( 𝑦 ∈ V ∧ 𝑦 ≠ ∅ ) → ∃ 𝑥 ∈ 𝑦 ( 𝑥 ∩ 𝑦 ) = ∅ )
6	1 4 5	sylancr	⊢ ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ → ∃ 𝑥 ∈ 𝑦 ( 𝑥 ∩ 𝑦 ) = ∅ )
7		ineq1	⊢ ( 𝑤 = 𝑥 → ( 𝑤 ∩ 𝑦 ) = ( 𝑥 ∩ 𝑦 ) )
8	7	eqeq1d	⊢ ( 𝑤 = 𝑥 → ( ( 𝑤 ∩ 𝑦 ) = ∅ ↔ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
9		ineq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∩ 𝑦 ) = ( 𝐴 ∩ 𝑦 ) )
10	9	eqeq1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∩ 𝑦 ) = ∅ ↔ ( 𝐴 ∩ 𝑦 ) = ∅ ) )
11	8 10	rexraleqim	⊢ ( ( ∃ 𝑥 ∈ 𝑦 ( 𝑥 ∩ 𝑦 ) = ∅ ∧ ∀ 𝑤 ∈ 𝑦 ( ( 𝑤 ∩ 𝑦 ) = ∅ → 𝑤 = 𝐴 ) ) → ( 𝐴 ∩ 𝑦 ) = ∅ )
12	6 11	sylan	⊢ ( ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑦 ( ( 𝑤 ∩ 𝑦 ) = ∅ → 𝑤 = 𝐴 ) ) → ( 𝐴 ∩ 𝑦 ) = ∅ )
13		neneq	⊢ ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ → ¬ ( 𝐴 ∩ 𝑦 ) = ∅ )
14	13	adantr	⊢ ( ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑦 ( ( 𝑤 ∩ 𝑦 ) = ∅ → 𝑤 = 𝐴 ) ) → ¬ ( 𝐴 ∩ 𝑦 ) = ∅ )
15	12 14	pm2.65i	⊢ ¬ ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑦 ( ( 𝑤 ∩ 𝑦 ) = ∅ → 𝑤 = 𝐴 ) )
16	15	nex	⊢ ¬ ∃ 𝑦 ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑦 ( ( 𝑤 ∩ 𝑦 ) = ∅ → 𝑤 = 𝐴 ) )
17		eqeq2	⊢ ( 𝑥 = 𝐴 → ( 𝑤 = 𝑥 ↔ 𝑤 = 𝐴 ) )
18	17	imbi2d	⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑤 ∩ 𝑦 ) = ∅ → 𝑤 = 𝑥 ) ↔ ( ( 𝑤 ∩ 𝑦 ) = ∅ → 𝑤 = 𝐴 ) ) )
19	18	ralbidv	⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑤 ∈ 𝑦 ( ( 𝑤 ∩ 𝑦 ) = ∅ → 𝑤 = 𝑥 ) ↔ ∀ 𝑤 ∈ 𝑦 ( ( 𝑤 ∩ 𝑦 ) = ∅ → 𝑤 = 𝐴 ) ) )
20	19	anbi2d	⊢ ( 𝑥 = 𝐴 → ( ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑦 ( ( 𝑤 ∩ 𝑦 ) = ∅ → 𝑤 = 𝑥 ) ) ↔ ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑦 ( ( 𝑤 ∩ 𝑦 ) = ∅ → 𝑤 = 𝐴 ) ) ) )
21	20	exbidv	⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑦 ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑦 ( ( 𝑤 ∩ 𝑦 ) = ∅ → 𝑤 = 𝑥 ) ) ↔ ∃ 𝑦 ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑦 ( ( 𝑤 ∩ 𝑦 ) = ∅ → 𝑤 = 𝐴 ) ) ) )
22		dfttc4	⊢ TC+ 𝐴 = { 𝑥 ∣ ∃ 𝑦 ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑦 ( ( 𝑤 ∩ 𝑦 ) = ∅ → 𝑤 = 𝑥 ) ) }
23	21 22	elab2g	⊢ ( 𝐴 ∈ TC+ 𝐴 → ( 𝐴 ∈ TC+ 𝐴 ↔ ∃ 𝑦 ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑦 ( ( 𝑤 ∩ 𝑦 ) = ∅ → 𝑤 = 𝐴 ) ) ) )
24	23	ibi	⊢ ( 𝐴 ∈ TC+ 𝐴 → ∃ 𝑦 ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑦 ( ( 𝑤 ∩ 𝑦 ) = ∅ → 𝑤 = 𝐴 ) ) )
25	16 24	mto	⊢ ¬ 𝐴 ∈ TC+ 𝐴