Step | Hyp | Ref
| Expression |
1 | | acsmre 17026 |
. 2
⊢ (𝐶 ∈ (ACS‘𝑋) → 𝐶 ∈ (Moore‘𝑋)) |
2 | | mresspw 16966 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐶 ⊆ 𝒫 𝑋) |
3 | 1, 2 | syl 17 |
. . . . . . . . . 10
⊢ (𝐶 ∈ (ACS‘𝑋) → 𝐶 ⊆ 𝒫 𝑋) |
4 | 3 | sspwd 4503 |
. . . . . . . . 9
⊢ (𝐶 ∈ (ACS‘𝑋) → 𝒫 𝐶 ⊆ 𝒫 𝒫
𝑋) |
5 | 4 | sselda 3877 |
. . . . . . . 8
⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) → 𝑠 ∈ 𝒫 𝒫 𝑋) |
6 | 5 | elpwid 4499 |
. . . . . . 7
⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) → 𝑠 ⊆ 𝒫 𝑋) |
7 | | sspwuni 4985 |
. . . . . . 7
⊢ (𝑠 ⊆ 𝒫 𝑋 ↔ ∪ 𝑠
⊆ 𝑋) |
8 | 6, 7 | sylib 221 |
. . . . . 6
⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) → ∪ 𝑠 ⊆ 𝑋) |
9 | 8 | adantr 484 |
. . . . 5
⊢ (((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → ∪ 𝑠
⊆ 𝑋) |
10 | | elinel1 4085 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin) → 𝑥 ∈
𝒫 ∪ 𝑠) |
11 | 10 | elpwid 4499 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin) → 𝑥 ⊆
∪ 𝑠) |
12 | | elinel2 4086 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin) → 𝑥 ∈
Fin) |
13 | | fissuni 8902 |
. . . . . . . . . 10
⊢ ((𝑥 ⊆ ∪ 𝑠
∧ 𝑥 ∈ Fin) →
∃𝑦 ∈ (𝒫
𝑠 ∩ Fin)𝑥 ⊆ ∪ 𝑦) |
14 | 11, 12, 13 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin) → ∃𝑦
∈ (𝒫 𝑠 ∩
Fin)𝑥 ⊆ ∪ 𝑦) |
15 | 14 | ad2antll 729 |
. . . . . . . 8
⊢ (((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin))) → ∃𝑦 ∈ (𝒫 𝑠 ∩ Fin)𝑥 ⊆ ∪ 𝑦) |
16 | 1 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin))) ∧ (𝑦
∈ (𝒫 𝑠 ∩
Fin) ∧ 𝑥 ⊆ ∪ 𝑦))
→ 𝐶 ∈
(Moore‘𝑋)) |
17 | | eqid 2738 |
. . . . . . . . . 10
⊢
(mrCls‘𝐶) =
(mrCls‘𝐶) |
18 | | simprr 773 |
. . . . . . . . . 10
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin))) ∧ (𝑦
∈ (𝒫 𝑠 ∩
Fin) ∧ 𝑥 ⊆ ∪ 𝑦))
→ 𝑥 ⊆ ∪ 𝑦) |
19 | | elinel1 4085 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝒫 𝑠 ∩ Fin) → 𝑦 ∈ 𝒫 𝑠) |
20 | 19 | elpwid 4499 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (𝒫 𝑠 ∩ Fin) → 𝑦 ⊆ 𝑠) |
21 | 20 | unissd 4806 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (𝒫 𝑠 ∩ Fin) → ∪ 𝑦
⊆ ∪ 𝑠) |
22 | 21 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin))) ∧ (𝑦
∈ (𝒫 𝑠 ∩
Fin) ∧ 𝑥 ⊆ ∪ 𝑦))
→ ∪ 𝑦 ⊆ ∪ 𝑠) |
23 | 8 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin))) ∧ (𝑦
∈ (𝒫 𝑠 ∩
Fin) ∧ 𝑥 ⊆ ∪ 𝑦))
→ ∪ 𝑠 ⊆ 𝑋) |
24 | 22, 23 | sstrd 3887 |
. . . . . . . . . 10
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin))) ∧ (𝑦
∈ (𝒫 𝑠 ∩
Fin) ∧ 𝑥 ⊆ ∪ 𝑦))
→ ∪ 𝑦 ⊆ 𝑋) |
25 | 16, 17, 18, 24 | mrcssd 16998 |
. . . . . . . . 9
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin))) ∧ (𝑦
∈ (𝒫 𝑠 ∩
Fin) ∧ 𝑥 ⊆ ∪ 𝑦))
→ ((mrCls‘𝐶)‘𝑥) ⊆ ((mrCls‘𝐶)‘∪ 𝑦)) |
26 | | simpl 486 |
. . . . . . . . . . . . . . 15
⊢
(((toInc‘𝑠)
∈ Dirset ∧ 𝑦
∈ (𝒫 𝑠 ∩
Fin)) → (toInc‘𝑠) ∈ Dirset) |
27 | 20 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢
(((toInc‘𝑠)
∈ Dirset ∧ 𝑦
∈ (𝒫 𝑠 ∩
Fin)) → 𝑦 ⊆
𝑠) |
28 | | elinel2 4086 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (𝒫 𝑠 ∩ Fin) → 𝑦 ∈ Fin) |
29 | 28 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢
(((toInc‘𝑠)
∈ Dirset ∧ 𝑦
∈ (𝒫 𝑠 ∩
Fin)) → 𝑦 ∈
Fin) |
30 | | ipodrsfi 17889 |
. . . . . . . . . . . . . . 15
⊢
(((toInc‘𝑠)
∈ Dirset ∧ 𝑦
⊆ 𝑠 ∧ 𝑦 ∈ Fin) → ∃𝑥 ∈ 𝑠 ∪ 𝑦 ⊆ 𝑥) |
31 | 26, 27, 29, 30 | syl3anc 1372 |
. . . . . . . . . . . . . 14
⊢
(((toInc‘𝑠)
∈ Dirset ∧ 𝑦
∈ (𝒫 𝑠 ∩
Fin)) → ∃𝑥
∈ 𝑠 ∪ 𝑦
⊆ 𝑥) |
32 | 31 | adantl 485 |
. . . . . . . . . . . . 13
⊢ (((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin))) → ∃𝑥 ∈ 𝑠 ∪ 𝑦 ⊆ 𝑥) |
33 | 1 | ad3antrrr 730 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin))) ∧ (𝑥 ∈ 𝑠 ∧ ∪ 𝑦 ⊆ 𝑥)) → 𝐶 ∈ (Moore‘𝑋)) |
34 | | simprr 773 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin))) ∧ (𝑥 ∈ 𝑠 ∧ ∪ 𝑦 ⊆ 𝑥)) → ∪ 𝑦 ⊆ 𝑥) |
35 | | elpwi 4497 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ 𝒫 𝐶 → 𝑠 ⊆ 𝐶) |
36 | 35 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) → 𝑠 ⊆ 𝐶) |
37 | 36 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin))) ∧ (𝑥 ∈ 𝑠 ∧ ∪ 𝑦 ⊆ 𝑥)) → 𝑠 ⊆ 𝐶) |
38 | | simprl 771 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin))) ∧ (𝑥 ∈ 𝑠 ∧ ∪ 𝑦 ⊆ 𝑥)) → 𝑥 ∈ 𝑠) |
39 | 37, 38 | sseldd 3878 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin))) ∧ (𝑥 ∈ 𝑠 ∧ ∪ 𝑦 ⊆ 𝑥)) → 𝑥 ∈ 𝐶) |
40 | 17 | mrcsscl 16994 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∪ 𝑦
⊆ 𝑥 ∧ 𝑥 ∈ 𝐶) → ((mrCls‘𝐶)‘∪ 𝑦) ⊆ 𝑥) |
41 | 33, 34, 39, 40 | syl3anc 1372 |
. . . . . . . . . . . . . 14
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin))) ∧ (𝑥 ∈ 𝑠 ∧ ∪ 𝑦 ⊆ 𝑥)) → ((mrCls‘𝐶)‘∪ 𝑦) ⊆ 𝑥) |
42 | | elssuni 4828 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝑠 → 𝑥 ⊆ ∪ 𝑠) |
43 | 42 | ad2antrl 728 |
. . . . . . . . . . . . . 14
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin))) ∧ (𝑥 ∈ 𝑠 ∧ ∪ 𝑦 ⊆ 𝑥)) → 𝑥 ⊆ ∪ 𝑠) |
44 | 41, 43 | sstrd 3887 |
. . . . . . . . . . . . 13
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin))) ∧ (𝑥 ∈ 𝑠 ∧ ∪ 𝑦 ⊆ 𝑥)) → ((mrCls‘𝐶)‘∪ 𝑦) ⊆ ∪ 𝑠) |
45 | 32, 44 | rexlimddv 3201 |
. . . . . . . . . . . 12
⊢ (((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin))) → ((mrCls‘𝐶)‘∪ 𝑦)
⊆ ∪ 𝑠) |
46 | 45 | anassrs 471 |
. . . . . . . . . . 11
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → ((mrCls‘𝐶)‘∪ 𝑦)
⊆ ∪ 𝑠) |
47 | 46 | adantrr 717 |
. . . . . . . . . 10
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) ∧ (𝑦 ∈ (𝒫 𝑠 ∩ Fin) ∧ 𝑥 ⊆ ∪ 𝑦)) → ((mrCls‘𝐶)‘∪ 𝑦)
⊆ ∪ 𝑠) |
48 | 47 | adantlrr 721 |
. . . . . . . . 9
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin))) ∧ (𝑦
∈ (𝒫 𝑠 ∩
Fin) ∧ 𝑥 ⊆ ∪ 𝑦))
→ ((mrCls‘𝐶)‘∪ 𝑦) ⊆ ∪ 𝑠) |
49 | 25, 48 | sstrd 3887 |
. . . . . . . 8
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin))) ∧ (𝑦
∈ (𝒫 𝑠 ∩
Fin) ∧ 𝑥 ⊆ ∪ 𝑦))
→ ((mrCls‘𝐶)‘𝑥) ⊆ ∪ 𝑠) |
50 | 15, 49 | rexlimddv 3201 |
. . . . . . 7
⊢ (((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ ((toInc‘𝑠) ∈ Dirset ∧ 𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin))) → ((mrCls‘𝐶)‘𝑥) ⊆ ∪ 𝑠) |
51 | 50 | anassrs 471 |
. . . . . 6
⊢ ((((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) ∧ 𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin)) → ((mrCls‘𝐶)‘𝑥) ⊆ ∪ 𝑠) |
52 | 51 | ralrimiva 3096 |
. . . . 5
⊢ (((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → ∀𝑥 ∈ (𝒫 ∪ 𝑠
∩ Fin)((mrCls‘𝐶)‘𝑥) ⊆ ∪ 𝑠) |
53 | 17 | acsfiel 17028 |
. . . . . 6
⊢ (𝐶 ∈ (ACS‘𝑋) → (∪ 𝑠
∈ 𝐶 ↔ (∪ 𝑠
⊆ 𝑋 ∧
∀𝑥 ∈ (𝒫
∪ 𝑠 ∩ Fin)((mrCls‘𝐶)‘𝑥) ⊆ ∪ 𝑠))) |
54 | 53 | ad2antrr 726 |
. . . . 5
⊢ (((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → (∪ 𝑠
∈ 𝐶 ↔ (∪ 𝑠
⊆ 𝑋 ∧
∀𝑥 ∈ (𝒫
∪ 𝑠 ∩ Fin)((mrCls‘𝐶)‘𝑥) ⊆ ∪ 𝑠))) |
55 | 9, 52, 54 | mpbir2and 713 |
. . . 4
⊢ (((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → ∪ 𝑠
∈ 𝐶) |
56 | 55 | ex 416 |
. . 3
⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) → ((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) |
57 | 56 | ralrimiva 3096 |
. 2
⊢ (𝐶 ∈ (ACS‘𝑋) → ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) |
58 | 1, 57 | jca 515 |
1
⊢ (𝐶 ∈ (ACS‘𝑋) → (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶))) |