Proof of Theorem sigapildsyslem
Step | Hyp | Ref
| Expression |
1 | | iuneq1 4894 |
. . . . . . 7
⊢ (𝑁 = ∅ → ∪ 𝑛 ∈ 𝑁 𝐵 = ∪ 𝑛 ∈ ∅ 𝐵) |
2 | | 0iun 4945 |
. . . . . . 7
⊢ ∪ 𝑛 ∈ ∅ 𝐵 = ∅ |
3 | 1, 2 | eqtrdi 2789 |
. . . . . 6
⊢ (𝑁 = ∅ → ∪ 𝑛 ∈ 𝑁 𝐵 = ∅) |
4 | 3 | difeq2d 4011 |
. . . . 5
⊢ (𝑁 = ∅ → (𝐴 ∖ ∪ 𝑛 ∈ 𝑁 𝐵) = (𝐴 ∖ ∅)) |
5 | | dif0 4259 |
. . . . 5
⊢ (𝐴 ∖ ∅) = 𝐴 |
6 | 4, 5 | eqtrdi 2789 |
. . . 4
⊢ (𝑁 = ∅ → (𝐴 ∖ ∪ 𝑛 ∈ 𝑁 𝐵) = 𝐴) |
7 | 6 | adantl 485 |
. . 3
⊢ ((𝜑 ∧ 𝑁 = ∅) → (𝐴 ∖ ∪
𝑛 ∈ 𝑁 𝐵) = 𝐴) |
8 | | sigapildsyslem.2 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑡) |
9 | 8 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ 𝑁 = ∅) → 𝐴 ∈ 𝑡) |
10 | 7, 9 | eqeltrd 2833 |
. 2
⊢ ((𝜑 ∧ 𝑁 = ∅) → (𝐴 ∖ ∪
𝑛 ∈ 𝑁 𝐵) ∈ 𝑡) |
11 | | iindif2 4959 |
. . . 4
⊢ (𝑁 ≠ ∅ → ∩ 𝑛 ∈ 𝑁 (𝐴 ∖ 𝐵) = (𝐴 ∖ ∪
𝑛 ∈ 𝑁 𝐵)) |
12 | 11 | adantl 485 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ≠ ∅) → ∩ 𝑛 ∈ 𝑁 (𝐴 ∖ 𝐵) = (𝐴 ∖ ∪
𝑛 ∈ 𝑁 𝐵)) |
13 | | sigapildsyslem.1 |
. . . . . . . 8
⊢ (𝜑 → 𝑡 ∈ (𝑃 ∩ 𝐿)) |
14 | 13 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ≠ ∅) → 𝑡 ∈ (𝑃 ∩ 𝐿)) |
15 | 14 | elin1d 4086 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ≠ ∅) → 𝑡 ∈ 𝑃) |
16 | | dynkin.p |
. . . . . . 7
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠} |
17 | 16 | ispisys 31682 |
. . . . . 6
⊢ (𝑡 ∈ 𝑃 ↔ (𝑡 ∈ 𝒫 𝒫 𝑂 ∧ (fi‘𝑡) ⊆ 𝑡)) |
18 | 15, 17 | sylib 221 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ≠ ∅) → (𝑡 ∈ 𝒫 𝒫 𝑂 ∧ (fi‘𝑡) ⊆ 𝑡)) |
19 | 18 | simprd 499 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ≠ ∅) → (fi‘𝑡) ⊆ 𝑡) |
20 | | sigapildsyslem.n |
. . . . . . 7
⊢
Ⅎ𝑛𝜑 |
21 | | nfv 1920 |
. . . . . . 7
⊢
Ⅎ𝑛 𝑁 ≠ ∅ |
22 | 20, 21 | nfan 1905 |
. . . . . 6
⊢
Ⅎ𝑛(𝜑 ∧ 𝑁 ≠ ∅) |
23 | 18 | simpld 498 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 ≠ ∅) → 𝑡 ∈ 𝒫 𝒫 𝑂) |
24 | 23 | elpwid 4496 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ≠ ∅) → 𝑡 ⊆ 𝒫 𝑂) |
25 | 8 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ≠ ∅) → 𝐴 ∈ 𝑡) |
26 | 24, 25 | sseldd 3876 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ≠ ∅) → 𝐴 ∈ 𝒫 𝑂) |
27 | 26 | elpwid 4496 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ≠ ∅) → 𝐴 ⊆ 𝑂) |
28 | 27 | adantr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑁 ≠ ∅) ∧ 𝑛 ∈ 𝑁) → 𝐴 ⊆ 𝑂) |
29 | | difin2 4180 |
. . . . . . . . 9
⊢ (𝐴 ⊆ 𝑂 → (𝐴 ∖ 𝐵) = ((𝑂 ∖ 𝐵) ∩ 𝐴)) |
30 | 28, 29 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑁 ≠ ∅) ∧ 𝑛 ∈ 𝑁) → (𝐴 ∖ 𝐵) = ((𝑂 ∖ 𝐵) ∩ 𝐴)) |
31 | 19 | adantr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑁 ≠ ∅) ∧ 𝑛 ∈ 𝑁) → (fi‘𝑡) ⊆ 𝑡) |
32 | 14 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑁 ≠ ∅) ∧ 𝑛 ∈ 𝑁) → 𝑡 ∈ (𝑃 ∩ 𝐿)) |
33 | 14 | elin2d 4087 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑁 ≠ ∅) → 𝑡 ∈ 𝐿) |
34 | | dynkin.l |
. . . . . . . . . . . . . . . 16
⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))} |
35 | 34 | isldsys 31686 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ 𝐿 ↔ (𝑡 ∈ 𝒫 𝒫 𝑂 ∧ (∅ ∈ 𝑡 ∧ ∀𝑥 ∈ 𝑡 (𝑂 ∖ 𝑥) ∈ 𝑡 ∧ ∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑡)))) |
36 | 33, 35 | sylib 221 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑁 ≠ ∅) → (𝑡 ∈ 𝒫 𝒫 𝑂 ∧ (∅ ∈ 𝑡 ∧ ∀𝑥 ∈ 𝑡 (𝑂 ∖ 𝑥) ∈ 𝑡 ∧ ∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑡)))) |
37 | 36 | simprd 499 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 ≠ ∅) → (∅ ∈ 𝑡 ∧ ∀𝑥 ∈ 𝑡 (𝑂 ∖ 𝑥) ∈ 𝑡 ∧ ∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑡))) |
38 | 37 | simp2d 1144 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ≠ ∅) → ∀𝑥 ∈ 𝑡 (𝑂 ∖ 𝑥) ∈ 𝑡) |
39 | 38 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑁 ≠ ∅) ∧ 𝑛 ∈ 𝑁) → ∀𝑥 ∈ 𝑡 (𝑂 ∖ 𝑥) ∈ 𝑡) |
40 | | sigapildsyslem.4 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝐵 ∈ 𝑡) |
41 | 40 | adantlr 715 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑁 ≠ ∅) ∧ 𝑛 ∈ 𝑁) → 𝐵 ∈ 𝑡) |
42 | | nfv 1920 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(𝑂 ∖ 𝐵) ∈ 𝑡 |
43 | | difeq2 4005 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐵 → (𝑂 ∖ 𝑥) = (𝑂 ∖ 𝐵)) |
44 | 43 | eleq1d 2817 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝐵 → ((𝑂 ∖ 𝑥) ∈ 𝑡 ↔ (𝑂 ∖ 𝐵) ∈ 𝑡)) |
45 | 42, 44 | rspc 3512 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ 𝑡 → (∀𝑥 ∈ 𝑡 (𝑂 ∖ 𝑥) ∈ 𝑡 → (𝑂 ∖ 𝐵) ∈ 𝑡)) |
46 | 41, 45 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑁 ≠ ∅) ∧ 𝑛 ∈ 𝑁) → (∀𝑥 ∈ 𝑡 (𝑂 ∖ 𝑥) ∈ 𝑡 → (𝑂 ∖ 𝐵) ∈ 𝑡)) |
47 | 39, 46 | mpd 15 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑁 ≠ ∅) ∧ 𝑛 ∈ 𝑁) → (𝑂 ∖ 𝐵) ∈ 𝑡) |
48 | 25 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑁 ≠ ∅) ∧ 𝑛 ∈ 𝑁) → 𝐴 ∈ 𝑡) |
49 | | inelfi 8948 |
. . . . . . . . . 10
⊢ ((𝑡 ∈ (𝑃 ∩ 𝐿) ∧ (𝑂 ∖ 𝐵) ∈ 𝑡 ∧ 𝐴 ∈ 𝑡) → ((𝑂 ∖ 𝐵) ∩ 𝐴) ∈ (fi‘𝑡)) |
50 | 32, 47, 48, 49 | syl3anc 1372 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑁 ≠ ∅) ∧ 𝑛 ∈ 𝑁) → ((𝑂 ∖ 𝐵) ∩ 𝐴) ∈ (fi‘𝑡)) |
51 | 31, 50 | sseldd 3876 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑁 ≠ ∅) ∧ 𝑛 ∈ 𝑁) → ((𝑂 ∖ 𝐵) ∩ 𝐴) ∈ 𝑡) |
52 | 30, 51 | eqeltrd 2833 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑁 ≠ ∅) ∧ 𝑛 ∈ 𝑁) → (𝐴 ∖ 𝐵) ∈ 𝑡) |
53 | 52 | ex 416 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ≠ ∅) → (𝑛 ∈ 𝑁 → (𝐴 ∖ 𝐵) ∈ 𝑡)) |
54 | 22, 53 | ralrimi 3127 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ≠ ∅) → ∀𝑛 ∈ 𝑁 (𝐴 ∖ 𝐵) ∈ 𝑡) |
55 | | simpr 488 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ≠ ∅) → 𝑁 ≠ ∅) |
56 | | sigapildsyslem.3 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ Fin) |
57 | 56 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ≠ ∅) → 𝑁 ∈ Fin) |
58 | | vex 3401 |
. . . . . 6
⊢ 𝑡 ∈ V |
59 | | iinfi 8947 |
. . . . . 6
⊢ ((𝑡 ∈ V ∧ (∀𝑛 ∈ 𝑁 (𝐴 ∖ 𝐵) ∈ 𝑡 ∧ 𝑁 ≠ ∅ ∧ 𝑁 ∈ Fin)) → ∩ 𝑛 ∈ 𝑁 (𝐴 ∖ 𝐵) ∈ (fi‘𝑡)) |
60 | 58, 59 | mpan 690 |
. . . . 5
⊢
((∀𝑛 ∈
𝑁 (𝐴 ∖ 𝐵) ∈ 𝑡 ∧ 𝑁 ≠ ∅ ∧ 𝑁 ∈ Fin) → ∩ 𝑛 ∈ 𝑁 (𝐴 ∖ 𝐵) ∈ (fi‘𝑡)) |
61 | 54, 55, 57, 60 | syl3anc 1372 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ≠ ∅) → ∩ 𝑛 ∈ 𝑁 (𝐴 ∖ 𝐵) ∈ (fi‘𝑡)) |
62 | 19, 61 | sseldd 3876 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ≠ ∅) → ∩ 𝑛 ∈ 𝑁 (𝐴 ∖ 𝐵) ∈ 𝑡) |
63 | 12, 62 | eqeltrrd 2834 |
. 2
⊢ ((𝜑 ∧ 𝑁 ≠ ∅) → (𝐴 ∖ ∪
𝑛 ∈ 𝑁 𝐵) ∈ 𝑡) |
64 | 10, 63 | pm2.61dane 3021 |
1
⊢ (𝜑 → (𝐴 ∖ ∪
𝑛 ∈ 𝑁 𝐵) ∈ 𝑡) |