Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  inelsros Structured version   Visualization version   Unicode version
Theorem inelsros 30241
Description: A semi-ring of sets is closed under union. (Contributed by Thierry Arnoux, 18-Jul-2020.)
Hypothesis
Ref Expression
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
Ref Expression
inelsros |- ( ( S e. N /\ A e. S /\ B e. S ) -> ( A i^i B ) e. S )
Distinct variable groups:   t, s, x, y   O, s   S, s, x, y, z   x, A, y, z   y, B, z
Allowed substitution hints:   A( t, s)   B( x, t, s)   S( t)   N( x, y, z, t, s)   O( x, y, z, t)
Proof of Theorem inelsros
StepHypRef Expression
1 simp2 1062 . . 3 |- ( ( S e. N /\ A e. S /\ B e. S ) -> A e. S )
2 simp3 1063 . . 3 |- ( ( S e. N /\ A e. S /\ B e. S ) -> B e. S )
3 issros.1 . . . . . 6 |- 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 ) ) ) }
43issros 30238 . . . . 5 |- ( 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 ) ) ) )
54simp3bi 1078 . . . 4 |- ( 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 ) ) )
653ad2ant1 1082 . . 3 |- ( ( 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 3807 . . . . . 6 |- ( x = A -> ( x i^i y ) = ( A i^i y ) )
87eleq1d 2686 . . . . 5 |- ( x = A -> ( ( x i^i y ) e. S <-> ( A i^i y ) e. S ) )
9 difeq1 3721 . . . . . . . 8 |- ( x = A -> ( x \ y ) = ( A \ y ) )
109eqeq1d 2624 . . . . . . 7 |- ( x = A -> ( ( x \ y ) = U. z <-> ( A \ y ) = U. z ) )
11103anbi3d 1405 . . . . . 6 |- ( 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 ) ) )
1211rexbidv 3052 . . . . 5 |- ( 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 ) ) )
138, 12anbi12d 747 . . . 4 |- ( 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 3808 . . . . . 6 |- ( y = B -> ( A i^i y ) = ( A i^i B ) )
1514eleq1d 2686 . . . . 5 |- ( y = B -> ( ( A i^i y ) e. S <-> ( A i^i B ) e. S ) )
16 difeq2 3722 . . . . . . . 8 |- ( y = B -> ( A \ y ) = ( A \ B ) )
1716eqeq1d 2624 . . . . . . 7 |- ( y = B -> ( ( A \ y ) = U. z <-> ( A \ B ) = U. z ) )
18173anbi3d 1405 . . . . . 6 |- ( 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 ) ) )
1918rexbidv 3052 . . . . 5 |- ( 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 ) ) )
2015, 19anbi12d 747 . . . 4 |- ( 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 ) ) ) )
2113, 20rspc2va 3323 . . 3 |- ( ( ( 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 ) ) )
221, 2, 6, 21syl21anc 1325 . 2 |- ( ( 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 ) ) )
2322simpld 475 1 |- ( ( S e. N /\ A e. S /\ B e. S ) -> ( A i^i B ) e. S )
Colors of variables: wff setvar class
Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   A.wral 2912   E.wrex 2913   {crab 2916   \ cdif 3571   i^i cin 3573   (/)c0 3915   ~Pcpw 4158   U.cuni 4436  Disj wdisj 4620   Fincfn 7955
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-in 3581  df-ss 3588  df-pw 4160
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator