Step | Hyp | Ref
| Expression |
1 | | fveq2 6191 |
. . 3
⊢ (𝑥 = 𝑋 → (ACS‘𝑥) = (ACS‘𝑋)) |
2 | | pweq 4161 |
. . . 4
⊢ (𝑥 = 𝑋 → 𝒫 𝑥 = 𝒫 𝑋) |
3 | 2 | fveq2d 6195 |
. . 3
⊢ (𝑥 = 𝑋 → (Moore‘𝒫 𝑥) = (Moore‘𝒫 𝑋)) |
4 | 1, 3 | eleq12d 2695 |
. 2
⊢ (𝑥 = 𝑋 → ((ACS‘𝑥) ∈ (Moore‘𝒫 𝑥) ↔ (ACS‘𝑋) ∈ (Moore‘𝒫
𝑋))) |
5 | | acsmre 16313 |
. . . . . . . 8
⊢ (𝑎 ∈ (ACS‘𝑥) → 𝑎 ∈ (Moore‘𝑥)) |
6 | | mresspw 16252 |
. . . . . . . 8
⊢ (𝑎 ∈ (Moore‘𝑥) → 𝑎 ⊆ 𝒫 𝑥) |
7 | 5, 6 | syl 17 |
. . . . . . 7
⊢ (𝑎 ∈ (ACS‘𝑥) → 𝑎 ⊆ 𝒫 𝑥) |
8 | | selpw 4165 |
. . . . . . 7
⊢ (𝑎 ∈ 𝒫 𝒫
𝑥 ↔ 𝑎 ⊆ 𝒫 𝑥) |
9 | 7, 8 | sylibr 224 |
. . . . . 6
⊢ (𝑎 ∈ (ACS‘𝑥) → 𝑎 ∈ 𝒫 𝒫 𝑥) |
10 | 9 | ssriv 3607 |
. . . . 5
⊢
(ACS‘𝑥)
⊆ 𝒫 𝒫 𝑥 |
11 | 10 | a1i 11 |
. . . 4
⊢ (⊤
→ (ACS‘𝑥)
⊆ 𝒫 𝒫 𝑥) |
12 | | vex 3203 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
13 | | mremre 16264 |
. . . . . . . 8
⊢ (𝑥 ∈ V →
(Moore‘𝑥) ∈
(Moore‘𝒫 𝑥)) |
14 | 12, 13 | mp1i 13 |
. . . . . . 7
⊢ (𝑎 ⊆ (ACS‘𝑥) → (Moore‘𝑥) ∈ (Moore‘𝒫
𝑥)) |
15 | 5 | ssriv 3607 |
. . . . . . . 8
⊢
(ACS‘𝑥)
⊆ (Moore‘𝑥) |
16 | | sstr 3611 |
. . . . . . . 8
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ (ACS‘𝑥) ⊆ (Moore‘𝑥)) → 𝑎 ⊆ (Moore‘𝑥)) |
17 | 15, 16 | mpan2 707 |
. . . . . . 7
⊢ (𝑎 ⊆ (ACS‘𝑥) → 𝑎 ⊆ (Moore‘𝑥)) |
18 | | mrerintcl 16257 |
. . . . . . 7
⊢
(((Moore‘𝑥)
∈ (Moore‘𝒫 𝑥) ∧ 𝑎 ⊆ (Moore‘𝑥)) → (𝒫 𝑥 ∩ ∩ 𝑎) ∈ (Moore‘𝑥)) |
19 | 14, 17, 18 | syl2anc 693 |
. . . . . 6
⊢ (𝑎 ⊆ (ACS‘𝑥) → (𝒫 𝑥 ∩ ∩ 𝑎)
∈ (Moore‘𝑥)) |
20 | | ssel2 3598 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑 ∈ 𝑎) → 𝑑 ∈ (ACS‘𝑥)) |
21 | 20 | acsmred 16317 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑 ∈ 𝑎) → 𝑑 ∈ (Moore‘𝑥)) |
22 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢
(mrCls‘𝑑) =
(mrCls‘𝑑) |
23 | 21, 22 | mrcssvd 16283 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑 ∈ 𝑎) → ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥) |
24 | 23 | ralrimiva 2966 |
. . . . . . . . . . . . 13
⊢ (𝑎 ⊆ (ACS‘𝑥) → ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥) |
25 | 24 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑐 ∈ 𝒫 𝑥) → ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥) |
26 | | iunss 4561 |
. . . . . . . . . . . 12
⊢ (∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥 ↔ ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥) |
27 | 25, 26 | sylibr 224 |
. . . . . . . . . . 11
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑐 ∈ 𝒫 𝑥) → ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥) |
28 | 12 | elpw2 4828 |
. . . . . . . . . . 11
⊢ (∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ∈ 𝒫 𝑥 ↔ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥) |
29 | 27, 28 | sylibr 224 |
. . . . . . . . . 10
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑐 ∈ 𝒫 𝑥) → ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ∈ 𝒫 𝑥) |
30 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) = (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) |
31 | 29, 30 | fmptd 6385 |
. . . . . . . . 9
⊢ (𝑎 ⊆ (ACS‘𝑥) → (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥) |
32 | | fssxp 6060 |
. . . . . . . . 9
⊢ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 → (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) ⊆ (𝒫 𝑥 × 𝒫 𝑥)) |
33 | 31, 32 | syl 17 |
. . . . . . . 8
⊢ (𝑎 ⊆ (ACS‘𝑥) → (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) ⊆ (𝒫 𝑥 × 𝒫 𝑥)) |
34 | | vpwex 4849 |
. . . . . . . . 9
⊢ 𝒫
𝑥 ∈ V |
35 | 34, 34 | xpex 6962 |
. . . . . . . 8
⊢
(𝒫 𝑥 ×
𝒫 𝑥) ∈
V |
36 | | ssexg 4804 |
. . . . . . . 8
⊢ (((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) ⊆ (𝒫 𝑥 × 𝒫 𝑥) ∧ (𝒫 𝑥 × 𝒫 𝑥) ∈ V) → (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) ∈ V) |
37 | 33, 35, 36 | sylancl 694 |
. . . . . . 7
⊢ (𝑎 ⊆ (ACS‘𝑥) → (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) ∈ V) |
38 | 20 | adantlr 751 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑑 ∈ 𝑎) → 𝑑 ∈ (ACS‘𝑥)) |
39 | | elpwi 4168 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ 𝒫 𝑥 → 𝑏 ⊆ 𝑥) |
40 | 39 | ad2antlr 763 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑑 ∈ 𝑎) → 𝑏 ⊆ 𝑥) |
41 | 22 | acsfiel2 16316 |
. . . . . . . . . . . . 13
⊢ ((𝑑 ∈ (ACS‘𝑥) ∧ 𝑏 ⊆ 𝑥) → (𝑏 ∈ 𝑑 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)) |
42 | 38, 40, 41 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑑 ∈ 𝑎) → (𝑏 ∈ 𝑑 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)) |
43 | 42 | ralbidva 2985 |
. . . . . . . . . . 11
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∀𝑑 ∈ 𝑎 𝑏 ∈ 𝑑 ↔ ∀𝑑 ∈ 𝑎 ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)) |
44 | | iunss 4561 |
. . . . . . . . . . . . 13
⊢ (∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏) |
45 | 44 | ralbii 2980 |
. . . . . . . . . . . 12
⊢
(∀𝑒 ∈
(𝒫 𝑏 ∩
Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏) |
46 | | ralcom 3098 |
. . . . . . . . . . . 12
⊢
(∀𝑒 ∈
(𝒫 𝑏 ∩
Fin)∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑑 ∈ 𝑎 ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏) |
47 | 45, 46 | bitri 264 |
. . . . . . . . . . 11
⊢
(∀𝑒 ∈
(𝒫 𝑏 ∩
Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑑 ∈ 𝑎 ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏) |
48 | 43, 47 | syl6bbr 278 |
. . . . . . . . . 10
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∀𝑑 ∈ 𝑎 𝑏 ∈ 𝑑 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)) |
49 | | elrint2 4519 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ 𝒫 𝑥 → (𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∀𝑑 ∈ 𝑎 𝑏 ∈ 𝑑)) |
50 | 49 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∀𝑑 ∈ 𝑎 𝑏 ∈ 𝑑)) |
51 | | funmpt 5926 |
. . . . . . . . . . . . 13
⊢ Fun
(𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) |
52 | | funiunfv 6506 |
. . . . . . . . . . . . 13
⊢ (Fun
(𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → ∪
𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin))) |
53 | 51, 52 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ∪ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) |
54 | 53 | sseq1i 3629 |
. . . . . . . . . . 11
⊢ (∪ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏) |
55 | | iunss 4561 |
. . . . . . . . . . . 12
⊢ (∪ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏) |
56 | | inss1 3833 |
. . . . . . . . . . . . . . . . 17
⊢
(𝒫 𝑏 ∩
Fin) ⊆ 𝒫 𝑏 |
57 | | sspwb 4917 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 ⊆ 𝑥 ↔ 𝒫 𝑏 ⊆ 𝒫 𝑥) |
58 | 39, 57 | sylib 208 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 ∈ 𝒫 𝑥 → 𝒫 𝑏 ⊆ 𝒫 𝑥) |
59 | 58 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → 𝒫 𝑏 ⊆ 𝒫 𝑥) |
60 | 56, 59 | syl5ss 3614 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (𝒫 𝑏 ∩ Fin) ⊆ 𝒫 𝑥) |
61 | 60 | sselda 3603 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → 𝑒 ∈ 𝒫 𝑥) |
62 | 21, 22 | mrcssvd 16283 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑 ∈ 𝑎) → ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥) |
63 | 62 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ⊆ (ACS‘𝑥) → ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥) |
64 | 63 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥) |
65 | | iunss 4561 |
. . . . . . . . . . . . . . . . 17
⊢ (∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥 ↔ ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥) |
66 | 64, 65 | sylibr 224 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥) |
67 | | ssexg 4804 |
. . . . . . . . . . . . . . . 16
⊢
((∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥 ∧ 𝑥 ∈ V) → ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ∈ V) |
68 | 66, 12, 67 | sylancl 694 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ∈ V) |
69 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 = 𝑒 → ((mrCls‘𝑑)‘𝑐) = ((mrCls‘𝑑)‘𝑒)) |
70 | 69 | iuneq2d 4547 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = 𝑒 → ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) = ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒)) |
71 | 70, 30 | fvmptg 6280 |
. . . . . . . . . . . . . . 15
⊢ ((𝑒 ∈ 𝒫 𝑥 ∧ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ∈ V) → ((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒)) |
72 | 61, 68, 71 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → ((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒)) |
73 | 72 | sseq1d 3632 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → (((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)) |
74 | 73 | ralbidva 2985 |
. . . . . . . . . . . 12
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)) |
75 | 55, 74 | syl5bb 272 |
. . . . . . . . . . 11
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∪
𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)) |
76 | 54, 75 | syl5bbr 274 |
. . . . . . . . . 10
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∪
((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)) |
77 | 48, 50, 76 | 3bitr4d 300 |
. . . . . . . . 9
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ ((𝑐
∈ 𝒫 𝑥 ↦
∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)) |
78 | 77 | ralrimiva 2966 |
. . . . . . . 8
⊢ (𝑎 ⊆ (ACS‘𝑥) → ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ ((𝑐
∈ 𝒫 𝑥 ↦
∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)) |
79 | 31, 78 | jca 554 |
. . . . . . 7
⊢ (𝑎 ⊆ (ACS‘𝑥) → ((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ ((𝑐
∈ 𝒫 𝑥 ↦
∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))) |
80 | | feq1 6026 |
. . . . . . . . 9
⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → (𝑓:𝒫 𝑥⟶𝒫 𝑥 ↔ (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥)) |
81 | | imaeq1 5461 |
. . . . . . . . . . . . 13
⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → (𝑓 “ (𝒫 𝑏 ∩ Fin)) = ((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin))) |
82 | 81 | unieqd 4446 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → ∪ (𝑓 “ (𝒫 𝑏 ∩ Fin)) = ∪ ((𝑐
∈ 𝒫 𝑥 ↦
∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin))) |
83 | 82 | sseq1d 3632 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → (∪
(𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏 ↔ ∪ ((𝑐
∈ 𝒫 𝑥 ↦
∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)) |
84 | 83 | bibi2d 332 |
. . . . . . . . . 10
⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → ((𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ (𝑓
“ (𝒫 𝑏 ∩
Fin)) ⊆ 𝑏) ↔
(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎)
↔ ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))) |
85 | 84 | ralbidv 2986 |
. . . . . . . . 9
⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → (∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ (𝑓
“ (𝒫 𝑏 ∩
Fin)) ⊆ 𝑏) ↔
∀𝑏 ∈ 𝒫
𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ ((𝑐
∈ 𝒫 𝑥 ↦
∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))) |
86 | 80, 85 | anbi12d 747 |
. . . . . . . 8
⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → ((𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ (𝑓
“ (𝒫 𝑏 ∩
Fin)) ⊆ 𝑏)) ↔
((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ ((𝑐
∈ 𝒫 𝑥 ↦
∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)))) |
87 | 86 | spcegv 3294 |
. . . . . . 7
⊢ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) ∈ V → (((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ ((𝑐
∈ 𝒫 𝑥 ↦
∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)) → ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ (𝑓
“ (𝒫 𝑏 ∩
Fin)) ⊆ 𝑏)))) |
88 | 37, 79, 87 | sylc 65 |
. . . . . 6
⊢ (𝑎 ⊆ (ACS‘𝑥) → ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ (𝑓
“ (𝒫 𝑏 ∩
Fin)) ⊆ 𝑏))) |
89 | | isacs 16312 |
. . . . . 6
⊢
((𝒫 𝑥 ∩
∩ 𝑎) ∈ (ACS‘𝑥) ↔ ((𝒫 𝑥 ∩ ∩ 𝑎) ∈ (Moore‘𝑥) ∧ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ (𝑓
“ (𝒫 𝑏 ∩
Fin)) ⊆ 𝑏)))) |
90 | 19, 88, 89 | sylanbrc 698 |
. . . . 5
⊢ (𝑎 ⊆ (ACS‘𝑥) → (𝒫 𝑥 ∩ ∩ 𝑎)
∈ (ACS‘𝑥)) |
91 | 90 | adantl 482 |
. . . 4
⊢
((⊤ ∧ 𝑎
⊆ (ACS‘𝑥))
→ (𝒫 𝑥 ∩
∩ 𝑎) ∈ (ACS‘𝑥)) |
92 | 11, 91 | ismred2 16263 |
. . 3
⊢ (⊤
→ (ACS‘𝑥) ∈
(Moore‘𝒫 𝑥)) |
93 | 92 | trud 1493 |
. 2
⊢
(ACS‘𝑥) ∈
(Moore‘𝒫 𝑥) |
94 | 4, 93 | vtoclg 3266 |
1
⊢ (𝑋 ∈ 𝑉 → (ACS‘𝑋) ∈ (Moore‘𝒫 𝑋)) |