Metamath Proof Explorer

Theorem rossros

Description: Rings of sets are semirings of sets. (Contributed by Thierry Arnoux, 18-Jul-2020)

Ref Expression
Hypotheses rossros.q 
|- Q = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s A. y e. s ( ( x u. y ) e. s /\ ( x \ y ) e. s ) ) }
rossros.n 
|- 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 rossros 
|- ( S e. Q -> S e. N )

Proof

Step Hyp Ref Expression
1 rossros.q 
 |-  Q = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s A. y e. s ( ( x u. y ) e. s /\ ( x \ y ) e. s ) ) }
2 rossros.n 
 |-  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 ) ) ) }
3 1 rossspw 
 |-  ( S e. Q -> S C_ ~P O )
4 elpwg 
 |-  ( S e. Q -> ( S e. ~P ~P O <-> S C_ ~P O ) )
5 3 4 mpbird 
 |-  ( S e. Q -> S e. ~P ~P O )
6 1 0elros 
 |-  ( S e. Q -> (/) e. S )
7 uneq1 
 |-  ( u = x -> ( u u. v ) = ( x u. v ) )
8 7 eleq1d 
 |-  ( u = x -> ( ( u u. v ) e. s <-> ( x u. v ) e. s ) )
9 difeq1 
 |-  ( u = x -> ( u \ v ) = ( x \ v ) )
10 9 eleq1d 
 |-  ( u = x -> ( ( u \ v ) e. s <-> ( x \ v ) e. s ) )
11 8 10 anbi12d 
 |-  ( u = x -> ( ( ( u u. v ) e. s /\ ( u \ v ) e. s ) <-> ( ( x u. v ) e. s /\ ( x \ v ) e. s ) ) )
12 uneq2 
 |-  ( v = y -> ( x u. v ) = ( x u. y ) )
13 12 eleq1d 
 |-  ( v = y -> ( ( x u. v ) e. s <-> ( x u. y ) e. s ) )
14 difeq2 
 |-  ( v = y -> ( x \ v ) = ( x \ y ) )
15 14 eleq1d 
 |-  ( v = y -> ( ( x \ v ) e. s <-> ( x \ y ) e. s ) )
16 13 15 anbi12d 
 |-  ( v = y -> ( ( ( x u. v ) e. s /\ ( x \ v ) e. s ) <-> ( ( x u. y ) e. s /\ ( x \ y ) e. s ) ) )
17 11 16 cbvral2vw 
 |-  ( A. u e. s A. v e. s ( ( u u. v ) e. s /\ ( u \ v ) e. s ) <-> A. x e. s A. y e. s ( ( x u. y ) e. s /\ ( x \ y ) e. s ) )
18 17 anbi2i 
 |-  ( ( (/) e. s /\ A. u e. s A. v e. s ( ( u u. v ) e. s /\ ( u \ v ) e. s ) ) <-> ( (/) e. s /\ A. x e. s A. y e. s ( ( x u. y ) e. s /\ ( x \ y ) e. s ) ) )
19 18 rabbii 
 |-  { s e. ~P ~P O | ( (/) e. s /\ A. u e. s A. v e. s ( ( u u. v ) e. s /\ ( u \ v ) e. s ) ) } = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s A. y e. s ( ( x u. y ) e. s /\ ( x \ y ) e. s ) ) }
20 1 19 eqtr4i 
 |-  Q = { s e. ~P ~P O | ( (/) e. s /\ A. u e. s A. v e. s ( ( u u. v ) e. s /\ ( u \ v ) e. s ) ) }
21 20 inelros 
 |-  ( ( S e. Q /\ x e. S /\ y e. S ) -> ( x i^i y ) e. S )
22 21 3expb 
 |-  ( ( S e. Q /\ ( x e. S /\ y e. S ) ) -> ( x i^i y ) e. S )
23 20 difelros 
 |-  ( ( S e. Q /\ x e. S /\ y e. S ) -> ( x \ y ) e. S )
24 23 3expb 
 |-  ( ( S e. Q /\ ( x e. S /\ y e. S ) ) -> ( x \ y ) e. S )
25 24 snssd 
 |-  ( ( S e. Q /\ ( x e. S /\ y e. S ) ) -> { ( x \ y ) } C_ S )
26 snex 
 |-  { ( x \ y ) } e. _V
27 26 elpw 
 |-  ( { ( x \ y ) } e. ~P S <-> { ( x \ y ) } C_ S )
28 25 27 sylibr 
 |-  ( ( S e. Q /\ ( x e. S /\ y e. S ) ) -> { ( x \ y ) } e. ~P S )
29 snfi 
 |-  { ( x \ y ) } e. Fin
30 29 a1i 
 |-  ( ( S e. Q /\ ( x e. S /\ y e. S ) ) -> { ( x \ y ) } e. Fin )
31 disjxsn 
 |-  Disj_ t e. { ( x \ y ) } t
32 31 a1i 
 |-  ( ( S e. Q /\ ( x e. S /\ y e. S ) ) -> Disj_ t e. { ( x \ y ) } t )
33 unisng 
 |-  ( ( x \ y ) e. S -> U. { ( x \ y ) } = ( x \ y ) )
34 24 33 syl 
 |-  ( ( S e. Q /\ ( x e. S /\ y e. S ) ) -> U. { ( x \ y ) } = ( x \ y ) )
35 34 eqcomd 
 |-  ( ( S e. Q /\ ( x e. S /\ y e. S ) ) -> ( x \ y ) = U. { ( x \ y ) } )
36 eleq1 
 |-  ( z = { ( x \ y ) } -> ( z e. Fin <-> { ( x \ y ) } e. Fin ) )
37 disjeq1 
 |-  ( z = { ( x \ y ) } -> ( Disj_ t e. z t <-> Disj_ t e. { ( x \ y ) } t ) )
38 unieq 
 |-  ( z = { ( x \ y ) } -> U. z = U. { ( x \ y ) } )
39 38 eqeq2d 
 |-  ( z = { ( x \ y ) } -> ( ( x \ y ) = U. z <-> ( x \ y ) = U. { ( x \ y ) } ) )
40 36 37 39 3anbi123d 
 |-  ( z = { ( x \ y ) } -> ( ( z e. Fin /\ Disj_ t e. z t /\ ( x \ y ) = U. z ) <-> ( { ( x \ y ) } e. Fin /\ Disj_ t e. { ( x \ y ) } t /\ ( x \ y ) = U. { ( x \ y ) } ) ) )
41 40 rspcev 
 |-  ( ( { ( x \ y ) } e. ~P S /\ ( { ( x \ y ) } e. Fin /\ Disj_ t e. { ( x \ y ) } t /\ ( x \ y ) = U. { ( x \ y ) } ) ) -> E. z e. ~P S ( z e. Fin /\ Disj_ t e. z t /\ ( x \ y ) = U. z ) )
42 28 30 32 35 41 syl13anc 
 |-  ( ( S e. Q /\ ( x e. S /\ y e. S ) ) -> E. z e. ~P S ( z e. Fin /\ Disj_ t e. z t /\ ( x \ y ) = U. z ) )
43 22 42 jca 
 |-  ( ( S e. Q /\ ( x e. S /\ 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 ) ) )
44 43 ralrimivva 
 |-  ( S e. Q -> 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 ) ) )
45 5 6 44 3jca 
 |-  ( S e. Q -> ( 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 ) ) ) )
46 2 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 ) ) ) )
47 45 46 sylibr 
 |-  ( S e. Q -> S e. N )