Step | Hyp | Ref
| Expression |
1 | | isrnsigau 32095 |
. . . . . . . 8
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (𝑆 ⊆ 𝒫 ∪ 𝑆
∧ (∪ 𝑆 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∪ 𝑆 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆)))) |
2 | 1 | simprd 496 |
. . . . . . 7
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (∪
𝑆 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∪ 𝑆 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆))) |
3 | 2 | simp2d 1142 |
. . . . . 6
⊢ (𝑆 ∈ ∪ ran sigAlgebra → ∀𝑥 ∈ 𝑆 (∪ 𝑆 ∖ 𝑥) ∈ 𝑆) |
4 | 3 | adantr 481 |
. . . . 5
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → ∀𝑥 ∈ 𝑆 (∪ 𝑆 ∖ 𝑥) ∈ 𝑆) |
5 | | elpwi 4542 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝒫 𝑆 → 𝐴 ⊆ 𝑆) |
6 | | ssrexv 3988 |
. . . . . . . . . . . 12
⊢ (𝐴 ⊆ 𝑆 → (∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧) → ∃𝑧 ∈ 𝑆 𝑦 = (∪ 𝑆 ∖ 𝑧))) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝒫 𝑆 → (∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧) → ∃𝑧 ∈ 𝑆 𝑦 = (∪ 𝑆 ∖ 𝑧))) |
8 | 7 | ss2abdv 3997 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝒫 𝑆 → {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ⊆ {𝑦 ∣ ∃𝑧 ∈ 𝑆 𝑦 = (∪ 𝑆 ∖ 𝑧)}) |
9 | | isrnsigau 32095 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (𝑆 ⊆ 𝒫 ∪ 𝑆
∧ (∪ 𝑆 ∈ 𝑆 ∧ ∀𝑧 ∈ 𝑆 (∪ 𝑆 ∖ 𝑧) ∈ 𝑆 ∧ ∀𝑧 ∈ 𝒫 𝑆(𝑧 ≼ ω → ∪ 𝑧
∈ 𝑆)))) |
10 | 9 | simprd 496 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (∪
𝑆 ∈ 𝑆 ∧ ∀𝑧 ∈ 𝑆 (∪ 𝑆 ∖ 𝑧) ∈ 𝑆 ∧ ∀𝑧 ∈ 𝒫 𝑆(𝑧 ≼ ω → ∪ 𝑧
∈ 𝑆))) |
11 | 10 | simp2d 1142 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ ∪ ran sigAlgebra → ∀𝑧 ∈ 𝑆 (∪ 𝑆 ∖ 𝑧) ∈ 𝑆) |
12 | | uniiunlem 4019 |
. . . . . . . . . . . 12
⊢
(∀𝑧 ∈
𝑆 (∪ 𝑆
∖ 𝑧) ∈ 𝑆 → (∀𝑧 ∈ 𝑆 (∪ 𝑆 ∖ 𝑧) ∈ 𝑆 ↔ {𝑦 ∣ ∃𝑧 ∈ 𝑆 𝑦 = (∪ 𝑆 ∖ 𝑧)} ⊆ 𝑆)) |
13 | 11, 12 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (∀𝑧 ∈ 𝑆 (∪ 𝑆 ∖ 𝑧) ∈ 𝑆 ↔ {𝑦 ∣ ∃𝑧 ∈ 𝑆 𝑦 = (∪ 𝑆 ∖ 𝑧)} ⊆ 𝑆)) |
14 | 11, 13 | mpbid 231 |
. . . . . . . . . 10
⊢ (𝑆 ∈ ∪ ran sigAlgebra → {𝑦 ∣ ∃𝑧 ∈ 𝑆 𝑦 = (∪ 𝑆 ∖ 𝑧)} ⊆ 𝑆) |
15 | 8, 14 | sylan9ssr 3935 |
. . . . . . . . 9
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ⊆ 𝑆) |
16 | | abrexexg 7803 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝒫 𝑆 → {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ∈ V) |
17 | | elpwg 4536 |
. . . . . . . . . . 11
⊢ ({𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ∈ V → ({𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ∈ 𝒫 𝑆 ↔ {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ⊆ 𝑆)) |
18 | 16, 17 | syl 17 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝒫 𝑆 → ({𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ∈ 𝒫 𝑆 ↔ {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ⊆ 𝑆)) |
19 | 18 | adantl 482 |
. . . . . . . . 9
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → ({𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ∈ 𝒫 𝑆 ↔ {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ⊆ 𝑆)) |
20 | 15, 19 | mpbird 256 |
. . . . . . . 8
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ∈ 𝒫 𝑆) |
21 | 2 | simp3d 1143 |
. . . . . . . . 9
⊢ (𝑆 ∈ ∪ ran sigAlgebra → ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆)) |
22 | 21 | adantr 481 |
. . . . . . . 8
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆)) |
23 | 20, 22 | jca 512 |
. . . . . . 7
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → ({𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ∈ 𝒫 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆))) |
24 | | abrexdom2jm 30853 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝒫 𝑆 → {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ≼ 𝐴) |
25 | | domtr 8793 |
. . . . . . . . . 10
⊢ (({𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ≼ 𝐴 ∧ 𝐴 ≼ ω) → {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ≼ ω) |
26 | 24, 25 | sylan 580 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝒫 𝑆 ∧ 𝐴 ≼ ω) → {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ≼ ω) |
27 | 26 | ex 413 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝒫 𝑆 → (𝐴 ≼ ω → {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ≼ ω)) |
28 | 27 | adantl 482 |
. . . . . . 7
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → (𝐴 ≼ ω → {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ≼ ω)) |
29 | | breq1 5077 |
. . . . . . . . 9
⊢ (𝑥 = {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} → (𝑥 ≼ ω ↔ {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ≼ ω)) |
30 | | unieq 4850 |
. . . . . . . . . 10
⊢ (𝑥 = {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} → ∪ 𝑥 = ∪
{𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)}) |
31 | 30 | eleq1d 2823 |
. . . . . . . . 9
⊢ (𝑥 = {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} → (∪ 𝑥 ∈ 𝑆 ↔ ∪ {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ∈ 𝑆)) |
32 | 29, 31 | imbi12d 345 |
. . . . . . . 8
⊢ (𝑥 = {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} → ((𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆) ↔ ({𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ≼ ω → ∪ {𝑦
∣ ∃𝑧 ∈
𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ∈ 𝑆))) |
33 | 32 | rspcva 3559 |
. . . . . . 7
⊢ (({𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ∈ 𝒫 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆)) → ({𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ≼ ω → ∪ {𝑦
∣ ∃𝑧 ∈
𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ∈ 𝑆)) |
34 | 23, 28, 33 | sylsyld 61 |
. . . . . 6
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → (𝐴 ≼ ω → ∪ {𝑦
∣ ∃𝑧 ∈
𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ∈ 𝑆)) |
35 | 5 | adantl 482 |
. . . . . . . 8
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → 𝐴 ⊆ 𝑆) |
36 | 11 | adantr 481 |
. . . . . . . 8
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → ∀𝑧 ∈ 𝑆 (∪ 𝑆 ∖ 𝑧) ∈ 𝑆) |
37 | | ssralv 3987 |
. . . . . . . 8
⊢ (𝐴 ⊆ 𝑆 → (∀𝑧 ∈ 𝑆 (∪ 𝑆 ∖ 𝑧) ∈ 𝑆 → ∀𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧) ∈ 𝑆)) |
38 | 35, 36, 37 | sylc 65 |
. . . . . . 7
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → ∀𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧) ∈ 𝑆) |
39 | | dfiun2g 4960 |
. . . . . . 7
⊢
(∀𝑧 ∈
𝐴 (∪ 𝑆
∖ 𝑧) ∈ 𝑆 → ∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧) = ∪ {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)}) |
40 | | eleq1 2826 |
. . . . . . 7
⊢ (∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧) = ∪ {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} → (∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧) ∈ 𝑆 ↔ ∪ {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ∈ 𝑆)) |
41 | 38, 39, 40 | 3syl 18 |
. . . . . 6
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → (∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧) ∈ 𝑆 ↔ ∪ {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ∈ 𝑆)) |
42 | 34, 41 | sylibrd 258 |
. . . . 5
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → (𝐴 ≼ ω → ∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧) ∈ 𝑆)) |
43 | | difeq2 4051 |
. . . . . . 7
⊢ (𝑥 = ∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧) → (∪ 𝑆 ∖ 𝑥) = (∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧))) |
44 | 43 | eleq1d 2823 |
. . . . . 6
⊢ (𝑥 = ∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧) → ((∪ 𝑆 ∖ 𝑥) ∈ 𝑆 ↔ (∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧)) ∈ 𝑆)) |
45 | 44 | rspccv 3558 |
. . . . 5
⊢
(∀𝑥 ∈
𝑆 (∪ 𝑆
∖ 𝑥) ∈ 𝑆 → (∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧) ∈ 𝑆 → (∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧)) ∈ 𝑆)) |
46 | 4, 42, 45 | sylsyld 61 |
. . . 4
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → (𝐴 ≼ ω → (∪ 𝑆
∖ ∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧)) ∈ 𝑆)) |
47 | 46 | adantrd 492 |
. . 3
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → ((𝐴 ≼ ω ∧ 𝐴 ≠ ∅) → (∪ 𝑆
∖ ∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧)) ∈ 𝑆)) |
48 | 47 | imp 407 |
. 2
⊢ (((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) ∧ (𝐴 ≼ ω ∧ 𝐴 ≠ ∅)) → (∪ 𝑆
∖ ∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧)) ∈ 𝑆) |
49 | | simpr 485 |
. . . . . 6
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → 𝐴 ∈ 𝒫 𝑆) |
50 | | pwuni 4878 |
. . . . . . 7
⊢ 𝑆 ⊆ 𝒫 ∪ 𝑆 |
51 | 5, 50 | sstrdi 3933 |
. . . . . 6
⊢ (𝐴 ∈ 𝒫 𝑆 → 𝐴 ⊆ 𝒫 ∪ 𝑆) |
52 | | iundifdifd 30901 |
. . . . . 6
⊢ (𝐴 ⊆ 𝒫 ∪ 𝑆
→ (𝐴 ≠ ∅
→ ∩ 𝐴 = (∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧)))) |
53 | 49, 51, 52 | 3syl 18 |
. . . . 5
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → (𝐴 ≠ ∅ → ∩ 𝐴 =
(∪ 𝑆 ∖ ∪
𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧)))) |
54 | 53 | adantld 491 |
. . . 4
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → ((𝐴 ≼ ω ∧ 𝐴 ≠ ∅) → ∩ 𝐴 =
(∪ 𝑆 ∖ ∪
𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧)))) |
55 | | eleq1 2826 |
. . . 4
⊢ (∩ 𝐴 =
(∪ 𝑆 ∖ ∪
𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧)) → (∩ 𝐴 ∈ 𝑆 ↔ (∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧)) ∈ 𝑆)) |
56 | 54, 55 | syl6 35 |
. . 3
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → ((𝐴 ≼ ω ∧ 𝐴 ≠ ∅) → (∩ 𝐴
∈ 𝑆 ↔ (∪ 𝑆
∖ ∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧)) ∈ 𝑆))) |
57 | 56 | imp 407 |
. 2
⊢ (((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) ∧ (𝐴 ≼ ω ∧ 𝐴 ≠ ∅)) → (∩ 𝐴
∈ 𝑆 ↔ (∪ 𝑆
∖ ∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧)) ∈ 𝑆)) |
58 | 48, 57 | mpbird 256 |
1
⊢ (((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) ∧ (𝐴 ≼ ω ∧ 𝐴 ≠ ∅)) → ∩ 𝐴
∈ 𝑆) |