Step | Hyp | Ref
| Expression |
1 | | fveq2 6674 |
. . 3
⊢ (𝑥 = 𝑋 → (ACS‘𝑥) = (ACS‘𝑋)) |
2 | | pweq 4504 |
. . . 4
⊢ (𝑥 = 𝑋 → 𝒫 𝑥 = 𝒫 𝑋) |
3 | 2 | fveq2d 6678 |
. . 3
⊢ (𝑥 = 𝑋 → (Moore‘𝒫 𝑥) = (Moore‘𝒫 𝑋)) |
4 | 1, 3 | eleq12d 2827 |
. 2
⊢ (𝑥 = 𝑋 → ((ACS‘𝑥) ∈ (Moore‘𝒫 𝑥) ↔ (ACS‘𝑋) ∈ (Moore‘𝒫
𝑋))) |
5 | | acsmre 17026 |
. . . . . . 7
⊢ (𝑎 ∈ (ACS‘𝑥) → 𝑎 ∈ (Moore‘𝑥)) |
6 | | mresspw 16966 |
. . . . . . . 8
⊢ (𝑎 ∈ (Moore‘𝑥) → 𝑎 ⊆ 𝒫 𝑥) |
7 | 5, 6 | syl 17 |
. . . . . . 7
⊢ (𝑎 ∈ (ACS‘𝑥) → 𝑎 ⊆ 𝒫 𝑥) |
8 | 5, 7 | elpwd 4496 |
. . . . . 6
⊢ (𝑎 ∈ (ACS‘𝑥) → 𝑎 ∈ 𝒫 𝒫 𝑥) |
9 | 8 | ssriv 3881 |
. . . . 5
⊢
(ACS‘𝑥)
⊆ 𝒫 𝒫 𝑥 |
10 | 9 | a1i 11 |
. . . 4
⊢ (⊤
→ (ACS‘𝑥)
⊆ 𝒫 𝒫 𝑥) |
11 | | vex 3402 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
12 | | mremre 16978 |
. . . . . . . 8
⊢ (𝑥 ∈ V →
(Moore‘𝑥) ∈
(Moore‘𝒫 𝑥)) |
13 | 11, 12 | mp1i 13 |
. . . . . . 7
⊢ (𝑎 ⊆ (ACS‘𝑥) → (Moore‘𝑥) ∈ (Moore‘𝒫
𝑥)) |
14 | 5 | ssriv 3881 |
. . . . . . . 8
⊢
(ACS‘𝑥)
⊆ (Moore‘𝑥) |
15 | | sstr 3885 |
. . . . . . . 8
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ (ACS‘𝑥) ⊆ (Moore‘𝑥)) → 𝑎 ⊆ (Moore‘𝑥)) |
16 | 14, 15 | mpan2 691 |
. . . . . . 7
⊢ (𝑎 ⊆ (ACS‘𝑥) → 𝑎 ⊆ (Moore‘𝑥)) |
17 | | mrerintcl 16971 |
. . . . . . 7
⊢
(((Moore‘𝑥)
∈ (Moore‘𝒫 𝑥) ∧ 𝑎 ⊆ (Moore‘𝑥)) → (𝒫 𝑥 ∩ ∩ 𝑎) ∈ (Moore‘𝑥)) |
18 | 13, 16, 17 | syl2anc 587 |
. . . . . 6
⊢ (𝑎 ⊆ (ACS‘𝑥) → (𝒫 𝑥 ∩ ∩ 𝑎)
∈ (Moore‘𝑥)) |
19 | | ssel2 3872 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑 ∈ 𝑎) → 𝑑 ∈ (ACS‘𝑥)) |
20 | 19 | acsmred 17030 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑 ∈ 𝑎) → 𝑑 ∈ (Moore‘𝑥)) |
21 | | eqid 2738 |
. . . . . . . . . . . . . . 15
⊢
(mrCls‘𝑑) =
(mrCls‘𝑑) |
22 | 20, 21 | mrcssvd 16997 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑 ∈ 𝑎) → ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥) |
23 | 22 | ralrimiva 3096 |
. . . . . . . . . . . . 13
⊢ (𝑎 ⊆ (ACS‘𝑥) → ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥) |
24 | 23 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑐 ∈ 𝒫 𝑥) → ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥) |
25 | | iunss 4931 |
. . . . . . . . . . . 12
⊢ (∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥 ↔ ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥) |
26 | 24, 25 | sylibr 237 |
. . . . . . . . . . 11
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑐 ∈ 𝒫 𝑥) → ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥) |
27 | 11 | elpw2 5213 |
. . . . . . . . . . 11
⊢ (∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ∈ 𝒫 𝑥 ↔ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥) |
28 | 26, 27 | sylibr 237 |
. . . . . . . . . 10
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑐 ∈ 𝒫 𝑥) → ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ∈ 𝒫 𝑥) |
29 | 28 | fmpttd 6889 |
. . . . . . . . 9
⊢ (𝑎 ⊆ (ACS‘𝑥) → (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥) |
30 | | fssxp 6532 |
. . . . . . . . 9
⊢ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 → (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) ⊆ (𝒫 𝑥 × 𝒫 𝑥)) |
31 | 29, 30 | syl 17 |
. . . . . . . 8
⊢ (𝑎 ⊆ (ACS‘𝑥) → (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) ⊆ (𝒫 𝑥 × 𝒫 𝑥)) |
32 | | vpwex 5244 |
. . . . . . . . 9
⊢ 𝒫
𝑥 ∈ V |
33 | 32, 32 | xpex 7494 |
. . . . . . . 8
⊢
(𝒫 𝑥 ×
𝒫 𝑥) ∈
V |
34 | | ssexg 5191 |
. . . . . . . 8
⊢ (((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) ⊆ (𝒫 𝑥 × 𝒫 𝑥) ∧ (𝒫 𝑥 × 𝒫 𝑥) ∈ V) → (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) ∈ V) |
35 | 31, 33, 34 | sylancl 589 |
. . . . . . 7
⊢ (𝑎 ⊆ (ACS‘𝑥) → (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) ∈ V) |
36 | 19 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑑 ∈ 𝑎) → 𝑑 ∈ (ACS‘𝑥)) |
37 | | elpwi 4497 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ 𝒫 𝑥 → 𝑏 ⊆ 𝑥) |
38 | 37 | ad2antlr 727 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑑 ∈ 𝑎) → 𝑏 ⊆ 𝑥) |
39 | 21 | acsfiel2 17029 |
. . . . . . . . . . . . 13
⊢ ((𝑑 ∈ (ACS‘𝑥) ∧ 𝑏 ⊆ 𝑥) → (𝑏 ∈ 𝑑 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)) |
40 | 36, 38, 39 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑑 ∈ 𝑎) → (𝑏 ∈ 𝑑 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)) |
41 | 40 | ralbidva 3108 |
. . . . . . . . . . 11
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∀𝑑 ∈ 𝑎 𝑏 ∈ 𝑑 ↔ ∀𝑑 ∈ 𝑎 ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)) |
42 | | iunss 4931 |
. . . . . . . . . . . . 13
⊢ (∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏) |
43 | 42 | ralbii 3080 |
. . . . . . . . . . . 12
⊢
(∀𝑒 ∈
(𝒫 𝑏 ∩
Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏) |
44 | | ralcom 3258 |
. . . . . . . . . . . 12
⊢
(∀𝑒 ∈
(𝒫 𝑏 ∩
Fin)∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑑 ∈ 𝑎 ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏) |
45 | 43, 44 | bitri 278 |
. . . . . . . . . . 11
⊢
(∀𝑒 ∈
(𝒫 𝑏 ∩
Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑑 ∈ 𝑎 ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏) |
46 | 41, 45 | bitr4di 292 |
. . . . . . . . . 10
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∀𝑑 ∈ 𝑎 𝑏 ∈ 𝑑 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)) |
47 | | elrint2 4880 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ 𝒫 𝑥 → (𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∀𝑑 ∈ 𝑎 𝑏 ∈ 𝑑)) |
48 | 47 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∀𝑑 ∈ 𝑎 𝑏 ∈ 𝑑)) |
49 | | funmpt 6377 |
. . . . . . . . . . . . 13
⊢ Fun
(𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) |
50 | | funiunfv 7018 |
. . . . . . . . . . . . 13
⊢ (Fun
(𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → ∪
𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin))) |
51 | 49, 50 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ∪ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) |
52 | 51 | sseq1i 3905 |
. . . . . . . . . . 11
⊢ (∪ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏) |
53 | | iunss 4931 |
. . . . . . . . . . . 12
⊢ (∪ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏) |
54 | | eqid 2738 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) = (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) |
55 | | fveq2 6674 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = 𝑒 → ((mrCls‘𝑑)‘𝑐) = ((mrCls‘𝑑)‘𝑒)) |
56 | 55 | iuneq2d 4910 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = 𝑒 → ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) = ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒)) |
57 | | inss1 4119 |
. . . . . . . . . . . . . . . . 17
⊢
(𝒫 𝑏 ∩
Fin) ⊆ 𝒫 𝑏 |
58 | 37 | sspwd 4503 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 ∈ 𝒫 𝑥 → 𝒫 𝑏 ⊆ 𝒫 𝑥) |
59 | 58 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → 𝒫 𝑏 ⊆ 𝒫 𝑥) |
60 | 57, 59 | sstrid 3888 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (𝒫 𝑏 ∩ Fin) ⊆ 𝒫 𝑥) |
61 | 60 | sselda 3877 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → 𝑒 ∈ 𝒫 𝑥) |
62 | 20, 21 | mrcssvd 16997 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑 ∈ 𝑎) → ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥) |
63 | 62 | ralrimiva 3096 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ⊆ (ACS‘𝑥) → ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥) |
64 | 63 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥) |
65 | | iunss 4931 |
. . . . . . . . . . . . . . . . 17
⊢ (∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥 ↔ ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥) |
66 | 64, 65 | sylibr 237 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥) |
67 | | ssexg 5191 |
. . . . . . . . . . . . . . . 16
⊢
((∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥 ∧ 𝑥 ∈ V) → ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ∈ V) |
68 | 66, 11, 67 | sylancl 589 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ∈ V) |
69 | 54, 56, 61, 68 | fvmptd3 6798 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → ((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒)) |
70 | 69 | sseq1d 3908 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → (((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)) |
71 | 70 | ralbidva 3108 |
. . . . . . . . . . . 12
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)) |
72 | 53, 71 | syl5bb 286 |
. . . . . . . . . . 11
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∪
𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)) |
73 | 52, 72 | bitr3id 288 |
. . . . . . . . . 10
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∪
((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)) |
74 | 46, 48, 73 | 3bitr4d 314 |
. . . . . . . . 9
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ ((𝑐
∈ 𝒫 𝑥 ↦
∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)) |
75 | 74 | ralrimiva 3096 |
. . . . . . . 8
⊢ (𝑎 ⊆ (ACS‘𝑥) → ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ ((𝑐
∈ 𝒫 𝑥 ↦
∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)) |
76 | 29, 75 | jca 515 |
. . . . . . 7
⊢ (𝑎 ⊆ (ACS‘𝑥) → ((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ ((𝑐
∈ 𝒫 𝑥 ↦
∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))) |
77 | | feq1 6485 |
. . . . . . . 8
⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → (𝑓:𝒫 𝑥⟶𝒫 𝑥 ↔ (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥)) |
78 | | imaeq1 5898 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → (𝑓 “ (𝒫 𝑏 ∩ Fin)) = ((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin))) |
79 | 78 | unieqd 4810 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → ∪ (𝑓 “ (𝒫 𝑏 ∩ Fin)) = ∪ ((𝑐
∈ 𝒫 𝑥 ↦
∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin))) |
80 | 79 | sseq1d 3908 |
. . . . . . . . . 10
⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → (∪
(𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏 ↔ ∪ ((𝑐
∈ 𝒫 𝑥 ↦
∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)) |
81 | 80 | bibi2d 346 |
. . . . . . . . 9
⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → ((𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ (𝑓
“ (𝒫 𝑏 ∩
Fin)) ⊆ 𝑏) ↔
(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎)
↔ ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))) |
82 | 81 | ralbidv 3109 |
. . . . . . . 8
⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → (∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ (𝑓
“ (𝒫 𝑏 ∩
Fin)) ⊆ 𝑏) ↔
∀𝑏 ∈ 𝒫
𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ ((𝑐
∈ 𝒫 𝑥 ↦
∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))) |
83 | 77, 82 | anbi12d 634 |
. . . . . . 7
⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → ((𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ (𝑓
“ (𝒫 𝑏 ∩
Fin)) ⊆ 𝑏)) ↔
((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ ((𝑐
∈ 𝒫 𝑥 ↦
∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)))) |
84 | 35, 76, 83 | spcedv 3502 |
. . . . . 6
⊢ (𝑎 ⊆ (ACS‘𝑥) → ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ (𝑓
“ (𝒫 𝑏 ∩
Fin)) ⊆ 𝑏))) |
85 | | isacs 17025 |
. . . . . 6
⊢
((𝒫 𝑥 ∩
∩ 𝑎) ∈ (ACS‘𝑥) ↔ ((𝒫 𝑥 ∩ ∩ 𝑎) ∈ (Moore‘𝑥) ∧ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ (𝑓
“ (𝒫 𝑏 ∩
Fin)) ⊆ 𝑏)))) |
86 | 18, 84, 85 | sylanbrc 586 |
. . . . 5
⊢ (𝑎 ⊆ (ACS‘𝑥) → (𝒫 𝑥 ∩ ∩ 𝑎)
∈ (ACS‘𝑥)) |
87 | 86 | adantl 485 |
. . . 4
⊢
((⊤ ∧ 𝑎
⊆ (ACS‘𝑥))
→ (𝒫 𝑥 ∩
∩ 𝑎) ∈ (ACS‘𝑥)) |
88 | 10, 87 | ismred2 16977 |
. . 3
⊢ (⊤
→ (ACS‘𝑥) ∈
(Moore‘𝒫 𝑥)) |
89 | 88 | mptru 1549 |
. 2
⊢
(ACS‘𝑥) ∈
(Moore‘𝒫 𝑥) |
90 | 4, 89 | vtoclg 3470 |
1
⊢ (𝑋 ∈ 𝑉 → (ACS‘𝑋) ∈ (Moore‘𝒫 𝑋)) |