| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | isrnsigau 34129 | . . . . . . . 8
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (𝑆 ⊆ 𝒫 ∪ 𝑆
∧ (∪ 𝑆 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∪ 𝑆 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆)))) | 
| 2 | 1 | simprd 495 | . . . . . . 7
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (∪
𝑆 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∪ 𝑆 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆))) | 
| 3 | 2 | simp2d 1143 | . . . . . 6
⊢ (𝑆 ∈ ∪ ran sigAlgebra → ∀𝑥 ∈ 𝑆 (∪ 𝑆 ∖ 𝑥) ∈ 𝑆) | 
| 4 | 3 | adantr 480 | . . . . 5
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → ∀𝑥 ∈ 𝑆 (∪ 𝑆 ∖ 𝑥) ∈ 𝑆) | 
| 5 |  | elpwi 4606 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝒫 𝑆 → 𝐴 ⊆ 𝑆) | 
| 6 |  | ssrexv 4052 | . . . . . . . . . . . 12
⊢ (𝐴 ⊆ 𝑆 → (∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧) → ∃𝑧 ∈ 𝑆 𝑦 = (∪ 𝑆 ∖ 𝑧))) | 
| 7 | 5, 6 | syl 17 | . . . . . . . . . . 11
⊢ (𝐴 ∈ 𝒫 𝑆 → (∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧) → ∃𝑧 ∈ 𝑆 𝑦 = (∪ 𝑆 ∖ 𝑧))) | 
| 8 | 7 | ss2abdv 4065 | . . . . . . . . . 10
⊢ (𝐴 ∈ 𝒫 𝑆 → {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ⊆ {𝑦 ∣ ∃𝑧 ∈ 𝑆 𝑦 = (∪ 𝑆 ∖ 𝑧)}) | 
| 9 |  | isrnsigau 34129 | . . . . . . . . . . . . 13
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (𝑆 ⊆ 𝒫 ∪ 𝑆
∧ (∪ 𝑆 ∈ 𝑆 ∧ ∀𝑧 ∈ 𝑆 (∪ 𝑆 ∖ 𝑧) ∈ 𝑆 ∧ ∀𝑧 ∈ 𝒫 𝑆(𝑧 ≼ ω → ∪ 𝑧
∈ 𝑆)))) | 
| 10 | 9 | simprd 495 | . . . . . . . . . . . 12
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (∪
𝑆 ∈ 𝑆 ∧ ∀𝑧 ∈ 𝑆 (∪ 𝑆 ∖ 𝑧) ∈ 𝑆 ∧ ∀𝑧 ∈ 𝒫 𝑆(𝑧 ≼ ω → ∪ 𝑧
∈ 𝑆))) | 
| 11 | 10 | simp2d 1143 | . . . . . . . . . . 11
⊢ (𝑆 ∈ ∪ ran sigAlgebra → ∀𝑧 ∈ 𝑆 (∪ 𝑆 ∖ 𝑧) ∈ 𝑆) | 
| 12 |  | uniiunlem 4086 | . . . . . . . . . . . 12
⊢
(∀𝑧 ∈
𝑆 (∪ 𝑆
∖ 𝑧) ∈ 𝑆 → (∀𝑧 ∈ 𝑆 (∪ 𝑆 ∖ 𝑧) ∈ 𝑆 ↔ {𝑦 ∣ ∃𝑧 ∈ 𝑆 𝑦 = (∪ 𝑆 ∖ 𝑧)} ⊆ 𝑆)) | 
| 13 | 11, 12 | syl 17 | . . . . . . . . . . 11
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (∀𝑧 ∈ 𝑆 (∪ 𝑆 ∖ 𝑧) ∈ 𝑆 ↔ {𝑦 ∣ ∃𝑧 ∈ 𝑆 𝑦 = (∪ 𝑆 ∖ 𝑧)} ⊆ 𝑆)) | 
| 14 | 11, 13 | mpbid 232 | . . . . . . . . . 10
⊢ (𝑆 ∈ ∪ ran sigAlgebra → {𝑦 ∣ ∃𝑧 ∈ 𝑆 𝑦 = (∪ 𝑆 ∖ 𝑧)} ⊆ 𝑆) | 
| 15 | 8, 14 | sylan9ssr 3997 | . . . . . . . . 9
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ⊆ 𝑆) | 
| 16 |  | abrexexg 7986 | . . . . . . . . . . 11
⊢ (𝐴 ∈ 𝒫 𝑆 → {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ∈ V) | 
| 17 |  | elpwg 4602 | . . . . . . . . . . 11
⊢ ({𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ∈ V → ({𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ∈ 𝒫 𝑆 ↔ {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ⊆ 𝑆)) | 
| 18 | 16, 17 | syl 17 | . . . . . . . . . 10
⊢ (𝐴 ∈ 𝒫 𝑆 → ({𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ∈ 𝒫 𝑆 ↔ {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ⊆ 𝑆)) | 
| 19 | 18 | adantl 481 | . . . . . . . . 9
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → ({𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ∈ 𝒫 𝑆 ↔ {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ⊆ 𝑆)) | 
| 20 | 15, 19 | mpbird 257 | . . . . . . . 8
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ∈ 𝒫 𝑆) | 
| 21 | 2 | simp3d 1144 | . . . . . . . . 9
⊢ (𝑆 ∈ ∪ ran sigAlgebra → ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆)) | 
| 22 | 21 | adantr 480 | . . . . . . . 8
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆)) | 
| 23 | 20, 22 | jca 511 | . . . . . . 7
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → ({𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ∈ 𝒫 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆))) | 
| 24 |  | abrexdom2jm 32528 | . . . . . . . . . 10
⊢ (𝐴 ∈ 𝒫 𝑆 → {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ≼ 𝐴) | 
| 25 |  | domtr 9048 | . . . . . . . . . 10
⊢ (({𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ≼ 𝐴 ∧ 𝐴 ≼ ω) → {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ≼ ω) | 
| 26 | 24, 25 | sylan 580 | . . . . . . . . 9
⊢ ((𝐴 ∈ 𝒫 𝑆 ∧ 𝐴 ≼ ω) → {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ≼ ω) | 
| 27 | 26 | ex 412 | . . . . . . . 8
⊢ (𝐴 ∈ 𝒫 𝑆 → (𝐴 ≼ ω → {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ≼ ω)) | 
| 28 | 27 | adantl 481 | . . . . . . 7
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → (𝐴 ≼ ω → {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ≼ ω)) | 
| 29 |  | breq1 5145 | . . . . . . . . 9
⊢ (𝑥 = {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} → (𝑥 ≼ ω ↔ {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ≼ ω)) | 
| 30 |  | unieq 4917 | . . . . . . . . . 10
⊢ (𝑥 = {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} → ∪ 𝑥 = ∪
{𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)}) | 
| 31 | 30 | eleq1d 2825 | . . . . . . . . 9
⊢ (𝑥 = {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} → (∪ 𝑥 ∈ 𝑆 ↔ ∪ {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ∈ 𝑆)) | 
| 32 | 29, 31 | imbi12d 344 | . . . . . . . 8
⊢ (𝑥 = {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} → ((𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆) ↔ ({𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ≼ ω → ∪ {𝑦
∣ ∃𝑧 ∈
𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ∈ 𝑆))) | 
| 33 | 32 | rspcva 3619 | . . . . . . 7
⊢ (({𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ∈ 𝒫 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆)) → ({𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ≼ ω → ∪ {𝑦
∣ ∃𝑧 ∈
𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ∈ 𝑆)) | 
| 34 | 23, 28, 33 | sylsyld 61 | . . . . . 6
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → (𝐴 ≼ ω → ∪ {𝑦
∣ ∃𝑧 ∈
𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ∈ 𝑆)) | 
| 35 | 5 | adantl 481 | . . . . . . . 8
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → 𝐴 ⊆ 𝑆) | 
| 36 | 11 | adantr 480 | . . . . . . . 8
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → ∀𝑧 ∈ 𝑆 (∪ 𝑆 ∖ 𝑧) ∈ 𝑆) | 
| 37 |  | ssralv 4051 | . . . . . . . 8
⊢ (𝐴 ⊆ 𝑆 → (∀𝑧 ∈ 𝑆 (∪ 𝑆 ∖ 𝑧) ∈ 𝑆 → ∀𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧) ∈ 𝑆)) | 
| 38 | 35, 36, 37 | sylc 65 | . . . . . . 7
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → ∀𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧) ∈ 𝑆) | 
| 39 |  | dfiun2g 5029 | . . . . . . 7
⊢
(∀𝑧 ∈
𝐴 (∪ 𝑆
∖ 𝑧) ∈ 𝑆 → ∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧) = ∪ {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)}) | 
| 40 |  | eleq1 2828 | . . . . . . 7
⊢ (∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧) = ∪ {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} → (∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧) ∈ 𝑆 ↔ ∪ {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ∈ 𝑆)) | 
| 41 | 38, 39, 40 | 3syl 18 | . . . . . 6
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → (∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧) ∈ 𝑆 ↔ ∪ {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = (∪ 𝑆 ∖ 𝑧)} ∈ 𝑆)) | 
| 42 | 34, 41 | sylibrd 259 | . . . . 5
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → (𝐴 ≼ ω → ∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧) ∈ 𝑆)) | 
| 43 |  | difeq2 4119 | . . . . . . 7
⊢ (𝑥 = ∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧) → (∪ 𝑆 ∖ 𝑥) = (∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧))) | 
| 44 | 43 | eleq1d 2825 | . . . . . 6
⊢ (𝑥 = ∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧) → ((∪ 𝑆 ∖ 𝑥) ∈ 𝑆 ↔ (∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧)) ∈ 𝑆)) | 
| 45 | 44 | rspccv 3618 | . . . . 5
⊢
(∀𝑥 ∈
𝑆 (∪ 𝑆
∖ 𝑥) ∈ 𝑆 → (∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧) ∈ 𝑆 → (∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧)) ∈ 𝑆)) | 
| 46 | 4, 42, 45 | sylsyld 61 | . . . 4
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → (𝐴 ≼ ω → (∪ 𝑆
∖ ∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧)) ∈ 𝑆)) | 
| 47 | 46 | adantrd 491 | . . 3
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → ((𝐴 ≼ ω ∧ 𝐴 ≠ ∅) → (∪ 𝑆
∖ ∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧)) ∈ 𝑆)) | 
| 48 | 47 | imp 406 | . 2
⊢ (((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) ∧ (𝐴 ≼ ω ∧ 𝐴 ≠ ∅)) → (∪ 𝑆
∖ ∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧)) ∈ 𝑆) | 
| 49 |  | simpr 484 | . . . . . 6
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → 𝐴 ∈ 𝒫 𝑆) | 
| 50 |  | pwuni 4944 | . . . . . . 7
⊢ 𝑆 ⊆ 𝒫 ∪ 𝑆 | 
| 51 | 5, 50 | sstrdi 3995 | . . . . . 6
⊢ (𝐴 ∈ 𝒫 𝑆 → 𝐴 ⊆ 𝒫 ∪ 𝑆) | 
| 52 |  | iundifdifd 32575 | . . . . . 6
⊢ (𝐴 ⊆ 𝒫 ∪ 𝑆
→ (𝐴 ≠ ∅
→ ∩ 𝐴 = (∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧)))) | 
| 53 | 49, 51, 52 | 3syl 18 | . . . . 5
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → (𝐴 ≠ ∅ → ∩ 𝐴 =
(∪ 𝑆 ∖ ∪
𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧)))) | 
| 54 | 53 | adantld 490 | . . . 4
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → ((𝐴 ≼ ω ∧ 𝐴 ≠ ∅) → ∩ 𝐴 =
(∪ 𝑆 ∖ ∪
𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧)))) | 
| 55 |  | eleq1 2828 | . . . 4
⊢ (∩ 𝐴 =
(∪ 𝑆 ∖ ∪
𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧)) → (∩ 𝐴 ∈ 𝑆 ↔ (∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧)) ∈ 𝑆)) | 
| 56 | 54, 55 | syl6 35 | . . 3
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) → ((𝐴 ≼ ω ∧ 𝐴 ≠ ∅) → (∩ 𝐴
∈ 𝑆 ↔ (∪ 𝑆
∖ ∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧)) ∈ 𝑆))) | 
| 57 | 56 | imp 406 | . 2
⊢ (((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) ∧ (𝐴 ≼ ω ∧ 𝐴 ≠ ∅)) → (∩ 𝐴
∈ 𝑆 ↔ (∪ 𝑆
∖ ∪ 𝑧 ∈ 𝐴 (∪ 𝑆 ∖ 𝑧)) ∈ 𝑆)) | 
| 58 | 48, 57 | mpbird 257 | 1
⊢ (((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) ∧ (𝐴 ≼ ω ∧ 𝐴 ≠ ∅)) → ∩ 𝐴
∈ 𝑆) |