Theorem psshepw

Description: The relation between sets and their proper subsets is hereditary in the powerclass of any class. (Contributed by RP, 28-Mar-2020)

	Ref	Expression
Assertion	psshepw	$$⊢{[\subset ]}^{-1}hereditary𝒫A$$

Proof

Step	Hyp	Ref	Expression
1		dfhe3	$$⊢{[\subset ]}^{-1}hereditary𝒫A\leftrightarrow \forall x\left(x\in 𝒫A\to \forall y\left(x{[\subset ]}^{-1}y\to y\in 𝒫A\right)\right)$$
2		sstr2	$$⊢y\subseteq x\to \left(x\subseteq A\to y\subseteq A\right)$$
3		pssss	$$⊢y\subset x\to y\subseteq x$$
4	2 3	syl11	$$⊢x\subseteq A\to \left(y\subset x\to y\subseteq A\right)$$
5	4	alrimiv	$$⊢x\subseteq A\to \forall y\left(y\subset x\to y\subseteq A\right)$$
6		velpw	$$⊢x\in 𝒫A\leftrightarrow x\subseteq A$$
7		vex	$$⊢x\in \mathrm{V}$$
8		vex	$$⊢y\in \mathrm{V}$$
9	7 8	brcnv	$$⊢x{[\subset ]}^{-1}y\leftrightarrow y[\subset ]x$$
10	7	brrpss	$$⊢y[\subset ]x\leftrightarrow y\subset x$$
11	9 10	bitri	$$⊢x{[\subset ]}^{-1}y\leftrightarrow y\subset x$$
12		velpw	$$⊢y\in 𝒫A\leftrightarrow y\subseteq A$$
13	11 12	imbi12i	$$⊢\left(x{[\subset ]}^{-1}y\to y\in 𝒫A\right)\leftrightarrow \left(y\subset x\to y\subseteq A\right)$$
14	13	albii	$$⊢\forall y\left(x{[\subset ]}^{-1}y\to y\in 𝒫A\right)\leftrightarrow \forall y\left(y\subset x\to y\subseteq A\right)$$
15	5 6 14	3imtr4i	$$⊢x\in 𝒫A\to \forall y\left(x{[\subset ]}^{-1}y\to y\in 𝒫A\right)$$
16	1 15	mpgbir	$$⊢{[\subset ]}^{-1}hereditary𝒫A$$