| Step |
Hyp |
Ref |
Expression |
| 1 |
|
inex1g |
⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( 𝑆 ∩ 𝒫 𝐴 ) ∈ V ) |
| 2 |
1
|
adantr |
⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ) → ( 𝑆 ∩ 𝒫 𝐴 ) ∈ V ) |
| 3 |
|
inss2 |
⊢ ( 𝑆 ∩ 𝒫 𝐴 ) ⊆ 𝒫 𝐴 |
| 4 |
3
|
a1i |
⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ) → ( 𝑆 ∩ 𝒫 𝐴 ) ⊆ 𝒫 𝐴 ) |
| 5 |
|
simpr |
⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ) → 𝐴 ∈ 𝑆 ) |
| 6 |
|
pwidg |
⊢ ( 𝐴 ∈ 𝑆 → 𝐴 ∈ 𝒫 𝐴 ) |
| 7 |
5 6
|
syl |
⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ) → 𝐴 ∈ 𝒫 𝐴 ) |
| 8 |
5 7
|
elind |
⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ) → 𝐴 ∈ ( 𝑆 ∩ 𝒫 𝐴 ) ) |
| 9 |
|
simpll |
⊢ ( ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑥 ∈ ( 𝑆 ∩ 𝒫 𝐴 ) ) → 𝑆 ∈ ∪ ran sigAlgebra ) |
| 10 |
|
simplr |
⊢ ( ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑥 ∈ ( 𝑆 ∩ 𝒫 𝐴 ) ) → 𝐴 ∈ 𝑆 ) |
| 11 |
|
inss1 |
⊢ ( 𝑆 ∩ 𝒫 𝐴 ) ⊆ 𝑆 |
| 12 |
|
simpr |
⊢ ( ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑥 ∈ ( 𝑆 ∩ 𝒫 𝐴 ) ) → 𝑥 ∈ ( 𝑆 ∩ 𝒫 𝐴 ) ) |
| 13 |
11 12
|
sselid |
⊢ ( ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑥 ∈ ( 𝑆 ∩ 𝒫 𝐴 ) ) → 𝑥 ∈ 𝑆 ) |
| 14 |
|
difelsiga |
⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) → ( 𝐴 ∖ 𝑥 ) ∈ 𝑆 ) |
| 15 |
9 10 13 14
|
syl3anc |
⊢ ( ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑥 ∈ ( 𝑆 ∩ 𝒫 𝐴 ) ) → ( 𝐴 ∖ 𝑥 ) ∈ 𝑆 ) |
| 16 |
|
difss |
⊢ ( 𝐴 ∖ 𝑥 ) ⊆ 𝐴 |
| 17 |
|
elpwg |
⊢ ( ( 𝐴 ∖ 𝑥 ) ∈ 𝑆 → ( ( 𝐴 ∖ 𝑥 ) ∈ 𝒫 𝐴 ↔ ( 𝐴 ∖ 𝑥 ) ⊆ 𝐴 ) ) |
| 18 |
16 17
|
mpbiri |
⊢ ( ( 𝐴 ∖ 𝑥 ) ∈ 𝑆 → ( 𝐴 ∖ 𝑥 ) ∈ 𝒫 𝐴 ) |
| 19 |
15 18
|
syl |
⊢ ( ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑥 ∈ ( 𝑆 ∩ 𝒫 𝐴 ) ) → ( 𝐴 ∖ 𝑥 ) ∈ 𝒫 𝐴 ) |
| 20 |
15 19
|
elind |
⊢ ( ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑥 ∈ ( 𝑆 ∩ 𝒫 𝐴 ) ) → ( 𝐴 ∖ 𝑥 ) ∈ ( 𝑆 ∩ 𝒫 𝐴 ) ) |
| 21 |
20
|
ralrimiva |
⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ) → ∀ 𝑥 ∈ ( 𝑆 ∩ 𝒫 𝐴 ) ( 𝐴 ∖ 𝑥 ) ∈ ( 𝑆 ∩ 𝒫 𝐴 ) ) |
| 22 |
|
simplll |
⊢ ( ( ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝒫 ( 𝑆 ∩ 𝒫 𝐴 ) ) ∧ 𝑥 ≼ ω ) → 𝑆 ∈ ∪ ran sigAlgebra ) |
| 23 |
|
simplr |
⊢ ( ( ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝒫 ( 𝑆 ∩ 𝒫 𝐴 ) ) ∧ 𝑥 ≼ ω ) → 𝑥 ∈ 𝒫 ( 𝑆 ∩ 𝒫 𝐴 ) ) |
| 24 |
|
elpwi |
⊢ ( 𝑥 ∈ 𝒫 ( 𝑆 ∩ 𝒫 𝐴 ) → 𝑥 ⊆ ( 𝑆 ∩ 𝒫 𝐴 ) ) |
| 25 |
|
sstr |
⊢ ( ( 𝑥 ⊆ ( 𝑆 ∩ 𝒫 𝐴 ) ∧ ( 𝑆 ∩ 𝒫 𝐴 ) ⊆ 𝑆 ) → 𝑥 ⊆ 𝑆 ) |
| 26 |
11 25
|
mpan2 |
⊢ ( 𝑥 ⊆ ( 𝑆 ∩ 𝒫 𝐴 ) → 𝑥 ⊆ 𝑆 ) |
| 27 |
23 24 26
|
3syl |
⊢ ( ( ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝒫 ( 𝑆 ∩ 𝒫 𝐴 ) ) ∧ 𝑥 ≼ ω ) → 𝑥 ⊆ 𝑆 ) |
| 28 |
|
elpwg |
⊢ ( 𝑥 ∈ 𝒫 ( 𝑆 ∩ 𝒫 𝐴 ) → ( 𝑥 ∈ 𝒫 𝑆 ↔ 𝑥 ⊆ 𝑆 ) ) |
| 29 |
28
|
biimpar |
⊢ ( ( 𝑥 ∈ 𝒫 ( 𝑆 ∩ 𝒫 𝐴 ) ∧ 𝑥 ⊆ 𝑆 ) → 𝑥 ∈ 𝒫 𝑆 ) |
| 30 |
23 27 29
|
syl2anc |
⊢ ( ( ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝒫 ( 𝑆 ∩ 𝒫 𝐴 ) ) ∧ 𝑥 ≼ ω ) → 𝑥 ∈ 𝒫 𝑆 ) |
| 31 |
|
simpr |
⊢ ( ( ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝒫 ( 𝑆 ∩ 𝒫 𝐴 ) ) ∧ 𝑥 ≼ ω ) → 𝑥 ≼ ω ) |
| 32 |
|
sigaclcu |
⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑥 ∈ 𝒫 𝑆 ∧ 𝑥 ≼ ω ) → ∪ 𝑥 ∈ 𝑆 ) |
| 33 |
22 30 31 32
|
syl3anc |
⊢ ( ( ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝒫 ( 𝑆 ∩ 𝒫 𝐴 ) ) ∧ 𝑥 ≼ ω ) → ∪ 𝑥 ∈ 𝑆 ) |
| 34 |
|
sstr |
⊢ ( ( 𝑥 ⊆ ( 𝑆 ∩ 𝒫 𝐴 ) ∧ ( 𝑆 ∩ 𝒫 𝐴 ) ⊆ 𝒫 𝐴 ) → 𝑥 ⊆ 𝒫 𝐴 ) |
| 35 |
3 34
|
mpan2 |
⊢ ( 𝑥 ⊆ ( 𝑆 ∩ 𝒫 𝐴 ) → 𝑥 ⊆ 𝒫 𝐴 ) |
| 36 |
23 24 35
|
3syl |
⊢ ( ( ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝒫 ( 𝑆 ∩ 𝒫 𝐴 ) ) ∧ 𝑥 ≼ ω ) → 𝑥 ⊆ 𝒫 𝐴 ) |
| 37 |
|
sspwuni |
⊢ ( 𝑥 ⊆ 𝒫 𝐴 ↔ ∪ 𝑥 ⊆ 𝐴 ) |
| 38 |
|
vuniex |
⊢ ∪ 𝑥 ∈ V |
| 39 |
38
|
elpw |
⊢ ( ∪ 𝑥 ∈ 𝒫 𝐴 ↔ ∪ 𝑥 ⊆ 𝐴 ) |
| 40 |
37 39
|
bitr4i |
⊢ ( 𝑥 ⊆ 𝒫 𝐴 ↔ ∪ 𝑥 ∈ 𝒫 𝐴 ) |
| 41 |
36 40
|
sylib |
⊢ ( ( ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝒫 ( 𝑆 ∩ 𝒫 𝐴 ) ) ∧ 𝑥 ≼ ω ) → ∪ 𝑥 ∈ 𝒫 𝐴 ) |
| 42 |
33 41
|
elind |
⊢ ( ( ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝒫 ( 𝑆 ∩ 𝒫 𝐴 ) ) ∧ 𝑥 ≼ ω ) → ∪ 𝑥 ∈ ( 𝑆 ∩ 𝒫 𝐴 ) ) |
| 43 |
42
|
ex |
⊢ ( ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝒫 ( 𝑆 ∩ 𝒫 𝐴 ) ) → ( 𝑥 ≼ ω → ∪ 𝑥 ∈ ( 𝑆 ∩ 𝒫 𝐴 ) ) ) |
| 44 |
43
|
ralrimiva |
⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ) → ∀ 𝑥 ∈ 𝒫 ( 𝑆 ∩ 𝒫 𝐴 ) ( 𝑥 ≼ ω → ∪ 𝑥 ∈ ( 𝑆 ∩ 𝒫 𝐴 ) ) ) |
| 45 |
8 21 44
|
3jca |
⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ) → ( 𝐴 ∈ ( 𝑆 ∩ 𝒫 𝐴 ) ∧ ∀ 𝑥 ∈ ( 𝑆 ∩ 𝒫 𝐴 ) ( 𝐴 ∖ 𝑥 ) ∈ ( 𝑆 ∩ 𝒫 𝐴 ) ∧ ∀ 𝑥 ∈ 𝒫 ( 𝑆 ∩ 𝒫 𝐴 ) ( 𝑥 ≼ ω → ∪ 𝑥 ∈ ( 𝑆 ∩ 𝒫 𝐴 ) ) ) ) |
| 46 |
|
issiga |
⊢ ( ( 𝑆 ∩ 𝒫 𝐴 ) ∈ V → ( ( 𝑆 ∩ 𝒫 𝐴 ) ∈ ( sigAlgebra ‘ 𝐴 ) ↔ ( ( 𝑆 ∩ 𝒫 𝐴 ) ⊆ 𝒫 𝐴 ∧ ( 𝐴 ∈ ( 𝑆 ∩ 𝒫 𝐴 ) ∧ ∀ 𝑥 ∈ ( 𝑆 ∩ 𝒫 𝐴 ) ( 𝐴 ∖ 𝑥 ) ∈ ( 𝑆 ∩ 𝒫 𝐴 ) ∧ ∀ 𝑥 ∈ 𝒫 ( 𝑆 ∩ 𝒫 𝐴 ) ( 𝑥 ≼ ω → ∪ 𝑥 ∈ ( 𝑆 ∩ 𝒫 𝐴 ) ) ) ) ) ) |
| 47 |
46
|
biimpar |
⊢ ( ( ( 𝑆 ∩ 𝒫 𝐴 ) ∈ V ∧ ( ( 𝑆 ∩ 𝒫 𝐴 ) ⊆ 𝒫 𝐴 ∧ ( 𝐴 ∈ ( 𝑆 ∩ 𝒫 𝐴 ) ∧ ∀ 𝑥 ∈ ( 𝑆 ∩ 𝒫 𝐴 ) ( 𝐴 ∖ 𝑥 ) ∈ ( 𝑆 ∩ 𝒫 𝐴 ) ∧ ∀ 𝑥 ∈ 𝒫 ( 𝑆 ∩ 𝒫 𝐴 ) ( 𝑥 ≼ ω → ∪ 𝑥 ∈ ( 𝑆 ∩ 𝒫 𝐴 ) ) ) ) ) → ( 𝑆 ∩ 𝒫 𝐴 ) ∈ ( sigAlgebra ‘ 𝐴 ) ) |
| 48 |
2 4 45 47
|
syl12anc |
⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ) → ( 𝑆 ∩ 𝒫 𝐴 ) ∈ ( sigAlgebra ‘ 𝐴 ) ) |