| Step | Hyp | Ref
| Expression |
| 1 | | ssrab2 4080 |
. . . 4
⊢ {𝑠 ∈ 𝒫 𝒫
𝑂 ∣ (∅ ∈
𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))} ⊆ 𝒫 𝒫 𝑂 |
| 2 | | ldgenpisys.e |
. . . . . 6
⊢ 𝐸 = ∩
{𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡} |
| 3 | | dynkin.l |
. . . . . . 7
⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))} |
| 4 | | dynkin.o |
. . . . . . 7
⊢ (𝜑 → 𝑂 ∈ 𝑉) |
| 5 | | ssrab2 4080 |
. . . . . . . . 9
⊢ {𝑠 ∈ 𝒫 𝒫
𝑂 ∣ (fi‘𝑠) ⊆ 𝑠} ⊆ 𝒫 𝒫 𝑂 |
| 6 | | ldgenpisys.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇 ∈ 𝑃) |
| 7 | | dynkin.p |
. . . . . . . . . 10
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠} |
| 8 | 6, 7 | eleqtrdi 2851 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}) |
| 9 | 5, 8 | sselid 3981 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ 𝒫 𝒫 𝑂) |
| 10 | 9 | elpwid 4609 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ⊆ 𝒫 𝑂) |
| 11 | 3, 4, 10 | ldsysgenld 34161 |
. . . . . 6
⊢ (𝜑 → ∩ {𝑡
∈ 𝐿 ∣ 𝑇 ⊆ 𝑡} ∈ 𝐿) |
| 12 | 2, 11 | eqeltrid 2845 |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ 𝐿) |
| 13 | 12, 3 | eleqtrdi 2851 |
. . . 4
⊢ (𝜑 → 𝐸 ∈ {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))}) |
| 14 | 1, 13 | sselid 3981 |
. . 3
⊢ (𝜑 → 𝐸 ∈ 𝒫 𝒫 𝑂) |
| 15 | | simprr 773 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸)) → 𝑏 ∈ 𝐸) |
| 16 | | simprl 771 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸)) → 𝑎 ∈ 𝐸) |
| 17 | 4 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐸) → 𝑂 ∈ 𝑉) |
| 18 | 6 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐸) → 𝑇 ∈ 𝑃) |
| 19 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐸) → 𝑎 ∈ 𝐸) |
| 20 | 10 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐸) → 𝑇 ⊆ 𝒫 𝑂) |
| 21 | 20 | sselda 3983 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐸) ∧ 𝑏 ∈ 𝑇) → 𝑏 ∈ 𝒫 𝑂) |
| 22 | | incom 4209 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 ∩ 𝑎) = (𝑎 ∩ 𝑏) |
| 23 | 4 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐸) ∧ 𝑏 ∈ 𝑇) → 𝑂 ∈ 𝑉) |
| 24 | 6 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐸) ∧ 𝑏 ∈ 𝑇) → 𝑇 ∈ 𝑃) |
| 25 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐸) ∧ 𝑏 ∈ 𝑇) → 𝑏 ∈ 𝑇) |
| 26 | 7, 3, 23, 2, 24, 25 | ldgenpisyslem3 34166 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐸) ∧ 𝑏 ∈ 𝑇) → 𝐸 ⊆ {𝑐 ∈ 𝒫 𝑂 ∣ (𝑏 ∩ 𝑐) ∈ 𝐸}) |
| 27 | | simplr 769 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐸) ∧ 𝑏 ∈ 𝑇) → 𝑎 ∈ 𝐸) |
| 28 | 26, 27 | sseldd 3984 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐸) ∧ 𝑏 ∈ 𝑇) → 𝑎 ∈ {𝑐 ∈ 𝒫 𝑂 ∣ (𝑏 ∩ 𝑐) ∈ 𝐸}) |
| 29 | | ineq2 4214 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑐 = 𝑎 → (𝑏 ∩ 𝑐) = (𝑏 ∩ 𝑎)) |
| 30 | 29 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑐 = 𝑎 → ((𝑏 ∩ 𝑐) ∈ 𝐸 ↔ (𝑏 ∩ 𝑎) ∈ 𝐸)) |
| 31 | 30 | elrab 3692 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ∈ {𝑐 ∈ 𝒫 𝑂 ∣ (𝑏 ∩ 𝑐) ∈ 𝐸} ↔ (𝑎 ∈ 𝒫 𝑂 ∧ (𝑏 ∩ 𝑎) ∈ 𝐸)) |
| 32 | 28, 31 | sylib 218 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐸) ∧ 𝑏 ∈ 𝑇) → (𝑎 ∈ 𝒫 𝑂 ∧ (𝑏 ∩ 𝑎) ∈ 𝐸)) |
| 33 | 32 | simprd 495 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐸) ∧ 𝑏 ∈ 𝑇) → (𝑏 ∩ 𝑎) ∈ 𝐸) |
| 34 | 22, 33 | eqeltrrid 2846 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐸) ∧ 𝑏 ∈ 𝑇) → (𝑎 ∩ 𝑏) ∈ 𝐸) |
| 35 | 21, 34 | jca 511 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐸) ∧ 𝑏 ∈ 𝑇) → (𝑏 ∈ 𝒫 𝑂 ∧ (𝑎 ∩ 𝑏) ∈ 𝐸)) |
| 36 | | ineq2 4214 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = 𝑏 → (𝑎 ∩ 𝑐) = (𝑎 ∩ 𝑏)) |
| 37 | 36 | eleq1d 2826 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = 𝑏 → ((𝑎 ∩ 𝑐) ∈ 𝐸 ↔ (𝑎 ∩ 𝑏) ∈ 𝐸)) |
| 38 | 37 | elrab 3692 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ {𝑐 ∈ 𝒫 𝑂 ∣ (𝑎 ∩ 𝑐) ∈ 𝐸} ↔ (𝑏 ∈ 𝒫 𝑂 ∧ (𝑎 ∩ 𝑏) ∈ 𝐸)) |
| 39 | 35, 38 | sylibr 234 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐸) ∧ 𝑏 ∈ 𝑇) → 𝑏 ∈ {𝑐 ∈ 𝒫 𝑂 ∣ (𝑎 ∩ 𝑐) ∈ 𝐸}) |
| 40 | 39 | ex 412 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐸) → (𝑏 ∈ 𝑇 → 𝑏 ∈ {𝑐 ∈ 𝒫 𝑂 ∣ (𝑎 ∩ 𝑐) ∈ 𝐸})) |
| 41 | 40 | ssrdv 3989 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐸) → 𝑇 ⊆ {𝑐 ∈ 𝒫 𝑂 ∣ (𝑎 ∩ 𝑐) ∈ 𝐸}) |
| 42 | 7, 3, 17, 2, 18, 19, 41 | ldgenpisyslem2 34165 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐸) → 𝐸 ⊆ {𝑐 ∈ 𝒫 𝑂 ∣ (𝑎 ∩ 𝑐) ∈ 𝐸}) |
| 43 | 16, 42 | syldan 591 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸)) → 𝐸 ⊆ {𝑐 ∈ 𝒫 𝑂 ∣ (𝑎 ∩ 𝑐) ∈ 𝐸}) |
| 44 | | ssrab 4073 |
. . . . . . . . 9
⊢ (𝐸 ⊆ {𝑐 ∈ 𝒫 𝑂 ∣ (𝑎 ∩ 𝑐) ∈ 𝐸} ↔ (𝐸 ⊆ 𝒫 𝑂 ∧ ∀𝑐 ∈ 𝐸 (𝑎 ∩ 𝑐) ∈ 𝐸)) |
| 45 | 43, 44 | sylib 218 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸)) → (𝐸 ⊆ 𝒫 𝑂 ∧ ∀𝑐 ∈ 𝐸 (𝑎 ∩ 𝑐) ∈ 𝐸)) |
| 46 | 45 | simprd 495 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸)) → ∀𝑐 ∈ 𝐸 (𝑎 ∩ 𝑐) ∈ 𝐸) |
| 47 | 37 | rspcv 3618 |
. . . . . . 7
⊢ (𝑏 ∈ 𝐸 → (∀𝑐 ∈ 𝐸 (𝑎 ∩ 𝑐) ∈ 𝐸 → (𝑎 ∩ 𝑏) ∈ 𝐸)) |
| 48 | 15, 46, 47 | sylc 65 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸)) → (𝑎 ∩ 𝑏) ∈ 𝐸) |
| 49 | 48 | ralrimivva 3202 |
. . . . 5
⊢ (𝜑 → ∀𝑎 ∈ 𝐸 ∀𝑏 ∈ 𝐸 (𝑎 ∩ 𝑏) ∈ 𝐸) |
| 50 | | inficl 9465 |
. . . . . 6
⊢ (𝐸 ∈ 𝐿 → (∀𝑎 ∈ 𝐸 ∀𝑏 ∈ 𝐸 (𝑎 ∩ 𝑏) ∈ 𝐸 ↔ (fi‘𝐸) = 𝐸)) |
| 51 | 12, 50 | syl 17 |
. . . . 5
⊢ (𝜑 → (∀𝑎 ∈ 𝐸 ∀𝑏 ∈ 𝐸 (𝑎 ∩ 𝑏) ∈ 𝐸 ↔ (fi‘𝐸) = 𝐸)) |
| 52 | 49, 51 | mpbid 232 |
. . . 4
⊢ (𝜑 → (fi‘𝐸) = 𝐸) |
| 53 | | eqimss 4042 |
. . . 4
⊢
((fi‘𝐸) =
𝐸 → (fi‘𝐸) ⊆ 𝐸) |
| 54 | 52, 53 | syl 17 |
. . 3
⊢ (𝜑 → (fi‘𝐸) ⊆ 𝐸) |
| 55 | 14, 54 | jca 511 |
. 2
⊢ (𝜑 → (𝐸 ∈ 𝒫 𝒫 𝑂 ∧ (fi‘𝐸) ⊆ 𝐸)) |
| 56 | 7 | ispisys 34153 |
. 2
⊢ (𝐸 ∈ 𝑃 ↔ (𝐸 ∈ 𝒫 𝒫 𝑂 ∧ (fi‘𝐸) ⊆ 𝐸)) |
| 57 | 55, 56 | sylibr 234 |
1
⊢ (𝜑 → 𝐸 ∈ 𝑃) |