Step | Hyp | Ref
| Expression |
1 | | acsmre 16136 |
. 2
⊢ (𝐶 ∈ (ACS‘𝑋) → 𝐶 ∈ (Moore‘𝑋)) |
2 | | mresspw 16075 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐶 ⊆ 𝒫 𝑋) |
3 | 1, 2 | syl 17 |
. . . . . . . . . 10
⊢ (𝐶 ∈ (ACS‘𝑋) → 𝐶 ⊆ 𝒫 𝑋) |
4 | | sspwb 4844 |
. . . . . . . . . 10
⊢ (𝐶 ⊆ 𝒫 𝑋 ↔ 𝒫 𝐶 ⊆ 𝒫 𝒫
𝑋) |
5 | 3, 4 | sylib 207 |
. . . . . . . . 9
⊢ (𝐶 ∈ (ACS‘𝑋) → 𝒫 𝐶 ⊆ 𝒫 𝒫
𝑋) |
6 | 5 | sselda 3568 |
. . . . . . . 8
⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) → 𝑠 ∈ 𝒫 𝒫 𝑋) |
7 | 6 | elpwid 4118 |
. . . . . . 7
⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) → 𝑠 ⊆ 𝒫 𝑋) |
8 | | sspwuni 4547 |
. . . . . . 7
⊢ (𝑠 ⊆ 𝒫 𝑋 ↔ ∪ 𝑠
⊆ 𝑋) |
9 | 7, 8 | sylib 207 |
. . . . . 6
⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) → ∪ 𝑠 ⊆ 𝑋) |
10 | 9 | adantr 480 |
. . . . 5
⊢ (((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → ∪ 𝑠
⊆ 𝑋) |
11 | | inss1 3795 |
. . . . . . . . . . . 12
⊢
(𝒫 ∪ 𝑠 ∩ Fin) ⊆ 𝒫 ∪ 𝑠 |
12 | 11 | sseli 3564 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin) → 𝑥 ∈
𝒫 ∪ 𝑠) |
13 | 12 | elpwid 4118 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin) → 𝑥 ⊆
∪ 𝑠) |
14 | | inss2 3796 |
. . . . . . . . . . 11
⊢
(𝒫 ∪ 𝑠 ∩ Fin) ⊆ Fin |
15 | 14 | sseli 3564 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin) → 𝑥 ∈
Fin) |
16 | | fissuni 8154 |
. . . . . . . . . 10
⊢ ((𝑥 ⊆ ∪ 𝑠
∧ 𝑥 ∈ Fin) →
∃𝑦 ∈ (𝒫
𝑠 ∩ Fin)𝑥 ⊆ ∪ 𝑦) |
17 | 13, 15, 16 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin) → ∃𝑦
∈ (𝒫 𝑠 ∩
Fin)𝑥 ⊆ ∪ 𝑦) |
18 | 17 | ad2antll 761 |
. . . . . . . 8
⊢ (((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin))) → ∃𝑦 ∈ (𝒫 𝑠 ∩ Fin)𝑥 ⊆ ∪ 𝑦) |
19 | 1 | ad3antrrr 762 |
. . . . . . . . . 10
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin))) ∧ (𝑦
∈ (𝒫 𝑠 ∩
Fin) ∧ 𝑥 ⊆ ∪ 𝑦))
→ 𝐶 ∈
(Moore‘𝑋)) |
20 | | eqid 2610 |
. . . . . . . . . 10
⊢
(mrCls‘𝐶) =
(mrCls‘𝐶) |
21 | | simprr 792 |
. . . . . . . . . 10
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin))) ∧ (𝑦
∈ (𝒫 𝑠 ∩
Fin) ∧ 𝑥 ⊆ ∪ 𝑦))
→ 𝑥 ⊆ ∪ 𝑦) |
22 | | inss1 3795 |
. . . . . . . . . . . . . . 15
⊢
(𝒫 𝑠 ∩
Fin) ⊆ 𝒫 𝑠 |
23 | 22 | sseli 3564 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝒫 𝑠 ∩ Fin) → 𝑦 ∈ 𝒫 𝑠) |
24 | 23 | elpwid 4118 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (𝒫 𝑠 ∩ Fin) → 𝑦 ⊆ 𝑠) |
25 | 24 | unissd 4398 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (𝒫 𝑠 ∩ Fin) → ∪ 𝑦
⊆ ∪ 𝑠) |
26 | 25 | ad2antrl 760 |
. . . . . . . . . . 11
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin))) ∧ (𝑦
∈ (𝒫 𝑠 ∩
Fin) ∧ 𝑥 ⊆ ∪ 𝑦))
→ ∪ 𝑦 ⊆ ∪ 𝑠) |
27 | 9 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin))) ∧ (𝑦
∈ (𝒫 𝑠 ∩
Fin) ∧ 𝑥 ⊆ ∪ 𝑦))
→ ∪ 𝑠 ⊆ 𝑋) |
28 | 26, 27 | sstrd 3578 |
. . . . . . . . . 10
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin))) ∧ (𝑦
∈ (𝒫 𝑠 ∩
Fin) ∧ 𝑥 ⊆ ∪ 𝑦))
→ ∪ 𝑦 ⊆ 𝑋) |
29 | 19, 20, 21, 28 | mrcssd 16107 |
. . . . . . . . 9
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin))) ∧ (𝑦
∈ (𝒫 𝑠 ∩
Fin) ∧ 𝑥 ⊆ ∪ 𝑦))
→ ((mrCls‘𝐶)‘𝑥) ⊆ ((mrCls‘𝐶)‘∪ 𝑦)) |
30 | | simpl 472 |
. . . . . . . . . . . . . . 15
⊢
(((toInc‘𝑠)
∈ Dirset ∧ 𝑦
∈ (𝒫 𝑠 ∩
Fin)) → (toInc‘𝑠) ∈ Dirset) |
31 | 24 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢
(((toInc‘𝑠)
∈ Dirset ∧ 𝑦
∈ (𝒫 𝑠 ∩
Fin)) → 𝑦 ⊆
𝑠) |
32 | | inss2 3796 |
. . . . . . . . . . . . . . . . 17
⊢
(𝒫 𝑠 ∩
Fin) ⊆ Fin |
33 | 32 | sseli 3564 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (𝒫 𝑠 ∩ Fin) → 𝑦 ∈ Fin) |
34 | 33 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢
(((toInc‘𝑠)
∈ Dirset ∧ 𝑦
∈ (𝒫 𝑠 ∩
Fin)) → 𝑦 ∈
Fin) |
35 | | ipodrsfi 16986 |
. . . . . . . . . . . . . . 15
⊢
(((toInc‘𝑠)
∈ Dirset ∧ 𝑦
⊆ 𝑠 ∧ 𝑦 ∈ Fin) → ∃𝑥 ∈ 𝑠 ∪ 𝑦 ⊆ 𝑥) |
36 | 30, 31, 34, 35 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢
(((toInc‘𝑠)
∈ Dirset ∧ 𝑦
∈ (𝒫 𝑠 ∩
Fin)) → ∃𝑥
∈ 𝑠 ∪ 𝑦
⊆ 𝑥) |
37 | 36 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin))) → ∃𝑥 ∈ 𝑠 ∪ 𝑦 ⊆ 𝑥) |
38 | 1 | ad3antrrr 762 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin))) ∧ (𝑥 ∈ 𝑠 ∧ ∪ 𝑦 ⊆ 𝑥)) → 𝐶 ∈ (Moore‘𝑋)) |
39 | | simprr 792 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin))) ∧ (𝑥 ∈ 𝑠 ∧ ∪ 𝑦 ⊆ 𝑥)) → ∪ 𝑦 ⊆ 𝑥) |
40 | | elpwi 4117 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ 𝒫 𝐶 → 𝑠 ⊆ 𝐶) |
41 | 40 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) → 𝑠 ⊆ 𝐶) |
42 | 41 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin))) ∧ (𝑥 ∈ 𝑠 ∧ ∪ 𝑦 ⊆ 𝑥)) → 𝑠 ⊆ 𝐶) |
43 | | simprl 790 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin))) ∧ (𝑥 ∈ 𝑠 ∧ ∪ 𝑦 ⊆ 𝑥)) → 𝑥 ∈ 𝑠) |
44 | 42, 43 | sseldd 3569 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin))) ∧ (𝑥 ∈ 𝑠 ∧ ∪ 𝑦 ⊆ 𝑥)) → 𝑥 ∈ 𝐶) |
45 | 20 | mrcsscl 16103 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∪ 𝑦
⊆ 𝑥 ∧ 𝑥 ∈ 𝐶) → ((mrCls‘𝐶)‘∪ 𝑦) ⊆ 𝑥) |
46 | 38, 39, 44, 45 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin))) ∧ (𝑥 ∈ 𝑠 ∧ ∪ 𝑦 ⊆ 𝑥)) → ((mrCls‘𝐶)‘∪ 𝑦) ⊆ 𝑥) |
47 | | elssuni 4403 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝑠 → 𝑥 ⊆ ∪ 𝑠) |
48 | 47 | ad2antrl 760 |
. . . . . . . . . . . . . 14
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin))) ∧ (𝑥 ∈ 𝑠 ∧ ∪ 𝑦 ⊆ 𝑥)) → 𝑥 ⊆ ∪ 𝑠) |
49 | 46, 48 | sstrd 3578 |
. . . . . . . . . . . . 13
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin))) ∧ (𝑥 ∈ 𝑠 ∧ ∪ 𝑦 ⊆ 𝑥)) → ((mrCls‘𝐶)‘∪ 𝑦) ⊆ ∪ 𝑠) |
50 | 37, 49 | rexlimddv 3017 |
. . . . . . . . . . . 12
⊢ (((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin))) → ((mrCls‘𝐶)‘∪ 𝑦)
⊆ ∪ 𝑠) |
51 | 50 | anassrs 678 |
. . . . . . . . . . 11
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → ((mrCls‘𝐶)‘∪ 𝑦)
⊆ ∪ 𝑠) |
52 | 51 | adantrr 749 |
. . . . . . . . . 10
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) ∧ (𝑦 ∈ (𝒫 𝑠 ∩ Fin) ∧ 𝑥 ⊆ ∪ 𝑦)) → ((mrCls‘𝐶)‘∪ 𝑦)
⊆ ∪ 𝑠) |
53 | 52 | adantlrr 753 |
. . . . . . . . 9
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin))) ∧ (𝑦
∈ (𝒫 𝑠 ∩
Fin) ∧ 𝑥 ⊆ ∪ 𝑦))
→ ((mrCls‘𝐶)‘∪ 𝑦) ⊆ ∪ 𝑠) |
54 | 29, 53 | sstrd 3578 |
. . . . . . . 8
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin))) ∧ (𝑦
∈ (𝒫 𝑠 ∩
Fin) ∧ 𝑥 ⊆ ∪ 𝑦))
→ ((mrCls‘𝐶)‘𝑥) ⊆ ∪ 𝑠) |
55 | 18, 54 | rexlimddv 3017 |
. . . . . . 7
⊢ (((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin))) → ((mrCls‘𝐶)‘𝑥) ⊆ ∪ 𝑠) |
56 | 55 | anassrs 678 |
. . . . . 6
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) ∧ 𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin)) → ((mrCls‘𝐶)‘𝑥) ⊆ ∪ 𝑠) |
57 | 56 | ralrimiva 2949 |
. . . . 5
⊢ (((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → ∀𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin)((mrCls‘𝐶)‘𝑥) ⊆ ∪ 𝑠) |
58 | 20 | acsfiel 16138 |
. . . . . 6
⊢ (𝐶 ∈ (ACS‘𝑋) → (∪ 𝑠
∈ 𝐶 ↔ (∪ 𝑠
⊆ 𝑋 ∧
∀𝑥 ∈ (𝒫
∪ 𝑠 ∩ Fin)((mrCls‘𝐶)‘𝑥) ⊆ ∪ 𝑠))) |
59 | 58 | ad2antrr 758 |
. . . . 5
⊢ (((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → (∪ 𝑠
∈ 𝐶 ↔ (∪ 𝑠
⊆ 𝑋 ∧
∀𝑥 ∈ (𝒫
∪ 𝑠 ∩ Fin)((mrCls‘𝐶)‘𝑥) ⊆ ∪ 𝑠))) |
60 | 10, 57, 59 | mpbir2and 959 |
. . . 4
⊢ (((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → ∪ 𝑠
∈ 𝐶) |
61 | 60 | ex 449 |
. . 3
⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) → ((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) |
62 | 61 | ralrimiva 2949 |
. 2
⊢ (𝐶 ∈ (ACS‘𝑋) → ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) |
63 | 1, 62 | jca 553 |
1
⊢ (𝐶 ∈ (ACS‘𝑋) → (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶))) |