Step | Hyp | Ref
| Expression |
1 | | mrisval.2 |
. . 3
⊢ 𝐼 = (mrInd‘𝐴) |
2 | | fvssunirn 6693 |
. . . . 5
⊢
(Moore‘𝑋)
⊆ ∪ ran Moore |
3 | 2 | sseli 3962 |
. . . 4
⊢ (𝐴 ∈ (Moore‘𝑋) → 𝐴 ∈ ∪ ran
Moore) |
4 | | unieq 4839 |
. . . . . . 7
⊢ (𝑐 = 𝐴 → ∪ 𝑐 = ∪
𝐴) |
5 | 4 | pweqd 4543 |
. . . . . 6
⊢ (𝑐 = 𝐴 → 𝒫 ∪ 𝑐 =
𝒫 ∪ 𝐴) |
6 | | fveq2 6664 |
. . . . . . . . . . 11
⊢ (𝑐 = 𝐴 → (mrCls‘𝑐) = (mrCls‘𝐴)) |
7 | | mrisval.1 |
. . . . . . . . . . 11
⊢ 𝑁 = (mrCls‘𝐴) |
8 | 6, 7 | syl6eqr 2874 |
. . . . . . . . . 10
⊢ (𝑐 = 𝐴 → (mrCls‘𝑐) = 𝑁) |
9 | 8 | fveq1d 6666 |
. . . . . . . . 9
⊢ (𝑐 = 𝐴 → ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥})) = (𝑁‘(𝑠 ∖ {𝑥}))) |
10 | 9 | eleq2d 2898 |
. . . . . . . 8
⊢ (𝑐 = 𝐴 → (𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥})) ↔ 𝑥 ∈ (𝑁‘(𝑠 ∖ {𝑥})))) |
11 | 10 | notbid 320 |
. . . . . . 7
⊢ (𝑐 = 𝐴 → (¬ 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥})) ↔ ¬ 𝑥 ∈ (𝑁‘(𝑠 ∖ {𝑥})))) |
12 | 11 | ralbidv 3197 |
. . . . . 6
⊢ (𝑐 = 𝐴 → (∀𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥})) ↔ ∀𝑥 ∈ 𝑠 ¬ 𝑥 ∈ (𝑁‘(𝑠 ∖ {𝑥})))) |
13 | 5, 12 | rabeqbidv 3485 |
. . . . 5
⊢ (𝑐 = 𝐴 → {𝑠 ∈ 𝒫 ∪ 𝑐
∣ ∀𝑥 ∈
𝑠 ¬ 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))} = {𝑠 ∈ 𝒫 ∪ 𝐴
∣ ∀𝑥 ∈
𝑠 ¬ 𝑥 ∈ (𝑁‘(𝑠 ∖ {𝑥}))}) |
14 | | df-mri 16853 |
. . . . 5
⊢ mrInd =
(𝑐 ∈ ∪ ran Moore ↦ {𝑠 ∈ 𝒫 ∪ 𝑐
∣ ∀𝑥 ∈
𝑠 ¬ 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))}) |
15 | | vuniex 7459 |
. . . . . . 7
⊢ ∪ 𝑐
∈ V |
16 | 15 | pwex 5273 |
. . . . . 6
⊢ 𝒫
∪ 𝑐 ∈ V |
17 | 16 | rabex 5227 |
. . . . 5
⊢ {𝑠 ∈ 𝒫 ∪ 𝑐
∣ ∀𝑥 ∈
𝑠 ¬ 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))} ∈ V |
18 | 13, 14, 17 | fvmpt3i 6767 |
. . . 4
⊢ (𝐴 ∈ ∪ ran Moore → (mrInd‘𝐴) = {𝑠 ∈ 𝒫 ∪ 𝐴
∣ ∀𝑥 ∈
𝑠 ¬ 𝑥 ∈ (𝑁‘(𝑠 ∖ {𝑥}))}) |
19 | 3, 18 | syl 17 |
. . 3
⊢ (𝐴 ∈ (Moore‘𝑋) → (mrInd‘𝐴) = {𝑠 ∈ 𝒫 ∪ 𝐴
∣ ∀𝑥 ∈
𝑠 ¬ 𝑥 ∈ (𝑁‘(𝑠 ∖ {𝑥}))}) |
20 | 1, 19 | syl5eq 2868 |
. 2
⊢ (𝐴 ∈ (Moore‘𝑋) → 𝐼 = {𝑠 ∈ 𝒫 ∪ 𝐴
∣ ∀𝑥 ∈
𝑠 ¬ 𝑥 ∈ (𝑁‘(𝑠 ∖ {𝑥}))}) |
21 | | mreuni 16865 |
. . . 4
⊢ (𝐴 ∈ (Moore‘𝑋) → ∪ 𝐴 =
𝑋) |
22 | 21 | pweqd 4543 |
. . 3
⊢ (𝐴 ∈ (Moore‘𝑋) → 𝒫 ∪ 𝐴 =
𝒫 𝑋) |
23 | 22 | rabeqdv 3484 |
. 2
⊢ (𝐴 ∈ (Moore‘𝑋) → {𝑠 ∈ 𝒫 ∪ 𝐴
∣ ∀𝑥 ∈
𝑠 ¬ 𝑥 ∈ (𝑁‘(𝑠 ∖ {𝑥}))} = {𝑠 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑠 ¬ 𝑥 ∈ (𝑁‘(𝑠 ∖ {𝑥}))}) |
24 | 20, 23 | eqtrd 2856 |
1
⊢ (𝐴 ∈ (Moore‘𝑋) → 𝐼 = {𝑠 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑠 ¬ 𝑥 ∈ (𝑁‘(𝑠 ∖ {𝑥}))}) |