# Metamath Proof Explorer

## Theorem sspwtrALT2

Description: Short predicate calculus proof of the right-to-left implication of dftr4 . A class which is a subclass of its power class is transitive. This proof was constructed by applying Metamath's minimize command to the proof of sspwtrALT , which is the virtual deduction proof sspwtr without virtual deductions. (Contributed by Alan Sare, 3-May-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion sspwtrALT2 ${⊢}{A}\subseteq 𝒫{A}\to \mathrm{Tr}{A}$

### Proof

Step Hyp Ref Expression
1 ssel ${⊢}{A}\subseteq 𝒫{A}\to \left({y}\in {A}\to {y}\in 𝒫{A}\right)$
2 1 adantld ${⊢}{A}\subseteq 𝒫{A}\to \left(\left({z}\in {y}\wedge {y}\in {A}\right)\to {y}\in 𝒫{A}\right)$
3 elpwi ${⊢}{y}\in 𝒫{A}\to {y}\subseteq {A}$
4 2 3 syl6 ${⊢}{A}\subseteq 𝒫{A}\to \left(\left({z}\in {y}\wedge {y}\in {A}\right)\to {y}\subseteq {A}\right)$
5 simpl ${⊢}\left({z}\in {y}\wedge {y}\in {A}\right)\to {z}\in {y}$
6 5 a1i ${⊢}{A}\subseteq 𝒫{A}\to \left(\left({z}\in {y}\wedge {y}\in {A}\right)\to {z}\in {y}\right)$
7 ssel ${⊢}{y}\subseteq {A}\to \left({z}\in {y}\to {z}\in {A}\right)$
8 4 6 7 syl6c ${⊢}{A}\subseteq 𝒫{A}\to \left(\left({z}\in {y}\wedge {y}\in {A}\right)\to {z}\in {A}\right)$
9 8 alrimivv ${⊢}{A}\subseteq 𝒫{A}\to \forall {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({z}\in {y}\wedge {y}\in {A}\right)\to {z}\in {A}\right)$
10 dftr2 ${⊢}\mathrm{Tr}{A}↔\forall {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({z}\in {y}\wedge {y}\in {A}\right)\to {z}\in {A}\right)$
11 9 10 sylibr ${⊢}{A}\subseteq 𝒫{A}\to \mathrm{Tr}{A}$