Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  salexct Structured version   Visualization version   Unicode version

Theorem salexct 38230
Description: An example of non trivial sigma-algebra: the collection of all subsets which either are countable or have countable complement. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
Hypotheses
Ref Expression
salexct.a  |-  ( ph  ->  A  e.  V )
salexct.b  |-  S  =  { x  e.  ~P A  |  ( x  ~<_  om  \/  ( A  \  x )  ~<_  om ) }
Assertion
Ref Expression
salexct  |-  ( ph  ->  S  e. SAlg )
Distinct variable groups:    x, A    x, S    ph, x
Allowed substitution hint:    V( x)

Proof of Theorem salexct
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 salexct.b . . 3  |-  S  =  { x  e.  ~P A  |  ( x  ~<_  om  \/  ( A  \  x )  ~<_  om ) }
2 salexct.a . . . . 5  |-  ( ph  ->  A  e.  V )
3 pwexg 4600 . . . . 5  |-  ( A  e.  V  ->  ~P A  e.  _V )
42, 3syl 17 . . . 4  |-  ( ph  ->  ~P A  e.  _V )
5 rabexg 4566 . . . 4  |-  ( ~P A  e.  _V  ->  { x  e.  ~P A  |  ( x  ~<_  om  \/  ( A  \  x )  ~<_  om ) }  e.  _V )
64, 5syl 17 . . 3  |-  ( ph  ->  { x  e.  ~P A  |  ( x  ~<_  om  \/  ( A  \  x )  ~<_  om ) }  e.  _V )
71, 6syl5eqel 2543 . 2  |-  ( ph  ->  S  e.  _V )
8 0elpw 4585 . . . . 5  |-  (/)  e.  ~P A
98a1i 11 . . . 4  |-  ( ph  -> 
(/)  e.  ~P A
)
10 0fin 7824 . . . . . . 7  |-  (/)  e.  Fin
11 fict 8183 . . . . . . 7  |-  ( (/)  e.  Fin  ->  (/)  ~<_  om )
1210, 11ax-mp 5 . . . . . 6  |-  (/)  ~<_  om
1312orci 396 . . . . 5  |-  ( (/)  ~<_  om  \/  ( A  \  (/) )  ~<_  om )
1413a1i 11 . . . 4  |-  ( ph  ->  ( (/)  ~<_  om  \/  ( A  \  (/) )  ~<_  om )
)
159, 14jca 539 . . 3  |-  ( ph  ->  ( (/)  e.  ~P A  /\  ( (/)  ~<_  om  \/  ( A  \  (/) )  ~<_  om ) ) )
16 breq1 4418 . . . . 5  |-  ( x  =  (/)  ->  ( x  ~<_  om  <->  (/)  ~<_  om ) )
17 difeq2 3556 . . . . . 6  |-  ( x  =  (/)  ->  ( A 
\  x )  =  ( A  \  (/) ) )
1817breq1d 4425 . . . . 5  |-  ( x  =  (/)  ->  ( ( A  \  x )  ~<_  om  <->  ( A  \  (/) )  ~<_  om ) )
1916, 18orbi12d 721 . . . 4  |-  ( x  =  (/)  ->  ( ( x  ~<_  om  \/  ( A  \  x )  ~<_  om )  <->  ( (/)  ~<_  om  \/  ( A  \  (/) )  ~<_  om ) ) )
2019, 1elrab2 3209 . . 3  |-  ( (/)  e.  S  <->  ( (/)  e.  ~P A  /\  ( (/)  ~<_  om  \/  ( A  \  (/) )  ~<_  om ) ) )
2115, 20sylibr 217 . 2  |-  ( ph  -> 
(/)  e.  S )
22 snidg 4005 . . . . . 6  |-  ( y  e.  A  ->  y  e.  { y } )
23 snelpwi 4658 . . . . . . . 8  |-  ( y  e.  A  ->  { y }  e.  ~P A
)
24 snfi 7675 . . . . . . . . . . 11  |-  { y }  e.  Fin
25 fict 8183 . . . . . . . . . . 11  |-  ( { y }  e.  Fin  ->  { y }  ~<_  om )
2624, 25ax-mp 5 . . . . . . . . . 10  |-  { y }  ~<_  om
2726orci 396 . . . . . . . . 9  |-  ( { y }  ~<_  om  \/  ( A  \  { y } )  ~<_  om )
2827a1i 11 . . . . . . . 8  |-  ( y  e.  A  ->  ( { y }  ~<_  om  \/  ( A  \  { y } )  ~<_  om )
)
2923, 28jca 539 . . . . . . 7  |-  ( y  e.  A  ->  ( { y }  e.  ~P A  /\  ( { y }  ~<_  om  \/  ( A  \  { y } )  ~<_  om )
) )
30 breq1 4418 . . . . . . . . 9  |-  ( x  =  { y }  ->  ( x  ~<_  om  <->  { y }  ~<_  om )
)
31 difeq2 3556 . . . . . . . . . 10  |-  ( x  =  { y }  ->  ( A  \  x )  =  ( A  \  { y } ) )
3231breq1d 4425 . . . . . . . . 9  |-  ( x  =  { y }  ->  ( ( A 
\  x )  ~<_  om  <->  ( A  \  { y } )  ~<_  om )
)
3330, 32orbi12d 721 . . . . . . . 8  |-  ( x  =  { y }  ->  ( ( x  ~<_  om  \/  ( A 
\  x )  ~<_  om )  <->  ( { y }  ~<_  om  \/  ( A  \  { y } )  ~<_  om ) ) )
3433, 1elrab2 3209 . . . . . . 7  |-  ( { y }  e.  S  <->  ( { y }  e.  ~P A  /\  ( { y }  ~<_  om  \/  ( A  \  { y } )  ~<_  om )
) )
3529, 34sylibr 217 . . . . . 6  |-  ( y  e.  A  ->  { y }  e.  S )
36 elunii 4216 . . . . . 6  |-  ( ( y  e.  { y }  /\  { y }  e.  S )  ->  y  e.  U. S )
3722, 35, 36syl2anc 671 . . . . 5  |-  ( y  e.  A  ->  y  e.  U. S )
3837rgen 2758 . . . 4  |-  A. y  e.  A  y  e.  U. S
39 dfss3 3433 . . . 4  |-  ( A 
C_  U. S  <->  A. y  e.  A  y  e.  U. S )
4038, 39mpbir 214 . . 3  |-  A  C_  U. S
41 ssrab2 3525 . . . . . 6  |-  { x  e.  ~P A  |  ( x  ~<_  om  \/  ( A  \  x )  ~<_  om ) }  C_  ~P A
421, 41eqsstri 3473 . . . . 5  |-  S  C_  ~P A
4342unissi 4234 . . . 4  |-  U. S  C_ 
U. ~P A
44 unipw 4663 . . . 4  |-  U. ~P A  =  A
4543, 44sseqtri 3475 . . 3  |-  U. S  C_  A
4640, 45eqssi 3459 . 2  |-  A  = 
U. S
47 difssd 3572 . . . . . . 7  |-  ( ph  ->  ( A  \  x
)  C_  A )
482, 47ssexd 4563 . . . . . . . 8  |-  ( ph  ->  ( A  \  x
)  e.  _V )
49 elpwg 3970 . . . . . . . 8  |-  ( ( A  \  x )  e.  _V  ->  (
( A  \  x
)  e.  ~P A  <->  ( A  \  x ) 
C_  A ) )
5048, 49syl 17 . . . . . . 7  |-  ( ph  ->  ( ( A  \  x )  e.  ~P A 
<->  ( A  \  x
)  C_  A )
)
5147, 50mpbird 240 . . . . . 6  |-  ( ph  ->  ( A  \  x
)  e.  ~P A
)
5251ad2antrr 737 . . . . 5  |-  ( ( ( ph  /\  x  e.  S )  /\  x  ~<_  om )  ->  ( A 
\  x )  e. 
~P A )
5342sseli 3439 . . . . . . . . . 10  |-  ( x  e.  S  ->  x  e.  ~P A )
54 elpwi 3971 . . . . . . . . . 10  |-  ( x  e.  ~P A  ->  x  C_  A )
5553, 54syl 17 . . . . . . . . 9  |-  ( x  e.  S  ->  x  C_  A )
56 dfss4 3688 . . . . . . . . 9  |-  ( x 
C_  A  <->  ( A  \  ( A  \  x
) )  =  x )
5755, 56sylib 201 . . . . . . . 8  |-  ( x  e.  S  ->  ( A  \  ( A  \  x ) )  =  x )
5857ad2antlr 738 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  S )  /\  x  ~<_  om )  ->  ( A 
\  ( A  \  x ) )  =  x )
59 simpr 467 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  S )  /\  x  ~<_  om )  ->  x  ~<_  om )
6058, 59eqbrtrd 4436 . . . . . 6  |-  ( ( ( ph  /\  x  e.  S )  /\  x  ~<_  om )  ->  ( A 
\  ( A  \  x ) )  ~<_  om )
61 olc 390 . . . . . 6  |-  ( ( A  \  ( A 
\  x ) )  ~<_  om  ->  ( ( A  \  x )  ~<_  om  \/  ( A  \ 
( A  \  x
) )  ~<_  om )
)
6260, 61syl 17 . . . . 5  |-  ( ( ( ph  /\  x  e.  S )  /\  x  ~<_  om )  ->  ( ( A  \  x )  ~<_  om  \/  ( A 
\  ( A  \  x ) )  ~<_  om ) )
6352, 62jca 539 . . . 4  |-  ( ( ( ph  /\  x  e.  S )  /\  x  ~<_  om )  ->  ( ( A  \  x )  e.  ~P A  /\  ( ( A  \  x )  ~<_  om  \/  ( A  \  ( A  \  x ) )  ~<_  om ) ) )
64 breq1 4418 . . . . . 6  |-  ( y  =  ( A  \  x )  ->  (
y  ~<_  om  <->  ( A  \  x )  ~<_  om )
)
65 difeq2 3556 . . . . . . 7  |-  ( y  =  ( A  \  x )  ->  ( A  \  y )  =  ( A  \  ( A  \  x ) ) )
6665breq1d 4425 . . . . . 6  |-  ( y  =  ( A  \  x )  ->  (
( A  \  y
)  ~<_  om  <->  ( A  \ 
( A  \  x
) )  ~<_  om )
)
6764, 66orbi12d 721 . . . . 5  |-  ( y  =  ( A  \  x )  ->  (
( y  ~<_  om  \/  ( A  \  y
)  ~<_  om )  <->  ( ( A  \  x )  ~<_  om  \/  ( A  \ 
( A  \  x
) )  ~<_  om )
) )
68 breq1 4418 . . . . . . . 8  |-  ( x  =  y  ->  (
x  ~<_  om  <->  y  ~<_  om )
)
69 difeq2 3556 . . . . . . . . 9  |-  ( x  =  y  ->  ( A  \  x )  =  ( A  \  y
) )
7069breq1d 4425 . . . . . . . 8  |-  ( x  =  y  ->  (
( A  \  x
)  ~<_  om  <->  ( A  \ 
y )  ~<_  om )
)
7168, 70orbi12d 721 . . . . . . 7  |-  ( x  =  y  ->  (
( x  ~<_  om  \/  ( A  \  x
)  ~<_  om )  <->  ( y  ~<_  om  \/  ( A  \ 
y )  ~<_  om )
) )
7271cbvrabv 3055 . . . . . 6  |-  { x  e.  ~P A  |  ( x  ~<_  om  \/  ( A  \  x )  ~<_  om ) }  =  {
y  e.  ~P A  |  ( y  ~<_  om  \/  ( A  \ 
y )  ~<_  om ) }
731, 72eqtri 2483 . . . . 5  |-  S  =  { y  e.  ~P A  |  ( y  ~<_  om  \/  ( A  \ 
y )  ~<_  om ) }
7467, 73elrab2 3209 . . . 4  |-  ( ( A  \  x )  e.  S  <->  ( ( A  \  x )  e. 
~P A  /\  (
( A  \  x
)  ~<_  om  \/  ( A  \  ( A  \  x ) )  ~<_  om ) ) )
7563, 74sylibr 217 . . 3  |-  ( ( ( ph  /\  x  e.  S )  /\  x  ~<_  om )  ->  ( A 
\  x )  e.  S )
7651ad2antrr 737 . . . . 5  |-  ( ( ( ph  /\  x  e.  S )  /\  -.  x  ~<_  om )  ->  ( A  \  x )  e. 
~P A )
771rabeq2i 3053 . . . . . . . . . . 11  |-  ( x  e.  S  <->  ( x  e.  ~P A  /\  (
x  ~<_  om  \/  ( A  \  x )  ~<_  om ) ) )
7877biimpi 199 . . . . . . . . . 10  |-  ( x  e.  S  ->  (
x  e.  ~P A  /\  ( x  ~<_  om  \/  ( A  \  x
)  ~<_  om ) ) )
7978simprd 469 . . . . . . . . 9  |-  ( x  e.  S  ->  (
x  ~<_  om  \/  ( A  \  x )  ~<_  om ) )
8079adantl 472 . . . . . . . 8  |-  ( (
ph  /\  x  e.  S )  ->  (
x  ~<_  om  \/  ( A  \  x )  ~<_  om ) )
8180adantr 471 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  S )  /\  -.  x  ~<_  om )  ->  (
x  ~<_  om  \/  ( A  \  x )  ~<_  om ) )
82 simpr 467 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  S )  /\  -.  x  ~<_  om )  ->  -.  x  ~<_  om )
83 pm2.53 379 . . . . . . 7  |-  ( ( x  ~<_  om  \/  ( A  \  x )  ~<_  om )  ->  ( -.  x  ~<_  om  ->  ( A 
\  x )  ~<_  om ) )
8481, 82, 83sylc 62 . . . . . 6  |-  ( ( ( ph  /\  x  e.  S )  /\  -.  x  ~<_  om )  ->  ( A  \  x )  ~<_  om )
85 orc 391 . . . . . 6  |-  ( ( A  \  x )  ~<_  om  ->  ( ( A  \  x )  ~<_  om  \/  ( A  \ 
( A  \  x
) )  ~<_  om )
)
8684, 85syl 17 . . . . 5  |-  ( ( ( ph  /\  x  e.  S )  /\  -.  x  ~<_  om )  ->  (
( A  \  x
)  ~<_  om  \/  ( A  \  ( A  \  x ) )  ~<_  om ) )
8776, 86jca 539 . . . 4  |-  ( ( ( ph  /\  x  e.  S )  /\  -.  x  ~<_  om )  ->  (
( A  \  x
)  e.  ~P A  /\  ( ( A  \  x )  ~<_  om  \/  ( A  \  ( A  \  x ) )  ~<_  om ) ) )
8887, 74sylibr 217 . . 3  |-  ( ( ( ph  /\  x  e.  S )  /\  -.  x  ~<_  om )  ->  ( A  \  x )  e.  S )
8975, 88pm2.61dan 805 . 2  |-  ( (
ph  /\  x  e.  S )  ->  ( A  \  x )  e.  S )
90 elpwi 3971 . . . . . . . . . . . 12  |-  ( x  e.  ~P S  ->  x  C_  S )
9190adantr 471 . . . . . . . . . . 11  |-  ( ( x  e.  ~P S  /\  y  e.  x
)  ->  x  C_  S
)
92 simpr 467 . . . . . . . . . . 11  |-  ( ( x  e.  ~P S  /\  y  e.  x
)  ->  y  e.  x )
9391, 92sseldd 3444 . . . . . . . . . 10  |-  ( ( x  e.  ~P S  /\  y  e.  x
)  ->  y  e.  S )
9442sseli 3439 . . . . . . . . . . 11  |-  ( y  e.  S  ->  y  e.  ~P A )
95 elpwi 3971 . . . . . . . . . . 11  |-  ( y  e.  ~P A  -> 
y  C_  A )
9694, 95syl 17 . . . . . . . . . 10  |-  ( y  e.  S  ->  y  C_  A )
9793, 96syl 17 . . . . . . . . 9  |-  ( ( x  e.  ~P S  /\  y  e.  x
)  ->  y  C_  A )
9897ralrimiva 2813 . . . . . . . 8  |-  ( x  e.  ~P S  ->  A. y  e.  x  y  C_  A )
99 unissb 4242 . . . . . . . 8  |-  ( U. x  C_  A  <->  A. y  e.  x  y  C_  A )
10098, 99sylibr 217 . . . . . . 7  |-  ( x  e.  ~P S  ->  U. x  C_  A )
101 vex 3059 . . . . . . . . 9  |-  x  e. 
_V
102101uniex 6613 . . . . . . . 8  |-  U. x  e.  _V
103102elpw 3968 . . . . . . 7  |-  ( U. x  e.  ~P A  <->  U. x  C_  A )
104100, 103sylibr 217 . . . . . 6  |-  ( x  e.  ~P S  ->  U. x  e.  ~P A )
105104adantr 471 . . . . 5  |-  ( ( x  e.  ~P S  /\  x  ~<_  om )  ->  U. x  e.  ~P A )
106 id 22 . . . . . . . 8  |-  ( ( x  ~<_  om  /\  A. y  e.  x  y  ~<_  om )  ->  ( x  ~<_  om  /\  A. y  e.  x  y  ~<_  om ) )
107106adantll 725 . . . . . . 7  |-  ( ( ( x  e.  ~P S  /\  x  ~<_  om )  /\  A. y  e.  x  y  ~<_  om )  ->  (
x  ~<_  om  /\  A. y  e.  x  y  ~<_  om )
)
108 unictb 9025 . . . . . . 7  |-  ( ( x  ~<_  om  /\  A. y  e.  x  y  ~<_  om )  ->  U. x  ~<_  om )
109 orc 391 . . . . . . 7  |-  ( U. x  ~<_  om  ->  ( U. x  ~<_  om  \/  ( A  \  U. x )  ~<_  om ) )
110107, 108, 1093syl 18 . . . . . 6  |-  ( ( ( x  e.  ~P S  /\  x  ~<_  om )  /\  A. y  e.  x  y  ~<_  om )  ->  ( U. x  ~<_  om  \/  ( A  \  U. x )  ~<_  om ) )
111 rexnal 2847 . . . . . . . . . . . 12  |-  ( E. y  e.  x  -.  y  ~<_  om  <->  -.  A. y  e.  x  y  ~<_  om )
112111bicomi 207 . . . . . . . . . . 11  |-  ( -. 
A. y  e.  x  y  ~<_  om  <->  E. y  e.  x  -.  y  ~<_  om )
113112biimpi 199 . . . . . . . . . 10  |-  ( -. 
A. y  e.  x  y  ~<_  om  ->  E. y  e.  x  -.  y  ~<_  om )
114113adantl 472 . . . . . . . . 9  |-  ( ( x  e.  ~P S  /\  -.  A. y  e.  x  y  ~<_  om )  ->  E. y  e.  x  -.  y  ~<_  om )
115 nfv 1771 . . . . . . . . . . 11  |-  F/ y  x  e.  ~P S
116 nfra1 2780 . . . . . . . . . . . 12  |-  F/ y A. y  e.  x  y  ~<_  om
117116nfn 1993 . . . . . . . . . . 11  |-  F/ y  -.  A. y  e.  x  y  ~<_  om
118115, 117nfan 2021 . . . . . . . . . 10  |-  F/ y ( x  e.  ~P S  /\  -.  A. y  e.  x  y  ~<_  om )
119 nfv 1771 . . . . . . . . . 10  |-  F/ y ( A  \  U. x )  ~<_  om
120 elssuni 4240 . . . . . . . . . . . . . . 15  |-  ( y  e.  x  ->  y  C_ 
U. x )
1211203ad2ant2 1036 . . . . . . . . . . . . . 14  |-  ( ( x  e.  ~P S  /\  y  e.  x  /\  -.  y  ~<_  om )  ->  y  C_  U. x
)
122121sscond 3581 . . . . . . . . . . . . 13  |-  ( ( x  e.  ~P S  /\  y  e.  x  /\  -.  y  ~<_  om )  ->  ( A  \  U. x )  C_  ( A  \  y ) )
123933adant3 1034 . . . . . . . . . . . . . 14  |-  ( ( x  e.  ~P S  /\  y  e.  x  /\  -.  y  ~<_  om )  ->  y  e.  S )
124 simp3 1016 . . . . . . . . . . . . . 14  |-  ( ( x  e.  ~P S  /\  y  e.  x  /\  -.  y  ~<_  om )  ->  -.  y  ~<_  om )
12573rabeq2i 3053 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  S  <->  ( y  e.  ~P A  /\  (
y  ~<_  om  \/  ( A  \  y )  ~<_  om ) ) )
126125biimpi 199 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  S  ->  (
y  e.  ~P A  /\  ( y  ~<_  om  \/  ( A  \  y
)  ~<_  om ) ) )
127126simprd 469 . . . . . . . . . . . . . . . 16  |-  ( y  e.  S  ->  (
y  ~<_  om  \/  ( A  \  y )  ~<_  om ) )
128127adantr 471 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  S  /\  -.  y  ~<_  om )  ->  ( y  ~<_  om  \/  ( A  \  y
)  ~<_  om ) )
129 simpr 467 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  S  /\  -.  y  ~<_  om )  ->  -.  y  ~<_  om )
130 pm2.53 379 . . . . . . . . . . . . . . 15  |-  ( ( y  ~<_  om  \/  ( A  \  y )  ~<_  om )  ->  ( -.  y  ~<_  om  ->  ( A 
\  y )  ~<_  om ) )
131128, 129, 130sylc 62 . . . . . . . . . . . . . 14  |-  ( ( y  e.  S  /\  -.  y  ~<_  om )  ->  ( A  \  y
)  ~<_  om )
132123, 124, 131syl2anc 671 . . . . . . . . . . . . 13  |-  ( ( x  e.  ~P S  /\  y  e.  x  /\  -.  y  ~<_  om )  ->  ( A  \  y
)  ~<_  om )
133 ssct 7678 . . . . . . . . . . . . 13  |-  ( ( ( A  \  U. x )  C_  ( A  \  y )  /\  ( A  \  y
)  ~<_  om )  ->  ( A  \  U. x )  ~<_  om )
134122, 132, 133syl2anc 671 . . . . . . . . . . . 12  |-  ( ( x  e.  ~P S  /\  y  e.  x  /\  -.  y  ~<_  om )  ->  ( A  \  U. x )  ~<_  om )
1351343exp 1214 . . . . . . . . . . 11  |-  ( x  e.  ~P S  -> 
( y  e.  x  ->  ( -.  y  ~<_  om 
->  ( A  \  U. x )  ~<_  om )
) )
136135adantr 471 . . . . . . . . . 10  |-  ( ( x  e.  ~P S  /\  -.  A. y  e.  x  y  ~<_  om )  ->  ( y  e.  x  ->  ( -.  y  ~<_  om 
->  ( A  \  U. x )  ~<_  om )
) )
137118, 119, 136rexlimd 2882 . . . . . . . . 9  |-  ( ( x  e.  ~P S  /\  -.  A. y  e.  x  y  ~<_  om )  ->  ( E. y  e.  x  -.  y  ~<_  om 
->  ( A  \  U. x )  ~<_  om )
)
138114, 137mpd 15 . . . . . . . 8  |-  ( ( x  e.  ~P S  /\  -.  A. y  e.  x  y  ~<_  om )  ->  ( A  \  U. x )  ~<_  om )
139 olc 390 . . . . . . . 8  |-  ( ( A  \  U. x
)  ~<_  om  ->  ( U. x  ~<_  om  \/  ( A  \  U. x )  ~<_  om ) )
140138, 139syl 17 . . . . . . 7  |-  ( ( x  e.  ~P S  /\  -.  A. y  e.  x  y  ~<_  om )  ->  ( U. x  ~<_  om  \/  ( A  \  U. x )  ~<_  om )
)
141140adantlr 726 . . . . . 6  |-  ( ( ( x  e.  ~P S  /\  x  ~<_  om )  /\  -.  A. y  e.  x  y  ~<_  om )  ->  ( U. x  ~<_  om  \/  ( A  \  U. x )  ~<_  om )
)
142110, 141pm2.61dan 805 . . . . 5  |-  ( ( x  e.  ~P S  /\  x  ~<_  om )  ->  ( U. x  ~<_  om  \/  ( A  \  U. x )  ~<_  om )
)
143105, 142jca 539 . . . 4  |-  ( ( x  e.  ~P S  /\  x  ~<_  om )  ->  ( U. x  e. 
~P A  /\  ( U. x  ~<_  om  \/  ( A  \  U. x )  ~<_  om ) ) )
144 breq1 4418 . . . . . 6  |-  ( y  =  U. x  -> 
( y  ~<_  om  <->  U. x  ~<_  om ) )
145 difeq2 3556 . . . . . . 7  |-  ( y  =  U. x  -> 
( A  \  y
)  =  ( A 
\  U. x ) )
146145breq1d 4425 . . . . . 6  |-  ( y  =  U. x  -> 
( ( A  \ 
y )  ~<_  om  <->  ( A  \ 
U. x )  ~<_  om ) )
147144, 146orbi12d 721 . . . . 5  |-  ( y  =  U. x  -> 
( ( y  ~<_  om  \/  ( A  \ 
y )  ~<_  om )  <->  ( U. x  ~<_  om  \/  ( A  \  U. x
)  ~<_  om ) ) )
148147, 73elrab2 3209 . . . 4  |-  ( U. x  e.  S  <->  ( U. x  e.  ~P A  /\  ( U. x  ~<_  om  \/  ( A  \  U. x )  ~<_  om )
) )
149143, 148sylibr 217 . . 3  |-  ( ( x  e.  ~P S  /\  x  ~<_  om )  ->  U. x  e.  S
)
1501493adant1 1032 . 2  |-  ( (
ph  /\  x  e.  ~P S  /\  x  ~<_  om )  ->  U. x  e.  S )
1517, 21, 46, 89, 150issald 38229 1  |-  ( ph  ->  S  e. SAlg )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    \/ wo 374    /\ wa 375    /\ w3a 991    = wceq 1454    e. wcel 1897   A.wral 2748   E.wrex 2749   {crab 2752   _Vcvv 3056    \ cdif 3412    C_ wss 3415   (/)c0 3742   ~Pcpw 3962   {csn 3979   U.cuni 4211   class class class wbr 4415   omcom 6718    ~<_ cdom 7592   Fincfn 7594  SAlgcsalg 38206
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-rep 4528  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6609  ax-inf2 8171  ax-cc 8890
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rex 2754  df-reu 2755  df-rmo 2756  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-pss 3431  df-nul 3743  df-if 3893  df-pw 3964  df-sn 3980  df-pr 3982  df-tp 3984  df-op 3986  df-uni 4212  df-int 4248  df-iun 4293  df-br 4416  df-opab 4475  df-mpt 4476  df-tr 4511  df-eprel 4763  df-id 4767  df-po 4773  df-so 4774  df-fr 4811  df-se 4812  df-we 4813  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-pred 5398  df-ord 5444  df-on 5445  df-lim 5446  df-suc 5447  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-isom 5609  df-riota 6276  df-ov 6317  df-oprab 6318  df-mpt2 6319  df-om 6719  df-1st 6819  df-2nd 6820  df-wrecs 7053  df-recs 7115  df-rdg 7153  df-1o 7207  df-oadd 7211  df-er 7388  df-map 7499  df-en 7595  df-dom 7596  df-sdom 7597  df-fin 7598  df-oi 8050  df-card 8398  df-acn 8401  df-salg 38207
This theorem is referenced by:  salexct3  38238  salgencntex  38239  salgensscntex  38240
  Copyright terms: Public domain W3C validator