Theorem ttcwf2

Description: If a transitive closure class is a set, then it is well-founded, assuming Regularity. (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Assertion	ttcwf2	⊢ ( TC+ 𝐴 ∈ V ↔ TC+ 𝐴 ∈ ∪ ( 𝑅1 “ On ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝑥 ∈ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑥 ∩ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ) = ∅ ) → 𝑥 ∈ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) )
2	1	eldifad	⊢ ( ( 𝑥 ∈ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑥 ∩ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ) = ∅ ) → 𝑥 ∈ TC+ 𝐴 )
3		ttctr2	⊢ ( 𝑥 ∈ TC+ 𝐴 → 𝑥 ⊆ TC+ 𝐴 )
4	2 3	syl	⊢ ( ( 𝑥 ∈ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑥 ∩ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ) = ∅ ) → 𝑥 ⊆ TC+ 𝐴 )
5		dfss2	⊢ ( 𝑥 ⊆ TC+ 𝐴 ↔ ( 𝑥 ∩ TC+ 𝐴 ) = 𝑥 )
6	4 5	sylib	⊢ ( ( 𝑥 ∈ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑥 ∩ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ) = ∅ ) → ( 𝑥 ∩ TC+ 𝐴 ) = 𝑥 )
7		inssdif0	⊢ ( ( 𝑥 ∩ TC+ 𝐴 ) ⊆ ∪ ( 𝑅1 “ On ) ↔ ( 𝑥 ∩ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ) = ∅ )
8	7	bilanri	⊢ ( ( 𝑥 ∈ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑥 ∩ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ) = ∅ ) → ( 𝑥 ∩ TC+ 𝐴 ) ⊆ ∪ ( 𝑅1 “ On ) )
9	6 8	eqsstrrd	⊢ ( ( 𝑥 ∈ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑥 ∩ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ) = ∅ ) → 𝑥 ⊆ ∪ ( 𝑅1 “ On ) )
10		vex	⊢ 𝑥 ∈ V
11	10	r1elss	⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ↔ 𝑥 ⊆ ∪ ( 𝑅1 “ On ) )
12	9 11	sylibr	⊢ ( ( 𝑥 ∈ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑥 ∩ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ) = ∅ ) → 𝑥 ∈ ∪ ( 𝑅1 “ On ) )
13	1	eldifbd	⊢ ( ( 𝑥 ∈ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑥 ∩ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ) = ∅ ) → ¬ 𝑥 ∈ ∪ ( 𝑅1 “ On ) )
14	12 13	pm2.65da	⊢ ( 𝑥 ∈ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) → ¬ ( 𝑥 ∩ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ) = ∅ )
15	14	nrex	⊢ ¬ ∃ 𝑥 ∈ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ( 𝑥 ∩ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ) = ∅
16	15	a1i	⊢ ( TC+ 𝐴 ∈ V → ¬ ∃ 𝑥 ∈ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ( 𝑥 ∩ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ) = ∅ )
17		difexg	⊢ ( TC+ 𝐴 ∈ V → ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ∈ V )
18		zfreg	⊢ ( ( ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ∈ V ∧ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ≠ ∅ ) → ∃ 𝑥 ∈ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ( 𝑥 ∩ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ) = ∅ )
19	17 18	sylan	⊢ ( ( TC+ 𝐴 ∈ V ∧ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ≠ ∅ ) → ∃ 𝑥 ∈ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ( 𝑥 ∩ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ) = ∅ )
20	16 19	mtand	⊢ ( TC+ 𝐴 ∈ V → ¬ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ≠ ∅ )
21		nne	⊢ ( ¬ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ≠ ∅ ↔ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) = ∅ )
22	20 21	sylib	⊢ ( TC+ 𝐴 ∈ V → ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) = ∅ )
23		ssdif0	⊢ ( TC+ 𝐴 ⊆ ∪ ( 𝑅1 “ On ) ↔ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) = ∅ )
24	22 23	sylibr	⊢ ( TC+ 𝐴 ∈ V → TC+ 𝐴 ⊆ ∪ ( 𝑅1 “ On ) )
25		eleq1	⊢ ( 𝑥 = TC+ 𝐴 → ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ↔ TC+ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ) )
26		sseq1	⊢ ( 𝑥 = TC+ 𝐴 → ( 𝑥 ⊆ ∪ ( 𝑅1 “ On ) ↔ TC+ 𝐴 ⊆ ∪ ( 𝑅1 “ On ) ) )
27	25 26	bibi12d	⊢ ( 𝑥 = TC+ 𝐴 → ( ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ↔ 𝑥 ⊆ ∪ ( 𝑅1 “ On ) ) ↔ ( TC+ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ TC+ 𝐴 ⊆ ∪ ( 𝑅1 “ On ) ) ) )
28	27 11	vtoclg	⊢ ( TC+ 𝐴 ∈ V → ( TC+ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ TC+ 𝐴 ⊆ ∪ ( 𝑅1 “ On ) ) )
29	24 28	mpbird	⊢ ( TC+ 𝐴 ∈ V → TC+ 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
30		elex	⊢ ( TC+ 𝐴 ∈ ∪ ( 𝑅1 “ On ) → TC+ 𝐴 ∈ V )
31	29 30	impbii	⊢ ( TC+ 𝐴 ∈ V ↔ TC+ 𝐴 ∈ ∪ ( 𝑅1 “ On ) )