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 ) ) )