Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . 3
⊢ (𝑥 = 𝑋 → (ACS‘𝑥) = (ACS‘𝑋)) |
2 | | pweq 4111 |
. . . 4
⊢ (𝑥 = 𝑋 → 𝒫 𝑥 = 𝒫 𝑋) |
3 | 2 | fveq2d 6107 |
. . 3
⊢ (𝑥 = 𝑋 → (Moore‘𝒫 𝑥) = (Moore‘𝒫 𝑋)) |
4 | 1, 3 | eleq12d 2682 |
. 2
⊢ (𝑥 = 𝑋 → ((ACS‘𝑥) ∈ (Moore‘𝒫 𝑥) ↔ (ACS‘𝑋) ∈ (Moore‘𝒫
𝑋))) |
5 | | acsmre 16136 |
. . . . . . . 8
⊢ (𝑎 ∈ (ACS‘𝑥) → 𝑎 ∈ (Moore‘𝑥)) |
6 | | mresspw 16075 |
. . . . . . . 8
⊢ (𝑎 ∈ (Moore‘𝑥) → 𝑎 ⊆ 𝒫 𝑥) |
7 | 5, 6 | syl 17 |
. . . . . . 7
⊢ (𝑎 ∈ (ACS‘𝑥) → 𝑎 ⊆ 𝒫 𝑥) |
8 | | selpw 4115 |
. . . . . . 7
⊢ (𝑎 ∈ 𝒫 𝒫
𝑥 ↔ 𝑎 ⊆ 𝒫 𝑥) |
9 | 7, 8 | sylibr 223 |
. . . . . 6
⊢ (𝑎 ∈ (ACS‘𝑥) → 𝑎 ∈ 𝒫 𝒫 𝑥) |
10 | 9 | ssriv 3572 |
. . . . 5
⊢
(ACS‘𝑥)
⊆ 𝒫 𝒫 𝑥 |
11 | 10 | a1i 11 |
. . . 4
⊢ (⊤
→ (ACS‘𝑥)
⊆ 𝒫 𝒫 𝑥) |
12 | | vex 3176 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
13 | | mremre 16087 |
. . . . . . . 8
⊢ (𝑥 ∈ V →
(Moore‘𝑥) ∈
(Moore‘𝒫 𝑥)) |
14 | 12, 13 | mp1i 13 |
. . . . . . 7
⊢ (𝑎 ⊆ (ACS‘𝑥) → (Moore‘𝑥) ∈ (Moore‘𝒫
𝑥)) |
15 | 5 | ssriv 3572 |
. . . . . . . 8
⊢
(ACS‘𝑥)
⊆ (Moore‘𝑥) |
16 | | sstr 3576 |
. . . . . . . 8
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ (ACS‘𝑥) ⊆ (Moore‘𝑥)) → 𝑎 ⊆ (Moore‘𝑥)) |
17 | 15, 16 | mpan2 703 |
. . . . . . 7
⊢ (𝑎 ⊆ (ACS‘𝑥) → 𝑎 ⊆ (Moore‘𝑥)) |
18 | | mrerintcl 16080 |
. . . . . . 7
⊢
(((Moore‘𝑥)
∈ (Moore‘𝒫 𝑥) ∧ 𝑎 ⊆ (Moore‘𝑥)) → (𝒫 𝑥 ∩ ∩ 𝑎) ∈ (Moore‘𝑥)) |
19 | 14, 17, 18 | syl2anc 691 |
. . . . . 6
⊢ (𝑎 ⊆ (ACS‘𝑥) → (𝒫 𝑥 ∩ ∩ 𝑎)
∈ (Moore‘𝑥)) |
20 | | ssel2 3563 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑 ∈ 𝑎) → 𝑑 ∈ (ACS‘𝑥)) |
21 | 20 | acsmred 16140 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑 ∈ 𝑎) → 𝑑 ∈ (Moore‘𝑥)) |
22 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(mrCls‘𝑑) =
(mrCls‘𝑑) |
23 | 21, 22 | mrcssvd 16106 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑 ∈ 𝑎) → ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥) |
24 | 23 | ralrimiva 2949 |
. . . . . . . . . . . . 13
⊢ (𝑎 ⊆ (ACS‘𝑥) → ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥) |
25 | 24 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑐 ∈ 𝒫 𝑥) → ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥) |
26 | | iunss 4497 |
. . . . . . . . . . . 12
⊢ (∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥 ↔ ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥) |
27 | 25, 26 | sylibr 223 |
. . . . . . . . . . 11
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑐 ∈ 𝒫 𝑥) → ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥) |
28 | 12 | elpw2 4755 |
. . . . . . . . . . 11
⊢ (∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ∈ 𝒫 𝑥 ↔ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥) |
29 | 27, 28 | sylibr 223 |
. . . . . . . . . 10
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑐 ∈ 𝒫 𝑥) → ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ∈ 𝒫 𝑥) |
30 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) = (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) |
31 | 29, 30 | fmptd 6292 |
. . . . . . . . 9
⊢ (𝑎 ⊆ (ACS‘𝑥) → (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥) |
32 | | fssxp 5973 |
. . . . . . . . 9
⊢ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 → (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) ⊆ (𝒫 𝑥 × 𝒫 𝑥)) |
33 | 31, 32 | syl 17 |
. . . . . . . 8
⊢ (𝑎 ⊆ (ACS‘𝑥) → (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) ⊆ (𝒫 𝑥 × 𝒫 𝑥)) |
34 | | vpwex 4775 |
. . . . . . . . 9
⊢ 𝒫
𝑥 ∈ V |
35 | 34, 34 | xpex 6860 |
. . . . . . . 8
⊢
(𝒫 𝑥 ×
𝒫 𝑥) ∈
V |
36 | | ssexg 4732 |
. . . . . . . 8
⊢ (((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) ⊆ (𝒫 𝑥 × 𝒫 𝑥) ∧ (𝒫 𝑥 × 𝒫 𝑥) ∈ V) → (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) ∈ V) |
37 | 33, 35, 36 | sylancl 693 |
. . . . . . 7
⊢ (𝑎 ⊆ (ACS‘𝑥) → (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) ∈ V) |
38 | 20 | adantlr 747 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑑 ∈ 𝑎) → 𝑑 ∈ (ACS‘𝑥)) |
39 | | elpwi 4117 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ 𝒫 𝑥 → 𝑏 ⊆ 𝑥) |
40 | 39 | ad2antlr 759 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑑 ∈ 𝑎) → 𝑏 ⊆ 𝑥) |
41 | 22 | acsfiel2 16139 |
. . . . . . . . . . . . 13
⊢ ((𝑑 ∈ (ACS‘𝑥) ∧ 𝑏 ⊆ 𝑥) → (𝑏 ∈ 𝑑 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)) |
42 | 38, 40, 41 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑑 ∈ 𝑎) → (𝑏 ∈ 𝑑 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)) |
43 | 42 | ralbidva 2968 |
. . . . . . . . . . 11
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∀𝑑 ∈ 𝑎 𝑏 ∈ 𝑑 ↔ ∀𝑑 ∈ 𝑎 ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)) |
44 | | iunss 4497 |
. . . . . . . . . . . . 13
⊢ (∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏) |
45 | 44 | ralbii 2963 |
. . . . . . . . . . . 12
⊢
(∀𝑒 ∈
(𝒫 𝑏 ∩
Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏) |
46 | | ralcom 3079 |
. . . . . . . . . . . 12
⊢
(∀𝑒 ∈
(𝒫 𝑏 ∩
Fin)∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑑 ∈ 𝑎 ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏) |
47 | 45, 46 | bitri 263 |
. . . . . . . . . . 11
⊢
(∀𝑒 ∈
(𝒫 𝑏 ∩
Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑑 ∈ 𝑎 ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏) |
48 | 43, 47 | syl6bbr 277 |
. . . . . . . . . 10
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∀𝑑 ∈ 𝑎 𝑏 ∈ 𝑑 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)) |
49 | | elrint2 4454 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ 𝒫 𝑥 → (𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∀𝑑 ∈ 𝑎 𝑏 ∈ 𝑑)) |
50 | 49 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∀𝑑 ∈ 𝑎 𝑏 ∈ 𝑑)) |
51 | | funmpt 5840 |
. . . . . . . . . . . . 13
⊢ Fun
(𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) |
52 | | funiunfv 6410 |
. . . . . . . . . . . . 13
⊢ (Fun
(𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → ∪
𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin))) |
53 | 51, 52 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ∪ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) |
54 | 53 | sseq1i 3592 |
. . . . . . . . . . 11
⊢ (∪ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏) |
55 | | iunss 4497 |
. . . . . . . . . . . 12
⊢ (∪ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏) |
56 | | inss1 3795 |
. . . . . . . . . . . . . . . . 17
⊢
(𝒫 𝑏 ∩
Fin) ⊆ 𝒫 𝑏 |
57 | | sspwb 4844 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 ⊆ 𝑥 ↔ 𝒫 𝑏 ⊆ 𝒫 𝑥) |
58 | 39, 57 | sylib 207 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 ∈ 𝒫 𝑥 → 𝒫 𝑏 ⊆ 𝒫 𝑥) |
59 | 58 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → 𝒫 𝑏 ⊆ 𝒫 𝑥) |
60 | 56, 59 | syl5ss 3579 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (𝒫 𝑏 ∩ Fin) ⊆ 𝒫 𝑥) |
61 | 60 | sselda 3568 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → 𝑒 ∈ 𝒫 𝑥) |
62 | 21, 22 | mrcssvd 16106 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑 ∈ 𝑎) → ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥) |
63 | 62 | ralrimiva 2949 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ⊆ (ACS‘𝑥) → ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥) |
64 | 63 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥) |
65 | | iunss 4497 |
. . . . . . . . . . . . . . . . 17
⊢ (∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥 ↔ ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥) |
66 | 64, 65 | sylibr 223 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥) |
67 | | ssexg 4732 |
. . . . . . . . . . . . . . . 16
⊢
((∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥 ∧ 𝑥 ∈ V) → ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ∈ V) |
68 | 66, 12, 67 | sylancl 693 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ∈ V) |
69 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 = 𝑒 → ((mrCls‘𝑑)‘𝑐) = ((mrCls‘𝑑)‘𝑒)) |
70 | 69 | iuneq2d 4483 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = 𝑒 → ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) = ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒)) |
71 | 70, 30 | fvmptg 6189 |
. . . . . . . . . . . . . . 15
⊢ ((𝑒 ∈ 𝒫 𝑥 ∧ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ∈ V) → ((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒)) |
72 | 61, 68, 71 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → ((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒)) |
73 | 72 | sseq1d 3595 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → (((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)) |
74 | 73 | ralbidva 2968 |
. . . . . . . . . . . 12
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)) |
75 | 55, 74 | syl5bb 271 |
. . . . . . . . . . 11
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∪
𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)) |
76 | 54, 75 | syl5bbr 273 |
. . . . . . . . . 10
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∪
((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)) |
77 | 48, 50, 76 | 3bitr4d 299 |
. . . . . . . . 9
⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ ((𝑐
∈ 𝒫 𝑥 ↦
∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)) |
78 | 77 | ralrimiva 2949 |
. . . . . . . 8
⊢ (𝑎 ⊆ (ACS‘𝑥) → ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ ((𝑐
∈ 𝒫 𝑥 ↦
∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)) |
79 | 31, 78 | jca 553 |
. . . . . . 7
⊢ (𝑎 ⊆ (ACS‘𝑥) → ((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ ((𝑐
∈ 𝒫 𝑥 ↦
∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))) |
80 | | feq1 5939 |
. . . . . . . . 9
⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → (𝑓:𝒫 𝑥⟶𝒫 𝑥 ↔ (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥)) |
81 | | imaeq1 5380 |
. . . . . . . . . . . . 13
⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → (𝑓 “ (𝒫 𝑏 ∩ Fin)) = ((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin))) |
82 | 81 | unieqd 4382 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → ∪ (𝑓 “ (𝒫 𝑏 ∩ Fin)) = ∪ ((𝑐
∈ 𝒫 𝑥 ↦
∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin))) |
83 | 82 | sseq1d 3595 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → (∪
(𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏 ↔ ∪ ((𝑐
∈ 𝒫 𝑥 ↦
∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)) |
84 | 83 | bibi2d 331 |
. . . . . . . . . 10
⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → ((𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ (𝑓
“ (𝒫 𝑏 ∩
Fin)) ⊆ 𝑏) ↔
(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎)
↔ ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))) |
85 | 84 | ralbidv 2969 |
. . . . . . . . 9
⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → (∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ (𝑓
“ (𝒫 𝑏 ∩
Fin)) ⊆ 𝑏) ↔
∀𝑏 ∈ 𝒫
𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ ((𝑐
∈ 𝒫 𝑥 ↦
∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))) |
86 | 80, 85 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → ((𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ (𝑓
“ (𝒫 𝑏 ∩
Fin)) ⊆ 𝑏)) ↔
((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ ((𝑐
∈ 𝒫 𝑥 ↦
∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)))) |
87 | 86 | spcegv 3267 |
. . . . . . 7
⊢ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) ∈ V → (((𝑐 ∈ 𝒫 𝑥 ↦ ∪
𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ ((𝑐
∈ 𝒫 𝑥 ↦
∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)) → ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ (𝑓
“ (𝒫 𝑏 ∩
Fin)) ⊆ 𝑏)))) |
88 | 37, 79, 87 | sylc 63 |
. . . . . 6
⊢ (𝑎 ⊆ (ACS‘𝑥) → ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ (𝑓
“ (𝒫 𝑏 ∩
Fin)) ⊆ 𝑏))) |
89 | | isacs 16135 |
. . . . . 6
⊢
((𝒫 𝑥 ∩
∩ 𝑎) ∈ (ACS‘𝑥) ↔ ((𝒫 𝑥 ∩ ∩ 𝑎) ∈ (Moore‘𝑥) ∧ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ (𝑓
“ (𝒫 𝑏 ∩
Fin)) ⊆ 𝑏)))) |
90 | 19, 88, 89 | sylanbrc 695 |
. . . . 5
⊢ (𝑎 ⊆ (ACS‘𝑥) → (𝒫 𝑥 ∩ ∩ 𝑎)
∈ (ACS‘𝑥)) |
91 | 90 | adantl 481 |
. . . 4
⊢
((⊤ ∧ 𝑎
⊆ (ACS‘𝑥))
→ (𝒫 𝑥 ∩
∩ 𝑎) ∈ (ACS‘𝑥)) |
92 | 11, 91 | ismred2 16086 |
. . 3
⊢ (⊤
→ (ACS‘𝑥) ∈
(Moore‘𝒫 𝑥)) |
93 | 92 | trud 1484 |
. 2
⊢
(ACS‘𝑥) ∈
(Moore‘𝒫 𝑥) |
94 | 4, 93 | vtoclg 3239 |
1
⊢ (𝑋 ∈ 𝑉 → (ACS‘𝑋) ∈ (Moore‘𝒫 𝑋)) |