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		simpr	⊢ ( ( 𝑥 ∈ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑥 ∩ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ) = ∅ ) → ( 𝑥 ∩ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ) = ∅ )
8		inssdif0	⊢ ( ( 𝑥 ∩ TC+ 𝐴 ) ⊆ ∪ ( 𝑅1 “ On ) ↔ ( 𝑥 ∩ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ) = ∅ )
9	7 8	sylibr	⊢ ( ( 𝑥 ∈ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑥 ∩ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ) = ∅ ) → ( 𝑥 ∩ TC+ 𝐴 ) ⊆ ∪ ( 𝑅1 “ On ) )
10	6 9	eqsstrrd	⊢ ( ( 𝑥 ∈ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑥 ∩ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ) = ∅ ) → 𝑥 ⊆ ∪ ( 𝑅1 “ On ) )
11		vex	⊢ 𝑥 ∈ V
12	11	r1elss	⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ↔ 𝑥 ⊆ ∪ ( 𝑅1 “ On ) )
13	10 12	sylibr	⊢ ( ( 𝑥 ∈ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑥 ∩ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ) = ∅ ) → 𝑥 ∈ ∪ ( 𝑅1 “ On ) )
14	1	eldifbd	⊢ ( ( 𝑥 ∈ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ∧ ( 𝑥 ∩ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ) = ∅ ) → ¬ 𝑥 ∈ ∪ ( 𝑅1 “ On ) )
15	13 14	pm2.65da	⊢ ( 𝑥 ∈ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) → ¬ ( 𝑥 ∩ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ) = ∅ )
16	15	nrex	⊢ ¬ ∃ 𝑥 ∈ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ( 𝑥 ∩ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ) = ∅
17	16	a1i	⊢ ( TC+ 𝐴 ∈ V → ¬ ∃ 𝑥 ∈ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ( 𝑥 ∩ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ) = ∅ )
18		difexg	⊢ ( TC+ 𝐴 ∈ V → ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ∈ V )
19		zfreg	⊢ ( ( ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ∈ V ∧ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ≠ ∅ ) → ∃ 𝑥 ∈ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ( 𝑥 ∩ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ) = ∅ )
20	18 19	sylan	⊢ ( ( TC+ 𝐴 ∈ V ∧ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ≠ ∅ ) → ∃ 𝑥 ∈ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ( 𝑥 ∩ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ) = ∅ )
21	17 20	mtand	⊢ ( TC+ 𝐴 ∈ V → ¬ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ≠ ∅ )
22		nne	⊢ ( ¬ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) ≠ ∅ ↔ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) = ∅ )
23	21 22	sylib	⊢ ( TC+ 𝐴 ∈ V → ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) = ∅ )
24		ssdif0	⊢ ( TC+ 𝐴 ⊆ ∪ ( 𝑅1 “ On ) ↔ ( TC+ 𝐴 ∖ ∪ ( 𝑅1 “ On ) ) = ∅ )
25	23 24	sylibr	⊢ ( TC+ 𝐴 ∈ V → TC+ 𝐴 ⊆ ∪ ( 𝑅1 “ On ) )
26		eleq1	⊢ ( 𝑥 = TC+ 𝐴 → ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ↔ TC+ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ) )
27		sseq1	⊢ ( 𝑥 = TC+ 𝐴 → ( 𝑥 ⊆ ∪ ( 𝑅1 “ On ) ↔ TC+ 𝐴 ⊆ ∪ ( 𝑅1 “ On ) ) )
28	26 27	bibi12d	⊢ ( 𝑥 = TC+ 𝐴 → ( ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ↔ 𝑥 ⊆ ∪ ( 𝑅1 “ On ) ) ↔ ( TC+ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ TC+ 𝐴 ⊆ ∪ ( 𝑅1 “ On ) ) ) )
29	28 12	vtoclg	⊢ ( TC+ 𝐴 ∈ V → ( TC+ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ TC+ 𝐴 ⊆ ∪ ( 𝑅1 “ On ) ) )
30	25 29	mpbird	⊢ ( TC+ 𝐴 ∈ V → TC+ 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
31		elex	⊢ ( TC+ 𝐴 ∈ ∪ ( 𝑅1 “ On ) → TC+ 𝐴 ∈ V )
32	30 31	impbii	⊢ ( TC+ 𝐴 ∈ V ↔ TC+ 𝐴 ∈ ∪ ( 𝑅1 “ On ) )