| Step | Hyp | Ref
| Expression |
| 1 | | intex 5344 |
. . . 4
⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴
∈ V) |
| 2 | 1 | biimpi 216 |
. . 3
⊢ (𝐴 ≠ ∅ → ∩ 𝐴
∈ V) |
| 3 | 2 | adantr 480 |
. 2
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ ∩ 𝐴 ∈ V) |
| 4 | | intssuni 4970 |
. . . 4
⊢ (𝐴 ≠ ∅ → ∩ 𝐴
⊆ ∪ 𝐴) |
| 5 | 4 | adantr 480 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ ∩ 𝐴 ⊆ ∪ 𝐴) |
| 6 | | simpr 484 |
. . . . 5
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) |
| 7 | | elpwi 4607 |
. . . . . 6
⊢ (𝐴 ∈ 𝒫
(sigAlgebra‘𝑂) →
𝐴 ⊆
(sigAlgebra‘𝑂)) |
| 8 | | sigasspw 34117 |
. . . . . . . 8
⊢ (𝑠 ∈ (sigAlgebra‘𝑂) → 𝑠 ⊆ 𝒫 𝑂) |
| 9 | | velpw 4605 |
. . . . . . . 8
⊢ (𝑠 ∈ 𝒫 𝒫
𝑂 ↔ 𝑠 ⊆ 𝒫 𝑂) |
| 10 | 8, 9 | sylibr 234 |
. . . . . . 7
⊢ (𝑠 ∈ (sigAlgebra‘𝑂) → 𝑠 ∈ 𝒫 𝒫 𝑂) |
| 11 | 10 | ssriv 3987 |
. . . . . 6
⊢
(sigAlgebra‘𝑂)
⊆ 𝒫 𝒫 𝑂 |
| 12 | 7, 11 | sstrdi 3996 |
. . . . 5
⊢ (𝐴 ∈ 𝒫
(sigAlgebra‘𝑂) →
𝐴 ⊆ 𝒫
𝒫 𝑂) |
| 13 | 6, 12 | syl 17 |
. . . 4
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ 𝐴 ⊆ 𝒫
𝒫 𝑂) |
| 14 | | sspwuni 5100 |
. . . 4
⊢ (𝐴 ⊆ 𝒫 𝒫
𝑂 ↔ ∪ 𝐴
⊆ 𝒫 𝑂) |
| 15 | 13, 14 | sylib 218 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ ∪ 𝐴 ⊆ 𝒫 𝑂) |
| 16 | 5, 15 | sstrd 3994 |
. 2
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ ∩ 𝐴 ⊆ 𝒫 𝑂) |
| 17 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑠 ∈ 𝐴) → 𝑠 ∈ 𝐴) |
| 18 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑠 ∈ 𝐴) → 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) |
| 19 | | elelpwi 4610 |
. . . . . . . . 9
⊢ ((𝑠 ∈ 𝐴 ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → 𝑠 ∈ (sigAlgebra‘𝑂)) |
| 20 | 17, 18, 19 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑠 ∈ 𝐴) → 𝑠 ∈ (sigAlgebra‘𝑂)) |
| 21 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑠 ∈ V |
| 22 | | issiga 34113 |
. . . . . . . . 9
⊢ (𝑠 ∈ V → (𝑠 ∈ (sigAlgebra‘𝑂) ↔ (𝑠 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠))))) |
| 23 | 21, 22 | ax-mp 5 |
. . . . . . . 8
⊢ (𝑠 ∈ (sigAlgebra‘𝑂) ↔ (𝑠 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)))) |
| 24 | 20, 23 | sylib 218 |
. . . . . . 7
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑠 ∈ 𝐴) → (𝑠 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)))) |
| 25 | 24 | simprd 495 |
. . . . . 6
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑠 ∈ 𝐴) → (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠))) |
| 26 | 25 | simp1d 1143 |
. . . . 5
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑠 ∈ 𝐴) → 𝑂 ∈ 𝑠) |
| 27 | 26 | ralrimiva 3146 |
. . . 4
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ ∀𝑠 ∈
𝐴 𝑂 ∈ 𝑠) |
| 28 | | n0 4353 |
. . . . . . . . 9
⊢ (𝐴 ≠ ∅ ↔
∃𝑠 𝑠 ∈ 𝐴) |
| 29 | 28 | biimpi 216 |
. . . . . . . 8
⊢ (𝐴 ≠ ∅ →
∃𝑠 𝑠 ∈ 𝐴) |
| 30 | 29 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ ∃𝑠 𝑠 ∈ 𝐴) |
| 31 | 20 | ex 412 |
. . . . . . . 8
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ (𝑠 ∈ 𝐴 → 𝑠 ∈ (sigAlgebra‘𝑂))) |
| 32 | 31 | eximdv 1917 |
. . . . . . 7
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ (∃𝑠 𝑠 ∈ 𝐴 → ∃𝑠 𝑠 ∈ (sigAlgebra‘𝑂))) |
| 33 | 30, 32 | mpd 15 |
. . . . . 6
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ ∃𝑠 𝑠 ∈ (sigAlgebra‘𝑂)) |
| 34 | | elfvex 6944 |
. . . . . . 7
⊢ (𝑠 ∈ (sigAlgebra‘𝑂) → 𝑂 ∈ V) |
| 35 | 34 | exlimiv 1930 |
. . . . . 6
⊢
(∃𝑠 𝑠 ∈ (sigAlgebra‘𝑂) → 𝑂 ∈ V) |
| 36 | 33, 35 | syl 17 |
. . . . 5
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ 𝑂 ∈
V) |
| 37 | | elintg 4954 |
. . . . 5
⊢ (𝑂 ∈ V → (𝑂 ∈ ∩ 𝐴
↔ ∀𝑠 ∈
𝐴 𝑂 ∈ 𝑠)) |
| 38 | 36, 37 | syl 17 |
. . . 4
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ (𝑂 ∈ ∩ 𝐴
↔ ∀𝑠 ∈
𝐴 𝑂 ∈ 𝑠)) |
| 39 | 27, 38 | mpbird 257 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ 𝑂 ∈ ∩ 𝐴) |
| 40 | | simpll 767 |
. . . . . . . 8
⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ ∩ 𝐴)
∧ 𝑠 ∈ 𝐴) → (𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂))) |
| 41 | | simpr 484 |
. . . . . . . 8
⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ ∩ 𝐴)
∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ 𝐴) |
| 42 | 40, 41 | jca 511 |
. . . . . . 7
⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ ∩ 𝐴)
∧ 𝑠 ∈ 𝐴) → ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴)) |
| 43 | | elinti 4955 |
. . . . . . . . 9
⊢ (𝑥 ∈ ∩ 𝐴
→ (𝑠 ∈ 𝐴 → 𝑥 ∈ 𝑠)) |
| 44 | 43 | imp 406 |
. . . . . . . 8
⊢ ((𝑥 ∈ ∩ 𝐴
∧ 𝑠 ∈ 𝐴) → 𝑥 ∈ 𝑠) |
| 45 | 44 | adantll 714 |
. . . . . . 7
⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ ∩ 𝐴)
∧ 𝑠 ∈ 𝐴) → 𝑥 ∈ 𝑠) |
| 46 | 25 | simp2d 1144 |
. . . . . . . 8
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑠 ∈ 𝐴) → ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠) |
| 47 | 46 | r19.21bi 3251 |
. . . . . . 7
⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑠 ∈ 𝐴) ∧ 𝑥 ∈ 𝑠) → (𝑂 ∖ 𝑥) ∈ 𝑠) |
| 48 | 42, 45, 47 | syl2anc 584 |
. . . . . 6
⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ ∩ 𝐴)
∧ 𝑠 ∈ 𝐴) → (𝑂 ∖ 𝑥) ∈ 𝑠) |
| 49 | 48 | ralrimiva 3146 |
. . . . 5
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ ∩ 𝐴)
→ ∀𝑠 ∈
𝐴 (𝑂 ∖ 𝑥) ∈ 𝑠) |
| 50 | 36 | difexd 5331 |
. . . . . . 7
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ (𝑂 ∖ 𝑥) ∈ V) |
| 51 | 50 | adantr 480 |
. . . . . 6
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ ∩ 𝐴)
→ (𝑂 ∖ 𝑥) ∈ V) |
| 52 | | elintg 4954 |
. . . . . 6
⊢ ((𝑂 ∖ 𝑥) ∈ V → ((𝑂 ∖ 𝑥) ∈ ∩ 𝐴 ↔ ∀𝑠 ∈ 𝐴 (𝑂 ∖ 𝑥) ∈ 𝑠)) |
| 53 | 51, 52 | syl 17 |
. . . . 5
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ ∩ 𝐴)
→ ((𝑂 ∖ 𝑥) ∈ ∩ 𝐴
↔ ∀𝑠 ∈
𝐴 (𝑂 ∖ 𝑥) ∈ 𝑠)) |
| 54 | 49, 53 | mpbird 257 |
. . . 4
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ ∩ 𝐴)
→ (𝑂 ∖ 𝑥) ∈ ∩ 𝐴) |
| 55 | 54 | ralrimiva 3146 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ ∀𝑥 ∈
∩ 𝐴(𝑂 ∖ 𝑥) ∈ ∩ 𝐴) |
| 56 | | simplll 775 |
. . . . . . . . . 10
⊢
(((((𝐴 ≠ ∅
∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ 𝒫 ∩ 𝐴)
∧ 𝑥 ≼ ω)
∧ 𝑠 ∈ 𝐴) → (𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂))) |
| 57 | | simpr 484 |
. . . . . . . . . 10
⊢
(((((𝐴 ≠ ∅
∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ 𝒫 ∩ 𝐴)
∧ 𝑥 ≼ ω)
∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ 𝐴) |
| 58 | 56, 57 | jca 511 |
. . . . . . . . 9
⊢
(((((𝐴 ≠ ∅
∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ 𝒫 ∩ 𝐴)
∧ 𝑥 ≼ ω)
∧ 𝑠 ∈ 𝐴) → ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴)) |
| 59 | | simpllr 776 |
. . . . . . . . . 10
⊢
(((((𝐴 ≠ ∅
∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ 𝒫 ∩ 𝐴)
∧ 𝑥 ≼ ω)
∧ 𝑠 ∈ 𝐴) → 𝑥 ∈ 𝒫 ∩ 𝐴) |
| 60 | | elpwi 4607 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝒫 ∩ 𝐴
→ 𝑥 ⊆ ∩ 𝐴) |
| 61 | | intss1 4963 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑠) |
| 62 | 60, 61 | sylan9ss 3997 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝒫 ∩ 𝐴
∧ 𝑠 ∈ 𝐴) → 𝑥 ⊆ 𝑠) |
| 63 | | velpw 4605 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝒫 𝑠 ↔ 𝑥 ⊆ 𝑠) |
| 64 | 62, 63 | sylibr 234 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝒫 ∩ 𝐴
∧ 𝑠 ∈ 𝐴) → 𝑥 ∈ 𝒫 𝑠) |
| 65 | 59, 64 | sylancom 588 |
. . . . . . . . 9
⊢
(((((𝐴 ≠ ∅
∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ 𝒫 ∩ 𝐴)
∧ 𝑥 ≼ ω)
∧ 𝑠 ∈ 𝐴) → 𝑥 ∈ 𝒫 𝑠) |
| 66 | 58, 65 | jca 511 |
. . . . . . . 8
⊢
(((((𝐴 ≠ ∅
∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ 𝒫 ∩ 𝐴)
∧ 𝑥 ≼ ω)
∧ 𝑠 ∈ 𝐴) → (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) ∧ 𝑥 ∈ 𝒫 𝑠)) |
| 67 | | simplr 769 |
. . . . . . . 8
⊢
(((((𝐴 ≠ ∅
∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ 𝒫 ∩ 𝐴)
∧ 𝑥 ≼ ω)
∧ 𝑠 ∈ 𝐴) → 𝑥 ≼ ω) |
| 68 | 25 | simp3d 1145 |
. . . . . . . . 9
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑠 ∈ 𝐴) → ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)) |
| 69 | 68 | r19.21bi 3251 |
. . . . . . . 8
⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑠 ∈ 𝐴) ∧ 𝑥 ∈ 𝒫 𝑠) → (𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)) |
| 70 | 66, 67, 69 | sylc 65 |
. . . . . . 7
⊢
(((((𝐴 ≠ ∅
∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ 𝒫 ∩ 𝐴)
∧ 𝑥 ≼ ω)
∧ 𝑠 ∈ 𝐴) → ∪ 𝑥
∈ 𝑠) |
| 71 | 70 | ralrimiva 3146 |
. . . . . 6
⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ 𝒫 ∩ 𝐴)
∧ 𝑥 ≼ ω)
→ ∀𝑠 ∈
𝐴 ∪ 𝑥
∈ 𝑠) |
| 72 | | uniexg 7760 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝒫 ∩ 𝐴
→ ∪ 𝑥 ∈ V) |
| 73 | 72 | ad2antlr 727 |
. . . . . . 7
⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ 𝒫 ∩ 𝐴)
∧ 𝑥 ≼ ω)
→ ∪ 𝑥 ∈ V) |
| 74 | | elintg 4954 |
. . . . . . 7
⊢ (∪ 𝑥
∈ V → (∪ 𝑥 ∈ ∩ 𝐴 ↔ ∀𝑠 ∈ 𝐴 ∪ 𝑥 ∈ 𝑠)) |
| 75 | 73, 74 | syl 17 |
. . . . . 6
⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ 𝒫 ∩ 𝐴)
∧ 𝑥 ≼ ω)
→ (∪ 𝑥 ∈ ∩ 𝐴 ↔ ∀𝑠 ∈ 𝐴 ∪ 𝑥 ∈ 𝑠)) |
| 76 | 71, 75 | mpbird 257 |
. . . . 5
⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ 𝒫 ∩ 𝐴)
∧ 𝑥 ≼ ω)
→ ∪ 𝑥 ∈ ∩ 𝐴) |
| 77 | 76 | ex 412 |
. . . 4
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂)) ∧
𝑥 ∈ 𝒫 ∩ 𝐴)
→ (𝑥 ≼ ω
→ ∪ 𝑥 ∈ ∩ 𝐴)) |
| 78 | 77 | ralrimiva 3146 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ ∀𝑥 ∈
𝒫 ∩ 𝐴(𝑥 ≼ ω → ∪ 𝑥
∈ ∩ 𝐴)) |
| 79 | 39, 55, 78 | 3jca 1129 |
. 2
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ (𝑂 ∈ ∩ 𝐴
∧ ∀𝑥 ∈
∩ 𝐴(𝑂 ∖ 𝑥) ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ 𝒫 ∩ 𝐴(𝑥 ≼ ω → ∪ 𝑥
∈ ∩ 𝐴))) |
| 80 | | issiga 34113 |
. . 3
⊢ (∩ 𝐴
∈ V → (∩ 𝐴 ∈ (sigAlgebra‘𝑂) ↔ (∩ 𝐴 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ ∩ 𝐴(𝑂 ∖ 𝑥) ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ 𝒫 ∩ 𝐴(𝑥 ≼ ω → ∪ 𝑥
∈ ∩ 𝐴))))) |
| 81 | 80 | biimpar 477 |
. 2
⊢ ((∩ 𝐴
∈ V ∧ (∩ 𝐴 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ ∩ 𝐴(𝑂 ∖ 𝑥) ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ 𝒫 ∩ 𝐴(𝑥 ≼ ω → ∪ 𝑥
∈ ∩ 𝐴)))) → ∩
𝐴 ∈
(sigAlgebra‘𝑂)) |
| 82 | 3, 16, 79, 81 | syl12anc 837 |
1
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫
(sigAlgebra‘𝑂))
→ ∩ 𝐴 ∈ (sigAlgebra‘𝑂)) |