Theorem sspwtr

Description: Virtual deduction proof of the right-to-left implication of dftr4 . A class which is a subclass of its power class is transitive. This proof corresponds to the virtual deduction proof of sspwtr without accumulating results. (Contributed by Alan Sare, 2-May-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	sspwtr	$$⊢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		idn1	$$⊢\left(A\subseteq 𝒫A\to A\subseteq 𝒫A\right)$$
3		idn2	$$⊢\left(A\subseteq 𝒫A,\left(z\in y\wedge y\in A\right)\to \left(z\in y\wedge y\in A\right)\right)$$
4		simpr	$$⊢\left(z\in y\wedge y\in A\right)\to y\in A$$
5	3 4	e2	$$⊢\left(A\subseteq 𝒫A,\left(z\in y\wedge y\in A\right)\to y\in A\right)$$
6		ssel	$$⊢A\subseteq 𝒫A\to \left(y\in A\to y\in 𝒫A\right)$$
7	2 5 6	e12	$$⊢\left(A\subseteq 𝒫A,\left(z\in y\wedge y\in A\right)\to y\in 𝒫A\right)$$
8		elpwi	$$⊢y\in 𝒫A\to y\subseteq A$$
9	7 8	e2	$$⊢\left(A\subseteq 𝒫A,\left(z\in y\wedge y\in A\right)\to y\subseteq A\right)$$
10		simpl	$$⊢\left(z\in y\wedge y\in A\right)\to z\in y$$
11	3 10	e2	$$⊢\left(A\subseteq 𝒫A,\left(z\in y\wedge y\in A\right)\to z\in y\right)$$
12		ssel	$$⊢y\subseteq A\to \left(z\in y\to z\in A\right)$$
13	9 11 12	e22	$$⊢\left(A\subseteq 𝒫A,\left(z\in y\wedge y\in A\right)\to z\in A\right)$$
14	13	in2	$$⊢\left(A\subseteq 𝒫A\to \left(\left(z\in y\wedge y\in A\right)\to z\in A\right)\right)$$
15	14	gen12	$$⊢\left(A\subseteq 𝒫A\to \forall z\forall y\left(\left(z\in y\wedge y\in A\right)\to z\in A\right)\right)$$
16		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)$$
17	1 15 16	e01	$$⊢\left(A\subseteq 𝒫A\to \mathrm{Tr}A\right)$$
18	17	in1	$$⊢A\subseteq 𝒫A\to \mathrm{Tr}A$$