Theorem sspwtrALT

Description: Virtual deduction proof of sspwtr . This proof is the same as the proof of sspwtr except each virtual deduction symbol is replaced by its non-virtual deduction symbol equivalent. A class which is a subclass of its power class is transitive. (Contributed by Alan Sare, 3-May-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		dftr2	$$⊢\mathrm{Tr}A\leftrightarrow \forall z\forall y\left(\left(z\in y\wedge y\in A\right)\to z\in A\right)$$
2		simpr	$$⊢\left(z\in y\wedge y\in A\right)\to y\in A$$
3		ssel	$$⊢A\subseteq 𝒫A\to \left(y\in A\to y\in 𝒫A\right)$$
4		elpwi	$$⊢y\in 𝒫A\to y\subseteq A$$
5	2 3 4	syl56	$$⊢A\subseteq 𝒫A\to \left(\left(z\in y\wedge y\in A\right)\to y\subseteq A\right)$$
6		idd	$$⊢A\subseteq 𝒫A\to \left(\left(z\in y\wedge y\in A\right)\to \left(z\in y\wedge y\in A\right)\right)$$
7		simpl	$$⊢\left(z\in y\wedge y\in A\right)\to z\in y$$
8	6 7	syl6	$$⊢A\subseteq 𝒫A\to \left(\left(z\in y\wedge y\in A\right)\to z\in y\right)$$
9		ssel	$$⊢y\subseteq A\to \left(z\in y\to z\in A\right)$$
10	5 8 9	syl6c	$$⊢A\subseteq 𝒫A\to \left(\left(z\in y\wedge y\in A\right)\to z\in A\right)$$
11	10	alrimivv	$$⊢A\subseteq 𝒫A\to \forall z\forall y\left(\left(z\in y\wedge y\in A\right)\to z\in A\right)$$
12		biimpr	$$⊢\left(\mathrm{Tr}A\leftrightarrow \forall z\forall y\left(\left(z\in y\wedge y\in A\right)\to z\in A\right)\right)\to \left(\forall z\forall y\left(\left(z\in y\wedge y\in A\right)\to z\in A\right)\to \mathrm{Tr}A\right)$$
13	1 11 12	mpsyl	$$⊢A\subseteq 𝒫A\to \mathrm{Tr}A$$
14	13	idiALT	$$⊢A\subseteq 𝒫A\to \mathrm{Tr}A$$