Metamath Proof Explorer

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 
|- `' [C.] hereditary ~P A

Proof

Step Hyp Ref Expression
1 dfhe3 
 |-  ( `' [C.] hereditary ~P A <-> A. x ( x e. ~P A -> A. y ( x `' [C.] y -> y e. ~P A ) ) )
2 sstr2 
 |-  ( y C_ x -> ( x C_ A -> y C_ A ) )
3 pssss 
 |-  ( y C. x -> y C_ x )
4 2 3 syl11 
 |-  ( x C_ A -> ( y C. x -> y C_ A ) )
5 4 alrimiv 
 |-  ( x C_ A -> A. y ( y C. x -> y C_ A ) )
6 velpw 
 |-  ( x e. ~P A <-> x C_ A )
7 vex 
 |-  x e. _V
8 vex 
 |-  y e. _V
9 7 8 brcnv 
 |-  ( x `' [C.] y <-> y [C.] x )
10 7 brrpss 
 |-  ( y [C.] x <-> y C. x )
11 9 10 bitri 
 |-  ( x `' [C.] y <-> y C. x )
12 velpw 
 |-  ( y e. ~P A <-> y C_ A )
13 11 12 imbi12i 
 |-  ( ( x `' [C.] y -> y e. ~P A ) <-> ( y C. x -> y C_ A ) )
14 13 albii 
 |-  ( A. y ( x `' [C.] y -> y e. ~P A ) <-> A. y ( y C. x -> y C_ A ) )
15 5 6 14 3imtr4i 
 |-  ( x e. ~P A -> A. y ( x `' [C.] y -> y e. ~P A ) )
16 1 15 mpgbir 
 |-  `' [C.] hereditary ~P A