Step | Hyp | Ref
| Expression |
1 | | intex 4747 |
. . . 4
⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴
∈ V) |
2 | 1 | biimpi 205 |
. . 3
⊢ (𝐴 ≠ ∅ → ∩ 𝐴
∈ V) |
3 | 2 | adantr 480 |
. 2
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ ∩ 𝐴 ∈ V) |
4 | | intssuni 4434 |
. . . 4
⊢ (𝐴 ≠ ∅ → ∩ 𝐴
⊆ ∪ 𝐴) |
5 | 4 | adantr 480 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ ∩ 𝐴 ⊆ ∪ 𝐴) |
6 | | simpr 476 |
. . . . 5
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) |
7 | | elpwi 4117 |
. . . . . 6
⊢ (𝐴 ∈ 𝒫
(sigAlgebra‘𝑂) →
𝐴 ⊆
(sigAlgebra‘𝑂)) |
8 | | sigasspw 29506 |
. . . . . . . 8
⊢ (𝑠 ∈ (sigAlgebra‘𝑂) → 𝑠 ⊆ 𝒫 𝑂) |
9 | | selpw 4115 |
. . . . . . . 8
⊢ (𝑠 ∈ 𝒫 𝒫
𝑂 ↔ 𝑠 ⊆ 𝒫 𝑂) |
10 | 8, 9 | sylibr 223 |
. . . . . . 7
⊢ (𝑠 ∈ (sigAlgebra‘𝑂) → 𝑠 ∈ 𝒫 𝒫 𝑂) |
11 | 10 | ssriv 3572 |
. . . . . 6
⊢
(sigAlgebra‘𝑂)
⊆ 𝒫 𝒫 𝑂 |
12 | 7, 11 | syl6ss 3580 |
. . . . 5
⊢ (𝐴 ∈ 𝒫
(sigAlgebra‘𝑂) →
𝐴 ⊆ 𝒫
𝒫 𝑂) |
13 | 6, 12 | syl 17 |
. . . 4
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ 𝐴 ⊆ 𝒫
𝒫 𝑂) |
14 | | sspwuni 4547 |
. . . 4
⊢ (𝐴 ⊆ 𝒫 𝒫
𝑂 ↔ ∪ 𝐴
⊆ 𝒫 𝑂) |
15 | 13, 14 | sylib 207 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ ∪ 𝐴 ⊆ 𝒫 𝑂) |
16 | 5, 15 | sstrd 3578 |
. 2
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ ∩ 𝐴 ⊆ 𝒫 𝑂) |
17 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑠 ∈ 𝐴) → 𝑠 ∈ 𝐴) |
18 | | simplr 788 |
. . . . . . . . 9
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑠 ∈ 𝐴) → 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) |
19 | | elelpwi 4119 |
. . . . . . . . 9
⊢ ((𝑠 ∈ 𝐴 ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → 𝑠 ∈ (sigAlgebra‘𝑂)) |
20 | 17, 18, 19 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑠 ∈ 𝐴) → 𝑠 ∈ (sigAlgebra‘𝑂)) |
21 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑠 ∈ V |
22 | | issiga 29501 |
. . . . . . . . 9
⊢ (𝑠 ∈ V → (𝑠 ∈ (sigAlgebra‘𝑂) ↔ (𝑠 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠))))) |
23 | 21, 22 | ax-mp 5 |
. . . . . . . 8
⊢ (𝑠 ∈ (sigAlgebra‘𝑂) ↔ (𝑠 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)))) |
24 | 20, 23 | sylib 207 |
. . . . . . 7
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑠 ∈ 𝐴) → (𝑠 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)))) |
25 | 24 | simprd 478 |
. . . . . 6
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑠 ∈ 𝐴) → (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠))) |
26 | 25 | simp1d 1066 |
. . . . 5
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑠 ∈ 𝐴) → 𝑂 ∈ 𝑠) |
27 | 26 | ralrimiva 2949 |
. . . 4
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ ∀𝑠 ∈
𝐴 𝑂 ∈ 𝑠) |
28 | | n0 3890 |
. . . . . . . . 9
⊢ (𝐴 ≠ ∅ ↔
∃𝑠 𝑠 ∈ 𝐴) |
29 | 28 | biimpi 205 |
. . . . . . . 8
⊢ (𝐴 ≠ ∅ →
∃𝑠 𝑠 ∈ 𝐴) |
30 | 29 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ ∃𝑠 𝑠 ∈ 𝐴) |
31 | 20 | ex 449 |
. . . . . . . 8
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ (𝑠 ∈ 𝐴 → 𝑠 ∈ (sigAlgebra‘𝑂))) |
32 | 31 | eximdv 1833 |
. . . . . . 7
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ (∃𝑠 𝑠 ∈ 𝐴 → ∃𝑠 𝑠 ∈ (sigAlgebra‘𝑂))) |
33 | 30, 32 | mpd 15 |
. . . . . 6
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ ∃𝑠 𝑠 ∈ (sigAlgebra‘𝑂)) |
34 | | elfvex 6131 |
. . . . . . 7
⊢ (𝑠 ∈ (sigAlgebra‘𝑂) → 𝑂 ∈ V) |
35 | 34 | exlimiv 1845 |
. . . . . 6
⊢
(∃𝑠 𝑠 ∈ (sigAlgebra‘𝑂) → 𝑂 ∈ V) |
36 | 33, 35 | syl 17 |
. . . . 5
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ 𝑂 ∈
V) |
37 | | elintg 4418 |
. . . . 5
⊢ (𝑂 ∈ V → (𝑂 ∈ ∩ 𝐴
↔ ∀𝑠 ∈
𝐴 𝑂 ∈ 𝑠)) |
38 | 36, 37 | syl 17 |
. . . 4
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ (𝑂 ∈ ∩ 𝐴
↔ ∀𝑠 ∈
𝐴 𝑂 ∈ 𝑠)) |
39 | 27, 38 | mpbird 246 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ 𝑂 ∈ ∩ 𝐴) |
40 | | simpll 786 |
. . . . . . . 8
⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ ∩ 𝐴)
∧ 𝑠 ∈ 𝐴) → (𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂))) |
41 | | simpr 476 |
. . . . . . . 8
⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ ∩ 𝐴)
∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ 𝐴) |
42 | 40, 41 | jca 553 |
. . . . . . 7
⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ ∩ 𝐴)
∧ 𝑠 ∈ 𝐴) → ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴)) |
43 | | elinti 4420 |
. . . . . . . . 9
⊢ (𝑥 ∈ ∩ 𝐴
→ (𝑠 ∈ 𝐴 → 𝑥 ∈ 𝑠)) |
44 | 43 | imp 444 |
. . . . . . . 8
⊢ ((𝑥 ∈ ∩ 𝐴
∧ 𝑠 ∈ 𝐴) → 𝑥 ∈ 𝑠) |
45 | 44 | adantll 746 |
. . . . . . 7
⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ ∩ 𝐴)
∧ 𝑠 ∈ 𝐴) → 𝑥 ∈ 𝑠) |
46 | 25 | simp2d 1067 |
. . . . . . . 8
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑠 ∈ 𝐴) → ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠) |
47 | 46 | r19.21bi 2916 |
. . . . . . 7
⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑠 ∈ 𝐴) ∧ 𝑥 ∈ 𝑠) → (𝑂 ∖ 𝑥) ∈ 𝑠) |
48 | 42, 45, 47 | syl2anc 691 |
. . . . . 6
⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ ∩ 𝐴)
∧ 𝑠 ∈ 𝐴) → (𝑂 ∖ 𝑥) ∈ 𝑠) |
49 | 48 | ralrimiva 2949 |
. . . . 5
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ ∩ 𝐴)
→ ∀𝑠 ∈
𝐴 (𝑂 ∖ 𝑥) ∈ 𝑠) |
50 | | difexg 4735 |
. . . . . . . 8
⊢ (𝑂 ∈ V → (𝑂 ∖ 𝑥) ∈ V) |
51 | 36, 50 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ (𝑂 ∖ 𝑥) ∈ V) |
52 | 51 | adantr 480 |
. . . . . 6
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ ∩ 𝐴)
→ (𝑂 ∖ 𝑥) ∈ V) |
53 | | elintg 4418 |
. . . . . 6
⊢ ((𝑂 ∖ 𝑥) ∈ V → ((𝑂 ∖ 𝑥) ∈ ∩ 𝐴 ↔ ∀𝑠 ∈ 𝐴 (𝑂 ∖ 𝑥) ∈ 𝑠)) |
54 | 52, 53 | syl 17 |
. . . . 5
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ ∩ 𝐴)
→ ((𝑂 ∖ 𝑥) ∈ ∩ 𝐴
↔ ∀𝑠 ∈
𝐴 (𝑂 ∖ 𝑥) ∈ 𝑠)) |
55 | 49, 54 | mpbird 246 |
. . . 4
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ ∩ 𝐴)
→ (𝑂 ∖ 𝑥) ∈ ∩ 𝐴) |
56 | 55 | ralrimiva 2949 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ ∀𝑥 ∈
∩ 𝐴(𝑂 ∖ 𝑥) ∈ ∩ 𝐴) |
57 | | simplll 794 |
. . . . . . . . . 10
⊢
(((((𝐴 ≠ ∅
∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ 𝒫 ∩ 𝐴)
∧ 𝑥 ≼ ω)
∧ 𝑠 ∈ 𝐴) → (𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂))) |
58 | | simpr 476 |
. . . . . . . . . 10
⊢
(((((𝐴 ≠ ∅
∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ 𝒫 ∩ 𝐴)
∧ 𝑥 ≼ ω)
∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ 𝐴) |
59 | 57, 58 | jca 553 |
. . . . . . . . 9
⊢
(((((𝐴 ≠ ∅
∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ 𝒫 ∩ 𝐴)
∧ 𝑥 ≼ ω)
∧ 𝑠 ∈ 𝐴) → ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴)) |
60 | | simpllr 795 |
. . . . . . . . . 10
⊢
(((((𝐴 ≠ ∅
∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ 𝒫 ∩ 𝐴)
∧ 𝑥 ≼ ω)
∧ 𝑠 ∈ 𝐴) → 𝑥 ∈ 𝒫 ∩ 𝐴) |
61 | | elpwi 4117 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝒫 ∩ 𝐴
→ 𝑥 ⊆ ∩ 𝐴) |
62 | | intss1 4427 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑠) |
63 | 61, 62 | sylan9ss 3581 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝒫 ∩ 𝐴
∧ 𝑠 ∈ 𝐴) → 𝑥 ⊆ 𝑠) |
64 | | selpw 4115 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝒫 𝑠 ↔ 𝑥 ⊆ 𝑠) |
65 | 63, 64 | sylibr 223 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝒫 ∩ 𝐴
∧ 𝑠 ∈ 𝐴) → 𝑥 ∈ 𝒫 𝑠) |
66 | 60, 65 | sylancom 698 |
. . . . . . . . 9
⊢
(((((𝐴 ≠ ∅
∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ 𝒫 ∩ 𝐴)
∧ 𝑥 ≼ ω)
∧ 𝑠 ∈ 𝐴) → 𝑥 ∈ 𝒫 𝑠) |
67 | 59, 66 | jca 553 |
. . . . . . . 8
⊢
(((((𝐴 ≠ ∅
∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ 𝒫 ∩ 𝐴)
∧ 𝑥 ≼ ω)
∧ 𝑠 ∈ 𝐴) → (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) ∧ 𝑥 ∈ 𝒫 𝑠)) |
68 | | simplr 788 |
. . . . . . . 8
⊢
(((((𝐴 ≠ ∅
∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ 𝒫 ∩ 𝐴)
∧ 𝑥 ≼ ω)
∧ 𝑠 ∈ 𝐴) → 𝑥 ≼ ω) |
69 | 25 | simp3d 1068 |
. . . . . . . . 9
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑠 ∈ 𝐴) → ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)) |
70 | 69 | r19.21bi 2916 |
. . . . . . . 8
⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑠 ∈ 𝐴) ∧ 𝑥 ∈ 𝒫 𝑠) → (𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)) |
71 | 67, 68, 70 | sylc 63 |
. . . . . . 7
⊢
(((((𝐴 ≠ ∅
∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ 𝒫 ∩ 𝐴)
∧ 𝑥 ≼ ω)
∧ 𝑠 ∈ 𝐴) → ∪ 𝑥
∈ 𝑠) |
72 | 71 | ralrimiva 2949 |
. . . . . 6
⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ 𝒫 ∩ 𝐴)
∧ 𝑥 ≼ ω)
→ ∀𝑠 ∈
𝐴 ∪ 𝑥
∈ 𝑠) |
73 | | uniexg 6853 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝒫 ∩ 𝐴
→ ∪ 𝑥 ∈ V) |
74 | 73 | ad2antlr 759 |
. . . . . . 7
⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ 𝒫 ∩ 𝐴)
∧ 𝑥 ≼ ω)
→ ∪ 𝑥 ∈ V) |
75 | | elintg 4418 |
. . . . . . 7
⊢ (∪ 𝑥
∈ V → (∪ 𝑥 ∈ ∩ 𝐴 ↔ ∀𝑠 ∈ 𝐴 ∪ 𝑥 ∈ 𝑠)) |
76 | 74, 75 | syl 17 |
. . . . . 6
⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ 𝒫 ∩ 𝐴)
∧ 𝑥 ≼ ω)
→ (∪ 𝑥 ∈ ∩ 𝐴 ↔ ∀𝑠 ∈ 𝐴 ∪ 𝑥 ∈ 𝑠)) |
77 | 72, 76 | mpbird 246 |
. . . . 5
⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ 𝒫 ∩ 𝐴)
∧ 𝑥 ≼ ω)
→ ∪ 𝑥 ∈ ∩ 𝐴) |
78 | 77 | ex 449 |
. . . 4
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ 𝒫 ∩ 𝐴)
→ (𝑥 ≼ ω
→ ∪ 𝑥 ∈ ∩ 𝐴)) |
79 | 78 | ralrimiva 2949 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ ∀𝑥 ∈
𝒫 ∩ 𝐴(𝑥 ≼ ω → ∪ 𝑥
∈ ∩ 𝐴)) |
80 | 39, 56, 79 | 3jca 1235 |
. 2
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ (𝑂 ∈ ∩ 𝐴
∧ ∀𝑥 ∈
∩ 𝐴(𝑂 ∖ 𝑥) ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ 𝒫 ∩ 𝐴(𝑥 ≼ ω → ∪ 𝑥
∈ ∩ 𝐴))) |
81 | | issiga 29501 |
. . 3
⊢ (∩ 𝐴
∈ V → (∩ 𝐴 ∈ (sigAlgebra‘𝑂) ↔ (∩ 𝐴 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ ∩ 𝐴(𝑂 ∖ 𝑥) ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ 𝒫 ∩ 𝐴(𝑥 ≼ ω → ∪ 𝑥
∈ ∩ 𝐴))))) |
82 | 81 | biimpar 501 |
. 2
⊢ ((∩ 𝐴
∈ V ∧ (∩ 𝐴 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ ∩ 𝐴(𝑂 ∖ 𝑥) ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ 𝒫 ∩ 𝐴(𝑥 ≼ ω → ∪ 𝑥
∈ ∩ 𝐴)))) → ∩
𝐴 ∈
(sigAlgebra‘𝑂)) |
83 | 3, 16, 80, 82 | syl12anc 1316 |
1
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ ∩ 𝐴 ∈ (sigAlgebra‘𝑂)) |