This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pwtr

Description: A class is transitive iff its power class is transitive. (Contributed by Alan Sare, 25-Aug-2011) (Revised by Mario Carneiro, 15-Jun-2014)

Ref Expression
Assertion pwtr ⊢ Tr ⁡ A ↔ Tr ⁡ 𝒫 A

Proof

Step Hyp Ref Expression
1 unipw ⊢ ⋃ 𝒫 A = A
2 1 sseq1i ⊢ ⋃ 𝒫 A ⊆ 𝒫 A ↔ A ⊆ 𝒫 A
3 df-tr ⊢ Tr ⁡ 𝒫 A ↔ ⋃ 𝒫 A ⊆ 𝒫 A
4 dftr4 ⊢ Tr ⁡ A ↔ A ⊆ 𝒫 A
5 2 3 4 3bitr4ri ⊢ Tr ⁡ A ↔ Tr ⁡ 𝒫 A