Metamath Proof Explorer

Theorem sorpsscmpl

Description: The componentwise complement of a chain of sets is also a chain of sets. (Contributed by Stefan O'Rear, 2-Nov-2014)

Ref Expression
Assertion sorpsscmpl 
|- ( [C.] Or Y -> [C.] Or { u e. ~P A | ( A \ u ) e. Y } )

Proof

Step Hyp Ref Expression
1 difeq2 
 |-  ( u = x -> ( A \ u ) = ( A \ x ) )
2 1 eleq1d 
 |-  ( u = x -> ( ( A \ u ) e. Y <-> ( A \ x ) e. Y ) )
3 2 elrab 
 |-  ( x e. { u e. ~P A | ( A \ u ) e. Y } <-> ( x e. ~P A /\ ( A \ x ) e. Y ) )
4 difeq2 
 |-  ( u = y -> ( A \ u ) = ( A \ y ) )
5 4 eleq1d 
 |-  ( u = y -> ( ( A \ u ) e. Y <-> ( A \ y ) e. Y ) )
6 5 elrab 
 |-  ( y e. { u e. ~P A | ( A \ u ) e. Y } <-> ( y e. ~P A /\ ( A \ y ) e. Y ) )
7 an4 
 |-  ( ( ( x e. ~P A /\ ( A \ x ) e. Y ) /\ ( y e. ~P A /\ ( A \ y ) e. Y ) ) <-> ( ( x e. ~P A /\ y e. ~P A ) /\ ( ( A \ x ) e. Y /\ ( A \ y ) e. Y ) ) )
8 7 biimpi 
 |-  ( ( ( x e. ~P A /\ ( A \ x ) e. Y ) /\ ( y e. ~P A /\ ( A \ y ) e. Y ) ) -> ( ( x e. ~P A /\ y e. ~P A ) /\ ( ( A \ x ) e. Y /\ ( A \ y ) e. Y ) ) )
9 3 6 8 syl2anb 
 |-  ( ( x e. { u e. ~P A | ( A \ u ) e. Y } /\ y e. { u e. ~P A | ( A \ u ) e. Y } ) -> ( ( x e. ~P A /\ y e. ~P A ) /\ ( ( A \ x ) e. Y /\ ( A \ y ) e. Y ) ) )
10 sorpssi 
 |-  ( ( [C.] Or Y /\ ( ( A \ x ) e. Y /\ ( A \ y ) e. Y ) ) -> ( ( A \ x ) C_ ( A \ y ) \/ ( A \ y ) C_ ( A \ x ) ) )
11 10 expcom 
 |-  ( ( ( A \ x ) e. Y /\ ( A \ y ) e. Y ) -> ( [C.] Or Y -> ( ( A \ x ) C_ ( A \ y ) \/ ( A \ y ) C_ ( A \ x ) ) ) )
12 velpw 
 |-  ( x e. ~P A <-> x C_ A )
13 dfss4 
 |-  ( x C_ A <-> ( A \ ( A \ x ) ) = x )
14 12 13 bitri 
 |-  ( x e. ~P A <-> ( A \ ( A \ x ) ) = x )
15 velpw 
 |-  ( y e. ~P A <-> y C_ A )
16 dfss4 
 |-  ( y C_ A <-> ( A \ ( A \ y ) ) = y )
17 15 16 bitri 
 |-  ( y e. ~P A <-> ( A \ ( A \ y ) ) = y )
18 sscon 
 |-  ( ( A \ y ) C_ ( A \ x ) -> ( A \ ( A \ x ) ) C_ ( A \ ( A \ y ) ) )
19 sseq12 
 |-  ( ( ( A \ ( A \ x ) ) = x /\ ( A \ ( A \ y ) ) = y ) -> ( ( A \ ( A \ x ) ) C_ ( A \ ( A \ y ) ) <-> x C_ y ) )
20 18 19 syl5ib 
 |-  ( ( ( A \ ( A \ x ) ) = x /\ ( A \ ( A \ y ) ) = y ) -> ( ( A \ y ) C_ ( A \ x ) -> x C_ y ) )
21 sscon 
 |-  ( ( A \ x ) C_ ( A \ y ) -> ( A \ ( A \ y ) ) C_ ( A \ ( A \ x ) ) )
22 sseq12 
 |-  ( ( ( A \ ( A \ y ) ) = y /\ ( A \ ( A \ x ) ) = x ) -> ( ( A \ ( A \ y ) ) C_ ( A \ ( A \ x ) ) <-> y C_ x ) )
23 22 ancoms 
 |-  ( ( ( A \ ( A \ x ) ) = x /\ ( A \ ( A \ y ) ) = y ) -> ( ( A \ ( A \ y ) ) C_ ( A \ ( A \ x ) ) <-> y C_ x ) )
24 21 23 syl5ib 
 |-  ( ( ( A \ ( A \ x ) ) = x /\ ( A \ ( A \ y ) ) = y ) -> ( ( A \ x ) C_ ( A \ y ) -> y C_ x ) )
25 20 24 orim12d 
 |-  ( ( ( A \ ( A \ x ) ) = x /\ ( A \ ( A \ y ) ) = y ) -> ( ( ( A \ y ) C_ ( A \ x ) \/ ( A \ x ) C_ ( A \ y ) ) -> ( x C_ y \/ y C_ x ) ) )
26 14 17 25 syl2anb 
 |-  ( ( x e. ~P A /\ y e. ~P A ) -> ( ( ( A \ y ) C_ ( A \ x ) \/ ( A \ x ) C_ ( A \ y ) ) -> ( x C_ y \/ y C_ x ) ) )
27 26 com12 
 |-  ( ( ( A \ y ) C_ ( A \ x ) \/ ( A \ x ) C_ ( A \ y ) ) -> ( ( x e. ~P A /\ y e. ~P A ) -> ( x C_ y \/ y C_ x ) ) )
28 27 orcoms 
 |-  ( ( ( A \ x ) C_ ( A \ y ) \/ ( A \ y ) C_ ( A \ x ) ) -> ( ( x e. ~P A /\ y e. ~P A ) -> ( x C_ y \/ y C_ x ) ) )
29 11 28 syl6 
 |-  ( ( ( A \ x ) e. Y /\ ( A \ y ) e. Y ) -> ( [C.] Or Y -> ( ( x e. ~P A /\ y e. ~P A ) -> ( x C_ y \/ y C_ x ) ) ) )
30 29 com3l 
 |-  ( [C.] Or Y -> ( ( x e. ~P A /\ y e. ~P A ) -> ( ( ( A \ x ) e. Y /\ ( A \ y ) e. Y ) -> ( x C_ y \/ y C_ x ) ) ) )
31 30 impd 
 |-  ( [C.] Or Y -> ( ( ( x e. ~P A /\ y e. ~P A ) /\ ( ( A \ x ) e. Y /\ ( A \ y ) e. Y ) ) -> ( x C_ y \/ y C_ x ) ) )
32 9 31 syl5 
 |-  ( [C.] Or Y -> ( ( x e. { u e. ~P A | ( A \ u ) e. Y } /\ y e. { u e. ~P A | ( A \ u ) e. Y } ) -> ( x C_ y \/ y C_ x ) ) )
33 32 ralrimivv 
 |-  ( [C.] Or Y -> A. x e. { u e. ~P A | ( A \ u ) e. Y } A. y e. { u e. ~P A | ( A \ u ) e. Y } ( x C_ y \/ y C_ x ) )
34 sorpss 
 |-  ( [C.] Or { u e. ~P A | ( A \ u ) e. Y } <-> A. x e. { u e. ~P A | ( A \ u ) e. Y } A. y e. { u e. ~P A | ( A \ u ) e. Y } ( x C_ y \/ y C_ x ) )
35 33 34 sylibr 
 |-  ( [C.] Or Y -> [C.] Or { u e. ~P A | ( A \ u ) e. Y } )