Theorem ttcid

Description: The transitive closure contains its argument as a subclass. (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Assertion	ttcid	⊢ 𝐴 ⊆ TC+ 𝐴

Proof

Step	Hyp	Ref	Expression
1		vsnid	⊢ 𝑧 ∈ { 𝑧 }
2		vsnex	⊢ { 𝑧 } ∈ V
3	2	rdg0	⊢ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑧 } ) ‘ ∅ ) = { 𝑧 }
4		rdgfnon	⊢ rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑧 } ) Fn On
5		omsson	⊢ ω ⊆ On
6		peano1	⊢ ∅ ∈ ω
7		fnfvima	⊢ ( ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑧 } ) Fn On ∧ ω ⊆ On ∧ ∅ ∈ ω ) → ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑧 } ) ‘ ∅ ) ∈ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑧 } ) “ ω ) )
8	4 5 6 7	mp3an	⊢ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑧 } ) ‘ ∅ ) ∈ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑧 } ) “ ω )
9	3 8	eqeltrri	⊢ { 𝑧 } ∈ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑧 } ) “ ω )
10		elunii	⊢ ( ( 𝑧 ∈ { 𝑧 } ∧ { 𝑧 } ∈ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑧 } ) “ ω ) ) → 𝑧 ∈ ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑧 } ) “ ω ) )
11	1 9 10	mp2an	⊢ 𝑧 ∈ ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑧 } ) “ ω )
12		sneq	⊢ ( 𝑥 = 𝑧 → { 𝑥 } = { 𝑧 } )
13		rdgeq2	⊢ ( { 𝑥 } = { 𝑧 } → rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) = rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑧 } ) )
14	12 13	syl	⊢ ( 𝑥 = 𝑧 → rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) = rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑧 } ) )
15	14	imaeq1d	⊢ ( 𝑥 = 𝑧 → ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω ) = ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑧 } ) “ ω ) )
16	15	unieqd	⊢ ( 𝑥 = 𝑧 → ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω ) = ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑧 } ) “ ω ) )
17	16	eliuni	⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑧 } ) “ ω ) ) → 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω ) )
18	11 17	mpan2	⊢ ( 𝑧 ∈ 𝐴 → 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω ) )
19		df-ttc	⊢ TC+ 𝐴 = ∪ 𝑥 ∈ 𝐴 ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω )
20	18 19	eleqtrrdi	⊢ ( 𝑧 ∈ 𝐴 → 𝑧 ∈ TC+ 𝐴 )
21	20	ssriv	⊢ 𝐴 ⊆ TC+ 𝐴