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\forall y\left(\left(z\in y\wedge y\in A\right)\to z\in A\right)$$
10		dftr2	$$⊢\mathrm{Tr}A\leftrightarrow \forall z\forall y\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$$