Theorem ttcpwss

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

	Ref	Expression
Assertion	ttcpwss	⊢ TC+ 𝒫 𝐴 ⊆ 𝒫 TC+ 𝐴

Proof

Step	Hyp	Ref	Expression
1		ttcid	⊢ 𝐴 ⊆ TC+ 𝐴
2	1	sspwi	⊢ 𝒫 𝐴 ⊆ 𝒫 TC+ 𝐴
3		ttctr	⊢ Tr TC+ 𝐴
4		pwtr	⊢ ( Tr TC+ 𝐴 ↔ Tr 𝒫 TC+ 𝐴 )
5	3 4	mpbi	⊢ Tr 𝒫 TC+ 𝐴
6		ttcmin	⊢ ( ( 𝒫 𝐴 ⊆ 𝒫 TC+ 𝐴 ∧ Tr 𝒫 TC+ 𝐴 ) → TC+ 𝒫 𝐴 ⊆ 𝒫 TC+ 𝐴 )
7	2 5 6	mp2an	⊢ TC+ 𝒫 𝐴 ⊆ 𝒫 TC+ 𝐴