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	⊢ ◡ [⊊] hereditary 𝒫 𝐴

Proof

Step	Hyp	Ref	Expression
1		dfhe3	⊢ ( ◡ [⊊] hereditary 𝒫 𝐴 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝒫 𝐴 → ∀ 𝑦 ( 𝑥 ◡ [⊊] 𝑦 → 𝑦 ∈ 𝒫 𝐴 ) ) )
2		sstr2	⊢ ( 𝑦 ⊆ 𝑥 → ( 𝑥 ⊆ 𝐴 → 𝑦 ⊆ 𝐴 ) )
3		pssss	⊢ ( 𝑦 ⊊ 𝑥 → 𝑦 ⊆ 𝑥 )
4	2 3	syl11	⊢ ( 𝑥 ⊆ 𝐴 → ( 𝑦 ⊊ 𝑥 → 𝑦 ⊆ 𝐴 ) )
5	4	alrimiv	⊢ ( 𝑥 ⊆ 𝐴 → ∀ 𝑦 ( 𝑦 ⊊ 𝑥 → 𝑦 ⊆ 𝐴 ) )
6		velpw	⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴 )
7		vex	⊢ 𝑥 ∈ V
8		vex	⊢ 𝑦 ∈ V
9	7 8	brcnv	⊢ ( 𝑥 ◡ [⊊] 𝑦 ↔ 𝑦 [⊊] 𝑥 )
10	7	brrpss	⊢ ( 𝑦 [⊊] 𝑥 ↔ 𝑦 ⊊ 𝑥 )
11	9 10	bitri	⊢ ( 𝑥 ◡ [⊊] 𝑦 ↔ 𝑦 ⊊ 𝑥 )
12		velpw	⊢ ( 𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 ⊆ 𝐴 )
13	11 12	imbi12i	⊢ ( ( 𝑥 ◡ [⊊] 𝑦 → 𝑦 ∈ 𝒫 𝐴 ) ↔ ( 𝑦 ⊊ 𝑥 → 𝑦 ⊆ 𝐴 ) )
14	13	albii	⊢ ( ∀ 𝑦 ( 𝑥 ◡ [⊊] 𝑦 → 𝑦 ∈ 𝒫 𝐴 ) ↔ ∀ 𝑦 ( 𝑦 ⊊ 𝑥 → 𝑦 ⊆ 𝐴 ) )
15	5 6 14	3imtr4i	⊢ ( 𝑥 ∈ 𝒫 𝐴 → ∀ 𝑦 ( 𝑥 ◡ [⊊] 𝑦 → 𝑦 ∈ 𝒫 𝐴 ) )
16	1 15	mpgbir	⊢ ◡ [⊊] hereditary 𝒫 𝐴