Theorem trsspwALT

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

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

Proof

Step	Hyp	Ref	Expression
1		dfss2	$$⊢A\subseteq 𝒫A\leftrightarrow \forall x\left(x\in A\to x\in 𝒫A\right)$$
2		idn1	$$⊢\left(\mathrm{Tr}A\to \mathrm{Tr}A\right)$$
3		idn2	$$⊢\left(\mathrm{Tr}A,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	e12	$$⊢\left(\mathrm{Tr}A,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	e2bir	$$⊢\left(\mathrm{Tr}A,x\in A\to x\in 𝒫A\right)$$
9	8	in2	$$⊢\left(\mathrm{Tr}A\to \left(x\in A\to x\in 𝒫A\right)\right)$$
10	9	gen11	$$⊢\left(\mathrm{Tr}A\to \forall x\left(x\in A\to x\in 𝒫A\right)\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	e01	$$⊢\left(\mathrm{Tr}A\to A\subseteq 𝒫A\right)$$
13	12	in1	$$⊢\mathrm{Tr}A\to A\subseteq 𝒫A$$