Theorem trsspwALT2

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

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

Proof

Step	Hyp	Ref	Expression
1		df-ss	$$⊢A\subseteq 𝒫A\leftrightarrow \forall x\left(x\in A\to x\in 𝒫A\right)$$
2		id	$$⊢\mathrm{Tr}A\to \mathrm{Tr}A$$
3		idd	$$⊢\mathrm{Tr}A\to \left(x\in A\to x\in A\right)$$
4		trss	$$⊢\mathrm{Tr}A\to \left(x\in A\to x\subseteq A\right)$$
5	2 3 4	sylsyld	$$⊢\mathrm{Tr}A\to \left(x\in A\to x\subseteq A\right)$$
6		vex	$$⊢x\in \mathrm{V}$$
7	6	elpw	$$⊢x\in 𝒫A\leftrightarrow x\subseteq A$$
8	5 7	imbitrrdi	$$⊢\mathrm{Tr}A\to \left(x\in A\to x\in 𝒫A\right)$$
9	8	idiALT	$$⊢\mathrm{Tr}A\to \left(x\in A\to x\in 𝒫A\right)$$
10	9	alrimiv	$$⊢\mathrm{Tr}A\to \forall x\left(x\in A\to x\in 𝒫A\right)$$
11		biimpr	$$⊢\left(A\subseteq 𝒫A\leftrightarrow \forall x\left(x\in A\to x\in 𝒫A\right)\right)\to \left(\forall x\left(x\in A\to x\in 𝒫A\right)\to A\subseteq 𝒫A\right)$$
12	1 10 11	mpsyl	$$⊢\mathrm{Tr}A\to A\subseteq 𝒫A$$
13	12	idiALT	$$⊢\mathrm{Tr}A\to A\subseteq 𝒫A$$