Metamath Proof Explorer

Theorem diffiunisros

Description: In semiring of sets, complements can be written as finite disjoint unions. (Contributed by Thierry Arnoux, 18-Jul-2020)

Ref Expression
Hypothesis issros.1 
|- N = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s A. y e. s ( ( x i^i y ) e. s /\ E. z e. ~P s ( z e. Fin /\ Disj_ t e. z t /\ ( x \ y ) = U. z ) ) ) }
Assertion diffiunisros 
|- ( ( S e. N /\ A e. S /\ B e. S ) -> E. z e. ~P S ( z e. Fin /\ Disj_ t e. z t /\ ( A \ B ) = U. z ) )

Proof

Step Hyp Ref Expression
1 issros.1 
 |-  N = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s A. y e. s ( ( x i^i y ) e. s /\ E. z e. ~P s ( z e. Fin /\ Disj_ t e. z t /\ ( x \ y ) = U. z ) ) ) }
2 simp2 
 |-  ( ( S e. N /\ A e. S /\ B e. S ) -> A e. S )
3 simp3 
 |-  ( ( S e. N /\ A e. S /\ B e. S ) -> B e. S )
4 1 issros 
 |-  ( S e. N <-> ( S e. ~P ~P O /\ (/) e. S /\ A. x e. S A. y e. S ( ( x i^i y ) e. S /\ E. z e. ~P S ( z e. Fin /\ Disj_ t e. z t /\ ( x \ y ) = U. z ) ) ) )
5 4 simp3bi 
 |-  ( S e. N -> A. x e. S A. y e. S ( ( x i^i y ) e. S /\ E. z e. ~P S ( z e. Fin /\ Disj_ t e. z t /\ ( x \ y ) = U. z ) ) )
6 5 3ad2ant1 
 |-  ( ( S e. N /\ A e. S /\ B e. S ) -> A. x e. S A. y e. S ( ( x i^i y ) e. S /\ E. z e. ~P S ( z e. Fin /\ Disj_ t e. z t /\ ( x \ y ) = U. z ) ) )
7 ineq1 
 |-  ( x = A -> ( x i^i y ) = ( A i^i y ) )
8 7 eleq1d 
 |-  ( x = A -> ( ( x i^i y ) e. S <-> ( A i^i y ) e. S ) )
9 difeq1 
 |-  ( x = A -> ( x \ y ) = ( A \ y ) )
10 9 eqeq1d 
 |-  ( x = A -> ( ( x \ y ) = U. z <-> ( A \ y ) = U. z ) )
11 10 3anbi3d 
 |-  ( x = A -> ( ( z e. Fin /\ Disj_ t e. z t /\ ( x \ y ) = U. z ) <-> ( z e. Fin /\ Disj_ t e. z t /\ ( A \ y ) = U. z ) ) )
12 11 rexbidv 
 |-  ( x = A -> ( E. z e. ~P S ( z e. Fin /\ Disj_ t e. z t /\ ( x \ y ) = U. z ) <-> E. z e. ~P S ( z e. Fin /\ Disj_ t e. z t /\ ( A \ y ) = U. z ) ) )
13 8 12 anbi12d 
 |-  ( x = A -> ( ( ( x i^i y ) e. S /\ E. z e. ~P S ( z e. Fin /\ Disj_ t e. z t /\ ( x \ y ) = U. z ) ) <-> ( ( A i^i y ) e. S /\ E. z e. ~P S ( z e. Fin /\ Disj_ t e. z t /\ ( A \ y ) = U. z ) ) ) )
14 ineq2 
 |-  ( y = B -> ( A i^i y ) = ( A i^i B ) )
15 14 eleq1d 
 |-  ( y = B -> ( ( A i^i y ) e. S <-> ( A i^i B ) e. S ) )
16 difeq2 
 |-  ( y = B -> ( A \ y ) = ( A \ B ) )
17 16 eqeq1d 
 |-  ( y = B -> ( ( A \ y ) = U. z <-> ( A \ B ) = U. z ) )
18 17 3anbi3d 
 |-  ( y = B -> ( ( z e. Fin /\ Disj_ t e. z t /\ ( A \ y ) = U. z ) <-> ( z e. Fin /\ Disj_ t e. z t /\ ( A \ B ) = U. z ) ) )
19 18 rexbidv 
 |-  ( y = B -> ( E. z e. ~P S ( z e. Fin /\ Disj_ t e. z t /\ ( A \ y ) = U. z ) <-> E. z e. ~P S ( z e. Fin /\ Disj_ t e. z t /\ ( A \ B ) = U. z ) ) )
20 15 19 anbi12d 
 |-  ( y = B -> ( ( ( A i^i y ) e. S /\ E. z e. ~P S ( z e. Fin /\ Disj_ t e. z t /\ ( A \ y ) = U. z ) ) <-> ( ( A i^i B ) e. S /\ E. z e. ~P S ( z e. Fin /\ Disj_ t e. z t /\ ( A \ B ) = U. z ) ) ) )
21 13 20 rspc2va 
 |-  ( ( ( A e. S /\ B e. S ) /\ A. x e. S A. y e. S ( ( x i^i y ) e. S /\ E. z e. ~P S ( z e. Fin /\ Disj_ t e. z t /\ ( x \ y ) = U. z ) ) ) -> ( ( A i^i B ) e. S /\ E. z e. ~P S ( z e. Fin /\ Disj_ t e. z t /\ ( A \ B ) = U. z ) ) )
22 2 3 6 21 syl21anc 
 |-  ( ( S e. N /\ A e. S /\ B e. S ) -> ( ( A i^i B ) e. S /\ E. z e. ~P S ( z e. Fin /\ Disj_ t e. z t /\ ( A \ B ) = U. z ) ) )
23 22 simprd 
 |-  ( ( S e. N /\ A e. S /\ B e. S ) -> E. z e. ~P S ( z e. Fin /\ Disj_ t e. z t /\ ( A \ B ) = U. z ) )