Theorem sshepw

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

	Ref	Expression
Assertion	sshepw	⊢ ( ◡ [⊊] ∪ I ) hereditary 𝒫 𝐴

Proof

Step	Hyp	Ref	Expression
1		psshepw	⊢ ◡ [⊊] hereditary 𝒫 𝐴
2		idhe	⊢ I hereditary 𝒫 𝐴
3		unhe1	⊢ ( ( ◡ [⊊] hereditary 𝒫 𝐴 ∧ I hereditary 𝒫 𝐴 ) → ( ◡ [⊊] ∪ I ) hereditary 𝒫 𝐴 )
4	1 2 3	mp2an	⊢ ( ◡ [⊊] ∪ I ) hereditary 𝒫 𝐴