Theorem ttctrid

Description: The transitive closure of a transitive class is the class itself. (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Assertion	ttctrid	Could not format assertion : No typesetting found for |- ( Tr A -> TC+ A = A ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		ssid	$$⊢A\subseteq A$$
2		ttcmin	Could not format ( ( A C_ A /\ Tr A ) -> TC+ A C_ A ) : No typesetting found for |- ( ( A C_ A /\ Tr A ) -> TC+ A C_ A ) with typecode |-
3	1 2	mpan	Could not format ( Tr A -> TC+ A C_ A ) : No typesetting found for |- ( Tr A -> TC+ A C_ A ) with typecode |-
4		ttcid	Could not format A C_ TC+ A : No typesetting found for |- A C_ TC+ A with typecode |-
5	4	a1i	Could not format ( Tr A -> A C_ TC+ A ) : No typesetting found for |- ( Tr A -> A C_ TC+ A ) with typecode |-
6	3 5	eqssd	Could not format ( Tr A -> TC+ A = A ) : No typesetting found for |- ( Tr A -> TC+ A = A ) with typecode |-