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

Metamath Proof Explorer

Theorem iundifdif

Description: The intersection of a set is the complement of the union of the complements. TODO: shorten using iundifdifd . (Contributed by Thierry Arnoux, 4-Sep-2016)

Ref Expression
Hypotheses iundifdif.o 
|- O e. _V
iundifdif.2 
|- A C_ ~P O
Assertion iundifdif 
|- ( A =/= (/) -> |^| A = ( O \ U_ x e. A ( O \ x ) ) )

Proof

Step Hyp Ref Expression
1 iundifdif.o 
 |-  O e. _V
2 iundifdif.2 
 |-  A C_ ~P O
3 iundif2 
 |-  U_ x e. A ( O \ x ) = ( O \ |^|_ x e. A x )
4 intiin 
 |-  |^| A = |^|_ x e. A x
5 4 difeq2i 
 |-  ( O \ |^| A ) = ( O \ |^|_ x e. A x )
6 3 5 eqtr4i 
 |-  U_ x e. A ( O \ x ) = ( O \ |^| A )
7 6 difeq2i 
 |-  ( O \ U_ x e. A ( O \ x ) ) = ( O \ ( O \ |^| A ) )
8 2 jctl 
 |-  ( A =/= (/) -> ( A C_ ~P O /\ A =/= (/) ) )
9 intssuni2 
 |-  ( ( A C_ ~P O /\ A =/= (/) ) -> |^| A C_ U. ~P O )
10 unipw 
 |-  U. ~P O = O
11 10 sseq2i 
 |-  ( |^| A C_ U. ~P O <-> |^| A C_ O )
12 11 biimpi 
 |-  ( |^| A C_ U. ~P O -> |^| A C_ O )
13 8 9 12 3syl 
 |-  ( A =/= (/) -> |^| A C_ O )
14 dfss4 
 |-  ( |^| A C_ O <-> ( O \ ( O \ |^| A ) ) = |^| A )
15 13 14 sylib 
 |-  ( A =/= (/) -> ( O \ ( O \ |^| A ) ) = |^| A )
16 7 15 eqtr2id 
 |-  ( A =/= (/) -> |^| A = ( O \ U_ x e. A ( O \ x ) ) )