Step | Hyp | Ref
| Expression |
1 | | acsmre 16915 |
. 2
⊢ (𝐶 ∈ (ACS‘𝑋) → 𝐶 ∈ (Moore‘𝑋)) |
2 | | mresspw 16855 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐶 ⊆ 𝒫 𝑋) |
3 | 1, 2 | syl 17 |
. . . . . . . . . 10
⊢ (𝐶 ∈ (ACS‘𝑋) → 𝐶 ⊆ 𝒫 𝑋) |
4 | | sspwb 5332 |
. . . . . . . . . 10
⊢ (𝐶 ⊆ 𝒫 𝑋 ↔ 𝒫 𝐶 ⊆ 𝒫 𝒫
𝑋) |
5 | 3, 4 | sylib 220 |
. . . . . . . . 9
⊢ (𝐶 ∈ (ACS‘𝑋) → 𝒫 𝐶 ⊆ 𝒫 𝒫
𝑋) |
6 | 5 | sselda 3965 |
. . . . . . . 8
⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) → 𝑠 ∈ 𝒫 𝒫 𝑋) |
7 | 6 | elpwid 4551 |
. . . . . . 7
⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) → 𝑠 ⊆ 𝒫 𝑋) |
8 | | sspwuni 5013 |
. . . . . . 7
⊢ (𝑠 ⊆ 𝒫 𝑋 ↔ ∪ 𝑠
⊆ 𝑋) |
9 | 7, 8 | sylib 220 |
. . . . . 6
⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) → ∪ 𝑠 ⊆ 𝑋) |
10 | 9 | adantr 483 |
. . . . 5
⊢ (((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → ∪ 𝑠
⊆ 𝑋) |
11 | | elinel1 4170 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin) → 𝑥 ∈
𝒫 ∪ 𝑠) |
12 | 11 | elpwid 4551 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin) → 𝑥 ⊆
∪ 𝑠) |
13 | | elinel2 4171 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin) → 𝑥 ∈
Fin) |
14 | | fissuni 8821 |
. . . . . . . . . 10
⊢ ((𝑥 ⊆ ∪ 𝑠
∧ 𝑥 ∈ Fin) →
∃𝑦 ∈ (𝒫
𝑠 ∩ Fin)𝑥 ⊆ ∪ 𝑦) |
15 | 12, 13, 14 | syl2anc 586 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin) → ∃𝑦
∈ (𝒫 𝑠 ∩
Fin)𝑥 ⊆ ∪ 𝑦) |
16 | 15 | ad2antll 727 |
. . . . . . . 8
⊢ (((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin))) → ∃𝑦 ∈ (𝒫 𝑠 ∩ Fin)𝑥 ⊆ ∪ 𝑦) |
17 | 1 | ad3antrrr 728 |
. . . . . . . . . 10
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin))) ∧ (𝑦
∈ (𝒫 𝑠 ∩
Fin) ∧ 𝑥 ⊆ ∪ 𝑦))
→ 𝐶 ∈
(Moore‘𝑋)) |
18 | | eqid 2819 |
. . . . . . . . . 10
⊢
(mrCls‘𝐶) =
(mrCls‘𝐶) |
19 | | simprr 771 |
. . . . . . . . . 10
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin))) ∧ (𝑦
∈ (𝒫 𝑠 ∩
Fin) ∧ 𝑥 ⊆ ∪ 𝑦))
→ 𝑥 ⊆ ∪ 𝑦) |
20 | | elinel1 4170 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝒫 𝑠 ∩ Fin) → 𝑦 ∈ 𝒫 𝑠) |
21 | 20 | elpwid 4551 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (𝒫 𝑠 ∩ Fin) → 𝑦 ⊆ 𝑠) |
22 | 21 | unissd 4854 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (𝒫 𝑠 ∩ Fin) → ∪ 𝑦
⊆ ∪ 𝑠) |
23 | 22 | ad2antrl 726 |
. . . . . . . . . . 11
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin))) ∧ (𝑦
∈ (𝒫 𝑠 ∩
Fin) ∧ 𝑥 ⊆ ∪ 𝑦))
→ ∪ 𝑦 ⊆ ∪ 𝑠) |
24 | 9 | ad2antrr 724 |
. . . . . . . . . . 11
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin))) ∧ (𝑦
∈ (𝒫 𝑠 ∩
Fin) ∧ 𝑥 ⊆ ∪ 𝑦))
→ ∪ 𝑠 ⊆ 𝑋) |
25 | 23, 24 | sstrd 3975 |
. . . . . . . . . 10
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin))) ∧ (𝑦
∈ (𝒫 𝑠 ∩
Fin) ∧ 𝑥 ⊆ ∪ 𝑦))
→ ∪ 𝑦 ⊆ 𝑋) |
26 | 17, 18, 19, 25 | mrcssd 16887 |
. . . . . . . . 9
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin))) ∧ (𝑦
∈ (𝒫 𝑠 ∩
Fin) ∧ 𝑥 ⊆ ∪ 𝑦))
→ ((mrCls‘𝐶)‘𝑥) ⊆ ((mrCls‘𝐶)‘∪ 𝑦)) |
27 | | simpl 485 |
. . . . . . . . . . . . . . 15
⊢
(((toInc‘𝑠)
∈ Dirset ∧ 𝑦
∈ (𝒫 𝑠 ∩
Fin)) → (toInc‘𝑠) ∈ Dirset) |
28 | 21 | adantl 484 |
. . . . . . . . . . . . . . 15
⊢
(((toInc‘𝑠)
∈ Dirset ∧ 𝑦
∈ (𝒫 𝑠 ∩
Fin)) → 𝑦 ⊆
𝑠) |
29 | | elinel2 4171 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (𝒫 𝑠 ∩ Fin) → 𝑦 ∈ Fin) |
30 | 29 | adantl 484 |
. . . . . . . . . . . . . . 15
⊢
(((toInc‘𝑠)
∈ Dirset ∧ 𝑦
∈ (𝒫 𝑠 ∩
Fin)) → 𝑦 ∈
Fin) |
31 | | ipodrsfi 17765 |
. . . . . . . . . . . . . . 15
⊢
(((toInc‘𝑠)
∈ Dirset ∧ 𝑦
⊆ 𝑠 ∧ 𝑦 ∈ Fin) → ∃𝑥 ∈ 𝑠 ∪ 𝑦 ⊆ 𝑥) |
32 | 27, 28, 30, 31 | syl3anc 1366 |
. . . . . . . . . . . . . 14
⊢
(((toInc‘𝑠)
∈ Dirset ∧ 𝑦
∈ (𝒫 𝑠 ∩
Fin)) → ∃𝑥
∈ 𝑠 ∪ 𝑦
⊆ 𝑥) |
33 | 32 | adantl 484 |
. . . . . . . . . . . . 13
⊢ (((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin))) → ∃𝑥 ∈ 𝑠 ∪ 𝑦 ⊆ 𝑥) |
34 | 1 | ad3antrrr 728 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin))) ∧ (𝑥 ∈ 𝑠 ∧ ∪ 𝑦 ⊆ 𝑥)) → 𝐶 ∈ (Moore‘𝑋)) |
35 | | simprr 771 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin))) ∧ (𝑥 ∈ 𝑠 ∧ ∪ 𝑦 ⊆ 𝑥)) → ∪ 𝑦 ⊆ 𝑥) |
36 | | elpwi 4549 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ 𝒫 𝐶 → 𝑠 ⊆ 𝐶) |
37 | 36 | adantl 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) → 𝑠 ⊆ 𝐶) |
38 | 37 | ad2antrr 724 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin))) ∧ (𝑥 ∈ 𝑠 ∧ ∪ 𝑦 ⊆ 𝑥)) → 𝑠 ⊆ 𝐶) |
39 | | simprl 769 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin))) ∧ (𝑥 ∈ 𝑠 ∧ ∪ 𝑦 ⊆ 𝑥)) → 𝑥 ∈ 𝑠) |
40 | 38, 39 | sseldd 3966 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin))) ∧ (𝑥 ∈ 𝑠 ∧ ∪ 𝑦 ⊆ 𝑥)) → 𝑥 ∈ 𝐶) |
41 | 18 | mrcsscl 16883 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∪ 𝑦
⊆ 𝑥 ∧ 𝑥 ∈ 𝐶) → ((mrCls‘𝐶)‘∪ 𝑦) ⊆ 𝑥) |
42 | 34, 35, 40, 41 | syl3anc 1366 |
. . . . . . . . . . . . . 14
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin))) ∧ (𝑥 ∈ 𝑠 ∧ ∪ 𝑦 ⊆ 𝑥)) → ((mrCls‘𝐶)‘∪ 𝑦) ⊆ 𝑥) |
43 | | elssuni 4859 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝑠 → 𝑥 ⊆ ∪ 𝑠) |
44 | 43 | ad2antrl 726 |
. . . . . . . . . . . . . 14
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin))) ∧ (𝑥 ∈ 𝑠 ∧ ∪ 𝑦 ⊆ 𝑥)) → 𝑥 ⊆ ∪ 𝑠) |
45 | 42, 44 | sstrd 3975 |
. . . . . . . . . . . . 13
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin))) ∧ (𝑥 ∈ 𝑠 ∧ ∪ 𝑦 ⊆ 𝑥)) → ((mrCls‘𝐶)‘∪ 𝑦) ⊆ ∪ 𝑠) |
46 | 33, 45 | rexlimddv 3289 |
. . . . . . . . . . . 12
⊢ (((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin))) → ((mrCls‘𝐶)‘∪ 𝑦)
⊆ ∪ 𝑠) |
47 | 46 | anassrs 470 |
. . . . . . . . . . 11
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → ((mrCls‘𝐶)‘∪ 𝑦)
⊆ ∪ 𝑠) |
48 | 47 | adantrr 715 |
. . . . . . . . . 10
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) ∧ (𝑦 ∈ (𝒫 𝑠 ∩ Fin) ∧ 𝑥 ⊆ ∪ 𝑦)) → ((mrCls‘𝐶)‘∪ 𝑦)
⊆ ∪ 𝑠) |
49 | 48 | adantlrr 719 |
. . . . . . . . 9
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin))) ∧ (𝑦
∈ (𝒫 𝑠 ∩
Fin) ∧ 𝑥 ⊆ ∪ 𝑦))
→ ((mrCls‘𝐶)‘∪ 𝑦) ⊆ ∪ 𝑠) |
50 | 26, 49 | sstrd 3975 |
. . . . . . . 8
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin))) ∧ (𝑦
∈ (𝒫 𝑠 ∩
Fin) ∧ 𝑥 ⊆ ∪ 𝑦))
→ ((mrCls‘𝐶)‘𝑥) ⊆ ∪ 𝑠) |
51 | 16, 50 | rexlimddv 3289 |
. . . . . . 7
⊢ (((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin))) → ((mrCls‘𝐶)‘𝑥) ⊆ ∪ 𝑠) |
52 | 51 | anassrs 470 |
. . . . . 6
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) ∧ 𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin)) → ((mrCls‘𝐶)‘𝑥) ⊆ ∪ 𝑠) |
53 | 52 | ralrimiva 3180 |
. . . . 5
⊢ (((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → ∀𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin)((mrCls‘𝐶)‘𝑥) ⊆ ∪ 𝑠) |
54 | 18 | acsfiel 16917 |
. . . . . 6
⊢ (𝐶 ∈ (ACS‘𝑋) → (∪ 𝑠
∈ 𝐶 ↔ (∪ 𝑠
⊆ 𝑋 ∧
∀𝑥 ∈ (𝒫
∪ 𝑠 ∩ Fin)((mrCls‘𝐶)‘𝑥) ⊆ ∪ 𝑠))) |
55 | 54 | ad2antrr 724 |
. . . . 5
⊢ (((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → (∪ 𝑠
∈ 𝐶 ↔ (∪ 𝑠
⊆ 𝑋 ∧
∀𝑥 ∈ (𝒫
∪ 𝑠 ∩ Fin)((mrCls‘𝐶)‘𝑥) ⊆ ∪ 𝑠))) |
56 | 10, 53, 55 | mpbir2and 711 |
. . . 4
⊢ (((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → ∪ 𝑠
∈ 𝐶) |
57 | 56 | ex 415 |
. . 3
⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) → ((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) |
58 | 57 | ralrimiva 3180 |
. 2
⊢ (𝐶 ∈ (ACS‘𝑋) → ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) |
59 | 1, 58 | jca 514 |
1
⊢ (𝐶 ∈ (ACS‘𝑋) → (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶))) |