This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iundifdifd

Description: The intersection of a set is the complement of the union of the complements. (Contributed by Thierry Arnoux, 19-Dec-2016)

Ref Expression
Assertion iundifdifd 
|- ( A C_ ~P O -> ( A =/= (/) -> |^| A = ( O \ U_ x e. A ( O \ x ) ) ) )

Proof

Step Hyp Ref Expression
1 iundif2 
 |-  U_ x e. A ( O \ x ) = ( O \ |^|_ x e. A x )
2 intiin 
 |-  |^| A = |^|_ x e. A x
3 2 difeq2i 
 |-  ( O \ |^| A ) = ( O \ |^|_ x e. A x )
4 1 3 eqtr4i 
 |-  U_ x e. A ( O \ x ) = ( O \ |^| A )
5 4 difeq2i 
 |-  ( O \ U_ x e. A ( O \ x ) ) = ( O \ ( O \ |^| A ) )
6 intssuni2 
 |-  ( ( A C_ ~P O /\ A =/= (/) ) -> |^| A C_ U. ~P O )
7 unipw 
 |-  U. ~P O = O
8 6 7 sseqtrdi 
 |-  ( ( A C_ ~P O /\ A =/= (/) ) -> |^| A C_ O )
9 dfss4 
 |-  ( |^| A C_ O <-> ( O \ ( O \ |^| A ) ) = |^| A )
10 8 9 sylib 
 |-  ( ( A C_ ~P O /\ A =/= (/) ) -> ( O \ ( O \ |^| A ) ) = |^| A )
11 5 10 eqtr2id 
 |-  ( ( A C_ ~P O /\ A =/= (/) ) -> |^| A = ( O \ U_ x e. A ( O \ x ) ) )
12 11 ex 
 |-  ( A C_ ~P O -> ( A =/= (/) -> |^| A = ( O \ U_ x e. A ( O \ x ) ) ) )