| Step | Hyp | Ref
| Expression |
| 1 | | mrcfval.f |
. 2
⊢ 𝐹 = (mrCls‘𝐶) |
| 2 | | fvssunirn 6939 |
. . . . 5
⊢
(Moore‘𝑋)
⊆ ∪ ran Moore |
| 3 | 2 | sseli 3979 |
. . . 4
⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐶 ∈ ∪ ran
Moore) |
| 4 | | unieq 4918 |
. . . . . . 7
⊢ (𝑐 = 𝐶 → ∪ 𝑐 = ∪
𝐶) |
| 5 | 4 | pweqd 4617 |
. . . . . 6
⊢ (𝑐 = 𝐶 → 𝒫 ∪ 𝑐 =
𝒫 ∪ 𝐶) |
| 6 | | rabeq 3451 |
. . . . . . 7
⊢ (𝑐 = 𝐶 → {𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠} = {𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠}) |
| 7 | 6 | inteqd 4951 |
. . . . . 6
⊢ (𝑐 = 𝐶 → ∩ {𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠} = ∩ {𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠}) |
| 8 | 5, 7 | mpteq12dv 5233 |
. . . . 5
⊢ (𝑐 = 𝐶 → (𝑥 ∈ 𝒫 ∪ 𝑐
↦ ∩ {𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠}) = (𝑥 ∈ 𝒫 ∪ 𝐶
↦ ∩ {𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠})) |
| 9 | | df-mrc 17630 |
. . . . 5
⊢ mrCls =
(𝑐 ∈ ∪ ran Moore ↦ (𝑥 ∈ 𝒫 ∪ 𝑐
↦ ∩ {𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠})) |
| 10 | | mreunirn 17644 |
. . . . . . . 8
⊢ (𝑐 ∈ ∪ ran Moore ↔ 𝑐 ∈ (Moore‘∪ 𝑐)) |
| 11 | | mrcflem 17649 |
. . . . . . . 8
⊢ (𝑐 ∈ (Moore‘∪ 𝑐)
→ (𝑥 ∈ 𝒫
∪ 𝑐 ↦ ∩ {𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠}):𝒫 ∪
𝑐⟶𝑐) |
| 12 | 10, 11 | sylbi 217 |
. . . . . . 7
⊢ (𝑐 ∈ ∪ ran Moore → (𝑥 ∈ 𝒫 ∪ 𝑐
↦ ∩ {𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠}):𝒫 ∪
𝑐⟶𝑐) |
| 13 | | fssxp 6763 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝒫 ∪ 𝑐
↦ ∩ {𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠}):𝒫 ∪
𝑐⟶𝑐 → (𝑥 ∈ 𝒫 ∪ 𝑐
↦ ∩ {𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠}) ⊆ (𝒫 ∪ 𝑐
× 𝑐)) |
| 14 | 12, 13 | syl 17 |
. . . . . 6
⊢ (𝑐 ∈ ∪ ran Moore → (𝑥 ∈ 𝒫 ∪ 𝑐
↦ ∩ {𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠}) ⊆ (𝒫 ∪ 𝑐
× 𝑐)) |
| 15 | | vuniex 7759 |
. . . . . . . 8
⊢ ∪ 𝑐
∈ V |
| 16 | 15 | pwex 5380 |
. . . . . . 7
⊢ 𝒫
∪ 𝑐 ∈ V |
| 17 | | vex 3484 |
. . . . . . 7
⊢ 𝑐 ∈ V |
| 18 | 16, 17 | xpex 7773 |
. . . . . 6
⊢
(𝒫 ∪ 𝑐 × 𝑐) ∈ V |
| 19 | | ssexg 5323 |
. . . . . 6
⊢ (((𝑥 ∈ 𝒫 ∪ 𝑐
↦ ∩ {𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠}) ⊆ (𝒫 ∪ 𝑐
× 𝑐) ∧ (𝒫
∪ 𝑐 × 𝑐) ∈ V) → (𝑥 ∈ 𝒫 ∪ 𝑐
↦ ∩ {𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠}) ∈ V) |
| 20 | 14, 18, 19 | sylancl 586 |
. . . . 5
⊢ (𝑐 ∈ ∪ ran Moore → (𝑥 ∈ 𝒫 ∪ 𝑐
↦ ∩ {𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠}) ∈ V) |
| 21 | 8, 9, 20 | fvmpt3 7020 |
. . . 4
⊢ (𝐶 ∈ ∪ ran Moore → (mrCls‘𝐶) = (𝑥 ∈ 𝒫 ∪ 𝐶
↦ ∩ {𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠})) |
| 22 | 3, 21 | syl 17 |
. . 3
⊢ (𝐶 ∈ (Moore‘𝑋) → (mrCls‘𝐶) = (𝑥 ∈ 𝒫 ∪ 𝐶
↦ ∩ {𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠})) |
| 23 | | mreuni 17643 |
. . . . 5
⊢ (𝐶 ∈ (Moore‘𝑋) → ∪ 𝐶 =
𝑋) |
| 24 | 23 | pweqd 4617 |
. . . 4
⊢ (𝐶 ∈ (Moore‘𝑋) → 𝒫 ∪ 𝐶 =
𝒫 𝑋) |
| 25 | 24 | mpteq1d 5237 |
. . 3
⊢ (𝐶 ∈ (Moore‘𝑋) → (𝑥 ∈ 𝒫 ∪ 𝐶
↦ ∩ {𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠}) = (𝑥 ∈ 𝒫 𝑋 ↦ ∩ {𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠})) |
| 26 | 22, 25 | eqtrd 2777 |
. 2
⊢ (𝐶 ∈ (Moore‘𝑋) → (mrCls‘𝐶) = (𝑥 ∈ 𝒫 𝑋 ↦ ∩ {𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠})) |
| 27 | 1, 26 | eqtrid 2789 |
1
⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐹 = (𝑥 ∈ 𝒫 𝑋 ↦ ∩ {𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠})) |