Step |
Hyp |
Ref |
Expression |
1 |
|
inex1g |
|- ( S e. U. ran sigAlgebra -> ( S i^i ~P A ) e. _V ) |
2 |
1
|
adantr |
|- ( ( S e. U. ran sigAlgebra /\ A e. S ) -> ( S i^i ~P A ) e. _V ) |
3 |
|
inss2 |
|- ( S i^i ~P A ) C_ ~P A |
4 |
3
|
a1i |
|- ( ( S e. U. ran sigAlgebra /\ A e. S ) -> ( S i^i ~P A ) C_ ~P A ) |
5 |
|
simpr |
|- ( ( S e. U. ran sigAlgebra /\ A e. S ) -> A e. S ) |
6 |
|
pwidg |
|- ( A e. S -> A e. ~P A ) |
7 |
5 6
|
syl |
|- ( ( S e. U. ran sigAlgebra /\ A e. S ) -> A e. ~P A ) |
8 |
5 7
|
elind |
|- ( ( S e. U. ran sigAlgebra /\ A e. S ) -> A e. ( S i^i ~P A ) ) |
9 |
|
simpll |
|- ( ( ( S e. U. ran sigAlgebra /\ A e. S ) /\ x e. ( S i^i ~P A ) ) -> S e. U. ran sigAlgebra ) |
10 |
|
simplr |
|- ( ( ( S e. U. ran sigAlgebra /\ A e. S ) /\ x e. ( S i^i ~P A ) ) -> A e. S ) |
11 |
|
inss1 |
|- ( S i^i ~P A ) C_ S |
12 |
|
simpr |
|- ( ( ( S e. U. ran sigAlgebra /\ A e. S ) /\ x e. ( S i^i ~P A ) ) -> x e. ( S i^i ~P A ) ) |
13 |
11 12
|
sselid |
|- ( ( ( S e. U. ran sigAlgebra /\ A e. S ) /\ x e. ( S i^i ~P A ) ) -> x e. S ) |
14 |
|
difelsiga |
|- ( ( S e. U. ran sigAlgebra /\ A e. S /\ x e. S ) -> ( A \ x ) e. S ) |
15 |
9 10 13 14
|
syl3anc |
|- ( ( ( S e. U. ran sigAlgebra /\ A e. S ) /\ x e. ( S i^i ~P A ) ) -> ( A \ x ) e. S ) |
16 |
|
difss |
|- ( A \ x ) C_ A |
17 |
|
elpwg |
|- ( ( A \ x ) e. S -> ( ( A \ x ) e. ~P A <-> ( A \ x ) C_ A ) ) |
18 |
16 17
|
mpbiri |
|- ( ( A \ x ) e. S -> ( A \ x ) e. ~P A ) |
19 |
15 18
|
syl |
|- ( ( ( S e. U. ran sigAlgebra /\ A e. S ) /\ x e. ( S i^i ~P A ) ) -> ( A \ x ) e. ~P A ) |
20 |
15 19
|
elind |
|- ( ( ( S e. U. ran sigAlgebra /\ A e. S ) /\ x e. ( S i^i ~P A ) ) -> ( A \ x ) e. ( S i^i ~P A ) ) |
21 |
20
|
ralrimiva |
|- ( ( S e. U. ran sigAlgebra /\ A e. S ) -> A. x e. ( S i^i ~P A ) ( A \ x ) e. ( S i^i ~P A ) ) |
22 |
|
simplll |
|- ( ( ( ( S e. U. ran sigAlgebra /\ A e. S ) /\ x e. ~P ( S i^i ~P A ) ) /\ x ~<_ _om ) -> S e. U. ran sigAlgebra ) |
23 |
|
simplr |
|- ( ( ( ( S e. U. ran sigAlgebra /\ A e. S ) /\ x e. ~P ( S i^i ~P A ) ) /\ x ~<_ _om ) -> x e. ~P ( S i^i ~P A ) ) |
24 |
|
elpwi |
|- ( x e. ~P ( S i^i ~P A ) -> x C_ ( S i^i ~P A ) ) |
25 |
|
sstr |
|- ( ( x C_ ( S i^i ~P A ) /\ ( S i^i ~P A ) C_ S ) -> x C_ S ) |
26 |
11 25
|
mpan2 |
|- ( x C_ ( S i^i ~P A ) -> x C_ S ) |
27 |
23 24 26
|
3syl |
|- ( ( ( ( S e. U. ran sigAlgebra /\ A e. S ) /\ x e. ~P ( S i^i ~P A ) ) /\ x ~<_ _om ) -> x C_ S ) |
28 |
|
elpwg |
|- ( x e. ~P ( S i^i ~P A ) -> ( x e. ~P S <-> x C_ S ) ) |
29 |
28
|
biimpar |
|- ( ( x e. ~P ( S i^i ~P A ) /\ x C_ S ) -> x e. ~P S ) |
30 |
23 27 29
|
syl2anc |
|- ( ( ( ( S e. U. ran sigAlgebra /\ A e. S ) /\ x e. ~P ( S i^i ~P A ) ) /\ x ~<_ _om ) -> x e. ~P S ) |
31 |
|
simpr |
|- ( ( ( ( S e. U. ran sigAlgebra /\ A e. S ) /\ x e. ~P ( S i^i ~P A ) ) /\ x ~<_ _om ) -> x ~<_ _om ) |
32 |
|
sigaclcu |
|- ( ( S e. U. ran sigAlgebra /\ x e. ~P S /\ x ~<_ _om ) -> U. x e. S ) |
33 |
22 30 31 32
|
syl3anc |
|- ( ( ( ( S e. U. ran sigAlgebra /\ A e. S ) /\ x e. ~P ( S i^i ~P A ) ) /\ x ~<_ _om ) -> U. x e. S ) |
34 |
|
sstr |
|- ( ( x C_ ( S i^i ~P A ) /\ ( S i^i ~P A ) C_ ~P A ) -> x C_ ~P A ) |
35 |
3 34
|
mpan2 |
|- ( x C_ ( S i^i ~P A ) -> x C_ ~P A ) |
36 |
23 24 35
|
3syl |
|- ( ( ( ( S e. U. ran sigAlgebra /\ A e. S ) /\ x e. ~P ( S i^i ~P A ) ) /\ x ~<_ _om ) -> x C_ ~P A ) |
37 |
|
sspwuni |
|- ( x C_ ~P A <-> U. x C_ A ) |
38 |
|
vuniex |
|- U. x e. _V |
39 |
38
|
elpw |
|- ( U. x e. ~P A <-> U. x C_ A ) |
40 |
37 39
|
bitr4i |
|- ( x C_ ~P A <-> U. x e. ~P A ) |
41 |
36 40
|
sylib |
|- ( ( ( ( S e. U. ran sigAlgebra /\ A e. S ) /\ x e. ~P ( S i^i ~P A ) ) /\ x ~<_ _om ) -> U. x e. ~P A ) |
42 |
33 41
|
elind |
|- ( ( ( ( S e. U. ran sigAlgebra /\ A e. S ) /\ x e. ~P ( S i^i ~P A ) ) /\ x ~<_ _om ) -> U. x e. ( S i^i ~P A ) ) |
43 |
42
|
ex |
|- ( ( ( S e. U. ran sigAlgebra /\ A e. S ) /\ x e. ~P ( S i^i ~P A ) ) -> ( x ~<_ _om -> U. x e. ( S i^i ~P A ) ) ) |
44 |
43
|
ralrimiva |
|- ( ( S e. U. ran sigAlgebra /\ A e. S ) -> A. x e. ~P ( S i^i ~P A ) ( x ~<_ _om -> U. x e. ( S i^i ~P A ) ) ) |
45 |
8 21 44
|
3jca |
|- ( ( S e. U. ran sigAlgebra /\ A e. S ) -> ( A e. ( S i^i ~P A ) /\ A. x e. ( S i^i ~P A ) ( A \ x ) e. ( S i^i ~P A ) /\ A. x e. ~P ( S i^i ~P A ) ( x ~<_ _om -> U. x e. ( S i^i ~P A ) ) ) ) |
46 |
|
issiga |
|- ( ( S i^i ~P A ) e. _V -> ( ( S i^i ~P A ) e. ( sigAlgebra ` A ) <-> ( ( S i^i ~P A ) C_ ~P A /\ ( A e. ( S i^i ~P A ) /\ A. x e. ( S i^i ~P A ) ( A \ x ) e. ( S i^i ~P A ) /\ A. x e. ~P ( S i^i ~P A ) ( x ~<_ _om -> U. x e. ( S i^i ~P A ) ) ) ) ) ) |
47 |
46
|
biimpar |
|- ( ( ( S i^i ~P A ) e. _V /\ ( ( S i^i ~P A ) C_ ~P A /\ ( A e. ( S i^i ~P A ) /\ A. x e. ( S i^i ~P A ) ( A \ x ) e. ( S i^i ~P A ) /\ A. x e. ~P ( S i^i ~P A ) ( x ~<_ _om -> U. x e. ( S i^i ~P A ) ) ) ) ) -> ( S i^i ~P A ) e. ( sigAlgebra ` A ) ) |
48 |
2 4 45 47
|
syl12anc |
|- ( ( S e. U. ran sigAlgebra /\ A e. S ) -> ( S i^i ~P A ) e. ( sigAlgebra ` A ) ) |