Step | Hyp | Ref
| Expression |
1 | | nacsacs 36290 |
. . . 4
⊢ (𝐶 ∈ (NoeACS‘𝑋) → 𝐶 ∈ (ACS‘𝑋)) |
2 | 1 | acsmred 16140 |
. . 3
⊢ (𝐶 ∈ (NoeACS‘𝑋) → 𝐶 ∈ (Moore‘𝑋)) |
3 | | simpll 786 |
. . . . . . . 8
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → 𝐶 ∈ (NoeACS‘𝑋)) |
4 | 1 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → 𝐶 ∈ (ACS‘𝑋)) |
5 | | elpwi 4117 |
. . . . . . . . . 10
⊢ (𝑠 ∈ 𝒫 𝐶 → 𝑠 ⊆ 𝐶) |
6 | 5 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → 𝑠 ⊆ 𝐶) |
7 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → (toInc‘𝑠) ∈
Dirset) |
8 | | acsdrsel 16990 |
. . . . . . . . 9
⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ⊆ 𝐶 ∧ (toInc‘𝑠) ∈ Dirset) → ∪ 𝑠
∈ 𝐶) |
9 | 4, 6, 7, 8 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → ∪ 𝑠
∈ 𝐶) |
10 | | eqid 2610 |
. . . . . . . . 9
⊢
(mrCls‘𝐶) =
(mrCls‘𝐶) |
11 | 10 | nacsfg 36286 |
. . . . . . . 8
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ ∪ 𝑠
∈ 𝐶) →
∃𝑔 ∈ (𝒫
𝑋 ∩ Fin)∪ 𝑠 =
((mrCls‘𝐶)‘𝑔)) |
12 | 3, 9, 11 | syl2anc 691 |
. . . . . . 7
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑠 =
((mrCls‘𝐶)‘𝑔)) |
13 | 10 | mrefg2 36288 |
. . . . . . . . 9
⊢ (𝐶 ∈ (Moore‘𝑋) → (∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑠 =
((mrCls‘𝐶)‘𝑔) ↔ ∃𝑔 ∈ (𝒫 ∪ 𝑠
∩ Fin)∪ 𝑠 = ((mrCls‘𝐶)‘𝑔))) |
14 | 2, 13 | syl 17 |
. . . . . . . 8
⊢ (𝐶 ∈ (NoeACS‘𝑋) → (∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑠 =
((mrCls‘𝐶)‘𝑔) ↔ ∃𝑔 ∈ (𝒫 ∪ 𝑠
∩ Fin)∪ 𝑠 = ((mrCls‘𝐶)‘𝑔))) |
15 | 14 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → (∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑠 =
((mrCls‘𝐶)‘𝑔) ↔ ∃𝑔 ∈ (𝒫 ∪ 𝑠
∩ Fin)∪ 𝑠 = ((mrCls‘𝐶)‘𝑔))) |
16 | 12, 15 | mpbid 221 |
. . . . . 6
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → ∃𝑔 ∈ (𝒫 ∪ 𝑠
∩ Fin)∪ 𝑠 = ((mrCls‘𝐶)‘𝑔)) |
17 | | elfpw 8151 |
. . . . . . . . 9
⊢ (𝑔 ∈ (𝒫 ∪ 𝑠
∩ Fin) ↔ (𝑔
⊆ ∪ 𝑠 ∧ 𝑔 ∈ Fin)) |
18 | | fissuni 8154 |
. . . . . . . . 9
⊢ ((𝑔 ⊆ ∪ 𝑠
∧ 𝑔 ∈ Fin) →
∃ℎ ∈ (𝒫
𝑠 ∩ Fin)𝑔 ⊆ ∪ ℎ) |
19 | 17, 18 | sylbi 206 |
. . . . . . . 8
⊢ (𝑔 ∈ (𝒫 ∪ 𝑠
∩ Fin) → ∃ℎ
∈ (𝒫 𝑠 ∩
Fin)𝑔 ⊆ ∪ ℎ) |
20 | | elfpw 8151 |
. . . . . . . . . . . 12
⊢ (ℎ ∈ (𝒫 𝑠 ∩ Fin) ↔ (ℎ ⊆ 𝑠 ∧ ℎ ∈ Fin)) |
21 | | ipodrsfi 16986 |
. . . . . . . . . . . . 13
⊢
(((toInc‘𝑠)
∈ Dirset ∧ ℎ
⊆ 𝑠 ∧ ℎ ∈ Fin) → ∃𝑖 ∈ 𝑠 ∪ ℎ ⊆ 𝑖) |
22 | 21 | 3expb 1258 |
. . . . . . . . . . . 12
⊢
(((toInc‘𝑠)
∈ Dirset ∧ (ℎ
⊆ 𝑠 ∧ ℎ ∈ Fin)) → ∃𝑖 ∈ 𝑠 ∪ ℎ ⊆ 𝑖) |
23 | 20, 22 | sylan2b 491 |
. . . . . . . . . . 11
⊢
(((toInc‘𝑠)
∈ Dirset ∧ ℎ ∈
(𝒫 𝑠 ∩ Fin))
→ ∃𝑖 ∈
𝑠 ∪ ℎ
⊆ 𝑖) |
24 | | sstr 3576 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔 ⊆ ∪ ℎ
∧ ∪ ℎ ⊆ 𝑖) → 𝑔 ⊆ 𝑖) |
25 | 24 | ancoms 468 |
. . . . . . . . . . . . . 14
⊢ ((∪ ℎ
⊆ 𝑖 ∧ 𝑔 ⊆ ∪ ℎ)
→ 𝑔 ⊆ 𝑖) |
26 | | simpr 476 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖 ∈ 𝑠 ∧ 𝑔 ⊆ 𝑖)) ∧ ∪ 𝑠 = ((mrCls‘𝐶)‘𝑔)) → ∪ 𝑠 = ((mrCls‘𝐶)‘𝑔)) |
27 | 2 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖 ∈ 𝑠 ∧ 𝑔 ⊆ 𝑖)) → 𝐶 ∈ (Moore‘𝑋)) |
28 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖 ∈ 𝑠 ∧ 𝑔 ⊆ 𝑖)) → 𝑔 ⊆ 𝑖) |
29 | 5 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖 ∈ 𝑠 ∧ 𝑔 ⊆ 𝑖)) → 𝑠 ⊆ 𝐶) |
30 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖 ∈ 𝑠 ∧ 𝑔 ⊆ 𝑖)) → 𝑖 ∈ 𝑠) |
31 | 29, 30 | sseldd 3569 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖 ∈ 𝑠 ∧ 𝑔 ⊆ 𝑖)) → 𝑖 ∈ 𝐶) |
32 | 10 | mrcsscl 16103 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑔 ⊆ 𝑖 ∧ 𝑖 ∈ 𝐶) → ((mrCls‘𝐶)‘𝑔) ⊆ 𝑖) |
33 | 27, 28, 31, 32 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖 ∈ 𝑠 ∧ 𝑔 ⊆ 𝑖)) → ((mrCls‘𝐶)‘𝑔) ⊆ 𝑖) |
34 | 33 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖 ∈ 𝑠 ∧ 𝑔 ⊆ 𝑖)) ∧ ∪ 𝑠 = ((mrCls‘𝐶)‘𝑔)) → ((mrCls‘𝐶)‘𝑔) ⊆ 𝑖) |
35 | 26, 34 | eqsstrd 3602 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖 ∈ 𝑠 ∧ 𝑔 ⊆ 𝑖)) ∧ ∪ 𝑠 = ((mrCls‘𝐶)‘𝑔)) → ∪ 𝑠 ⊆ 𝑖) |
36 | | simplrl 796 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖 ∈ 𝑠 ∧ 𝑔 ⊆ 𝑖)) ∧ ∪ 𝑠 = ((mrCls‘𝐶)‘𝑔)) → 𝑖 ∈ 𝑠) |
37 | | elssuni 4403 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ 𝑠 → 𝑖 ⊆ ∪ 𝑠) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖 ∈ 𝑠 ∧ 𝑔 ⊆ 𝑖)) ∧ ∪ 𝑠 = ((mrCls‘𝐶)‘𝑔)) → 𝑖 ⊆ ∪ 𝑠) |
39 | 35, 38 | eqssd 3585 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖 ∈ 𝑠 ∧ 𝑔 ⊆ 𝑖)) ∧ ∪ 𝑠 = ((mrCls‘𝐶)‘𝑔)) → ∪ 𝑠 = 𝑖) |
40 | 39, 36 | eqeltrd 2688 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖 ∈ 𝑠 ∧ 𝑔 ⊆ 𝑖)) ∧ ∪ 𝑠 = ((mrCls‘𝐶)‘𝑔)) → ∪ 𝑠 ∈ 𝑠) |
41 | 40 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖 ∈ 𝑠 ∧ 𝑔 ⊆ 𝑖)) → (∪ 𝑠 = ((mrCls‘𝐶)‘𝑔) → ∪ 𝑠 ∈ 𝑠)) |
42 | 41 | expr 641 |
. . . . . . . . . . . . . 14
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ 𝑖 ∈ 𝑠) → (𝑔 ⊆ 𝑖 → (∪ 𝑠 = ((mrCls‘𝐶)‘𝑔) → ∪ 𝑠 ∈ 𝑠))) |
43 | 25, 42 | syl5 33 |
. . . . . . . . . . . . 13
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ 𝑖 ∈ 𝑠) → ((∪ ℎ ⊆ 𝑖 ∧ 𝑔 ⊆ ∪ ℎ) → (∪ 𝑠 =
((mrCls‘𝐶)‘𝑔) → ∪ 𝑠 ∈ 𝑠))) |
44 | 43 | expd 451 |
. . . . . . . . . . . 12
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ 𝑖 ∈ 𝑠) → (∪ ℎ ⊆ 𝑖 → (𝑔 ⊆ ∪ ℎ → (∪ 𝑠 =
((mrCls‘𝐶)‘𝑔) → ∪ 𝑠 ∈ 𝑠)))) |
45 | 44 | rexlimdva 3013 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) → (∃𝑖 ∈ 𝑠 ∪ ℎ ⊆ 𝑖 → (𝑔 ⊆ ∪ ℎ → (∪ 𝑠 =
((mrCls‘𝐶)‘𝑔) → ∪ 𝑠 ∈ 𝑠)))) |
46 | 23, 45 | syl5 33 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) → (((toInc‘𝑠) ∈ Dirset ∧ ℎ ∈ (𝒫 𝑠 ∩ Fin)) → (𝑔 ⊆ ∪ ℎ → (∪ 𝑠 =
((mrCls‘𝐶)‘𝑔) → ∪ 𝑠 ∈ 𝑠)))) |
47 | 46 | expdimp 452 |
. . . . . . . . 9
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → (ℎ ∈ (𝒫 𝑠 ∩ Fin) → (𝑔 ⊆ ∪ ℎ → (∪ 𝑠 =
((mrCls‘𝐶)‘𝑔) → ∪ 𝑠 ∈ 𝑠)))) |
48 | 47 | rexlimdv 3012 |
. . . . . . . 8
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → (∃ℎ ∈ (𝒫 𝑠 ∩ Fin)𝑔 ⊆ ∪ ℎ → (∪ 𝑠 =
((mrCls‘𝐶)‘𝑔) → ∪ 𝑠 ∈ 𝑠))) |
49 | 19, 48 | syl5 33 |
. . . . . . 7
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → (𝑔 ∈ (𝒫 ∪ 𝑠
∩ Fin) → (∪ 𝑠 = ((mrCls‘𝐶)‘𝑔) → ∪ 𝑠 ∈ 𝑠))) |
50 | 49 | rexlimdv 3012 |
. . . . . 6
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → (∃𝑔 ∈ (𝒫 ∪ 𝑠
∩ Fin)∪ 𝑠 = ((mrCls‘𝐶)‘𝑔) → ∪ 𝑠 ∈ 𝑠)) |
51 | 16, 50 | mpd 15 |
. . . . 5
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → ∪ 𝑠
∈ 𝑠) |
52 | 51 | ex 449 |
. . . 4
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) → ((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) |
53 | 52 | ralrimiva 2949 |
. . 3
⊢ (𝐶 ∈ (NoeACS‘𝑋) → ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) |
54 | 2, 53 | jca 553 |
. 2
⊢ (𝐶 ∈ (NoeACS‘𝑋) → (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠))) |
55 | | simpl 472 |
. . . 4
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) → 𝐶 ∈ (Moore‘𝑋)) |
56 | 5 | adantl 481 |
. . . . . . . 8
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) → 𝑠 ⊆ 𝐶) |
57 | 56 | sseld 3567 |
. . . . . . 7
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) → (∪ 𝑠 ∈ 𝑠 → ∪ 𝑠 ∈ 𝐶)) |
58 | 57 | imim2d 55 |
. . . . . 6
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) → (((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠) →
((toInc‘𝑠) ∈
Dirset → ∪ 𝑠 ∈ 𝐶))) |
59 | 58 | ralimdva 2945 |
. . . . 5
⊢ (𝐶 ∈ (Moore‘𝑋) → (∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠) →
∀𝑠 ∈ 𝒫
𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶))) |
60 | 59 | imp 444 |
. . . 4
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) →
∀𝑠 ∈ 𝒫
𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) |
61 | | isacs3 16997 |
. . . 4
⊢ (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶))) |
62 | 55, 60, 61 | sylanbrc 695 |
. . 3
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) → 𝐶 ∈ (ACS‘𝑋)) |
63 | 10 | mrcid 16096 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡 ∈ 𝐶) → ((mrCls‘𝐶)‘𝑡) = 𝑡) |
64 | 63 | adantlr 747 |
. . . . . . . . 9
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) ∧ 𝑡 ∈ 𝐶) → ((mrCls‘𝐶)‘𝑡) = 𝑡) |
65 | 62 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) ∧ 𝑡 ∈ 𝐶) → 𝐶 ∈ (ACS‘𝑋)) |
66 | | mress 16076 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡 ∈ 𝐶) → 𝑡 ⊆ 𝑋) |
67 | 66 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) ∧ 𝑡 ∈ 𝐶) → 𝑡 ⊆ 𝑋) |
68 | 65, 10, 67 | acsficld 16998 |
. . . . . . . . 9
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) ∧ 𝑡 ∈ 𝐶) → ((mrCls‘𝐶)‘𝑡) = ∪
((mrCls‘𝐶) “
(𝒫 𝑡 ∩
Fin))) |
69 | 64, 68 | eqtr3d 2646 |
. . . . . . . 8
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) ∧ 𝑡 ∈ 𝐶) → 𝑡 = ∪
((mrCls‘𝐶) “
(𝒫 𝑡 ∩
Fin))) |
70 | 10 | mrcf 16092 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ (Moore‘𝑋) → (mrCls‘𝐶):𝒫 𝑋⟶𝐶) |
71 | | ffn 5958 |
. . . . . . . . . . . . 13
⊢
((mrCls‘𝐶):𝒫 𝑋⟶𝐶 → (mrCls‘𝐶) Fn 𝒫 𝑋) |
72 | 70, 71 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ (Moore‘𝑋) → (mrCls‘𝐶) Fn 𝒫 𝑋) |
73 | 72 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡 ∈ 𝐶) → (mrCls‘𝐶) Fn 𝒫 𝑋) |
74 | 10 | mrcss 16099 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑔 ⊆ ℎ ∧ ℎ ⊆ 𝑋) → ((mrCls‘𝐶)‘𝑔) ⊆ ((mrCls‘𝐶)‘ℎ)) |
75 | 74 | 3expb 1258 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ (𝑔 ⊆ ℎ ∧ ℎ ⊆ 𝑋)) → ((mrCls‘𝐶)‘𝑔) ⊆ ((mrCls‘𝐶)‘ℎ)) |
76 | 75 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡 ∈ 𝐶) ∧ (𝑔 ⊆ ℎ ∧ ℎ ⊆ 𝑋)) → ((mrCls‘𝐶)‘𝑔) ⊆ ((mrCls‘𝐶)‘ℎ)) |
77 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑡 ∈ V |
78 | | fpwipodrs 16987 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ V →
(toInc‘(𝒫 𝑡
∩ Fin)) ∈ Dirset) |
79 | 77, 78 | mp1i 13 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡 ∈ 𝐶) → (toInc‘(𝒫 𝑡 ∩ Fin)) ∈
Dirset) |
80 | | inss1 3795 |
. . . . . . . . . . . 12
⊢
(𝒫 𝑡 ∩
Fin) ⊆ 𝒫 𝑡 |
81 | | sspwb 4844 |
. . . . . . . . . . . . 13
⊢ (𝑡 ⊆ 𝑋 ↔ 𝒫 𝑡 ⊆ 𝒫 𝑋) |
82 | 66, 81 | sylib 207 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡 ∈ 𝐶) → 𝒫 𝑡 ⊆ 𝒫 𝑋) |
83 | 80, 82 | syl5ss 3579 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡 ∈ 𝐶) → (𝒫 𝑡 ∩ Fin) ⊆ 𝒫 𝑋) |
84 | | fvex 6113 |
. . . . . . . . . . . . 13
⊢
(mrCls‘𝐶)
∈ V |
85 | | imaexg 6995 |
. . . . . . . . . . . . 13
⊢
((mrCls‘𝐶)
∈ V → ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ∈ V) |
86 | 84, 85 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
((mrCls‘𝐶)
“ (𝒫 𝑡 ∩
Fin)) ∈ V |
87 | 86 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡 ∈ 𝐶) → ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ∈ V) |
88 | 73, 76, 79, 83, 87 | ipodrsima 16988 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡 ∈ 𝐶) → (toInc‘((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin))) ∈
Dirset) |
89 | 88 | adantlr 747 |
. . . . . . . . 9
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) ∧ 𝑡 ∈ 𝐶) → (toInc‘((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin))) ∈
Dirset) |
90 | | imassrn 5396 |
. . . . . . . . . . . . . 14
⊢
((mrCls‘𝐶)
“ (𝒫 𝑡 ∩
Fin)) ⊆ ran (mrCls‘𝐶) |
91 | | frn 5966 |
. . . . . . . . . . . . . . 15
⊢
((mrCls‘𝐶):𝒫 𝑋⟶𝐶 → ran (mrCls‘𝐶) ⊆ 𝐶) |
92 | 70, 91 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝐶 ∈ (Moore‘𝑋) → ran (mrCls‘𝐶) ⊆ 𝐶) |
93 | 90, 92 | syl5ss 3579 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ (Moore‘𝑋) → ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝐶) |
94 | 93 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡 ∈ 𝐶) → ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝐶) |
95 | 86 | elpw 4114 |
. . . . . . . . . . . 12
⊢
(((mrCls‘𝐶)
“ (𝒫 𝑡 ∩
Fin)) ∈ 𝒫 𝐶
↔ ((mrCls‘𝐶)
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝐶) |
96 | 94, 95 | sylibr 223 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡 ∈ 𝐶) → ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ∈ 𝒫 𝐶) |
97 | 96 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) ∧ 𝑡 ∈ 𝐶) → ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ∈ 𝒫 𝐶) |
98 | | simplr 788 |
. . . . . . . . . 10
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) ∧ 𝑡 ∈ 𝐶) → ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) |
99 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑠 = ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) →
(toInc‘𝑠) =
(toInc‘((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)))) |
100 | 99 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ (𝑠 = ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) →
((toInc‘𝑠) ∈
Dirset ↔ (toInc‘((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin))) ∈
Dirset)) |
101 | | unieq 4380 |
. . . . . . . . . . . . 13
⊢ (𝑠 = ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) → ∪ 𝑠 =
∪ ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin))) |
102 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑠 = ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) → 𝑠 = ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin))) |
103 | 101, 102 | eleq12d 2682 |
. . . . . . . . . . . 12
⊢ (𝑠 = ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) → (∪ 𝑠
∈ 𝑠 ↔ ∪ ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ∈ ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)))) |
104 | 100, 103 | imbi12d 333 |
. . . . . . . . . . 11
⊢ (𝑠 = ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) →
(((toInc‘𝑠) ∈
Dirset → ∪ 𝑠 ∈ 𝑠) ↔ ((toInc‘((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin))) ∈ Dirset
→ ∪ ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ∈ ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin))))) |
105 | 104 | rspcva 3280 |
. . . . . . . . . 10
⊢
((((mrCls‘𝐶)
“ (𝒫 𝑡 ∩
Fin)) ∈ 𝒫 𝐶
∧ ∀𝑠 ∈
𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) →
((toInc‘((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin))) ∈ Dirset → ∪ ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ∈ ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)))) |
106 | 97, 98, 105 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) ∧ 𝑡 ∈ 𝐶) → ((toInc‘((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin))) ∈ Dirset
→ ∪ ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ∈ ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)))) |
107 | 89, 106 | mpd 15 |
. . . . . . . 8
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) ∧ 𝑡 ∈ 𝐶) → ∪
((mrCls‘𝐶) “
(𝒫 𝑡 ∩ Fin))
∈ ((mrCls‘𝐶)
“ (𝒫 𝑡 ∩
Fin))) |
108 | 69, 107 | eqeltrd 2688 |
. . . . . . 7
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) ∧ 𝑡 ∈ 𝐶) → 𝑡 ∈ ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin))) |
109 | | fvelimab 6163 |
. . . . . . . . 9
⊢
(((mrCls‘𝐶) Fn
𝒫 𝑋 ∧
(𝒫 𝑡 ∩ Fin)
⊆ 𝒫 𝑋) →
(𝑡 ∈
((mrCls‘𝐶) “
(𝒫 𝑡 ∩ Fin))
↔ ∃𝑔 ∈
(𝒫 𝑡 ∩
Fin)((mrCls‘𝐶)‘𝑔) = 𝑡)) |
110 | 73, 83, 109 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡 ∈ 𝐶) → (𝑡 ∈ ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ↔ ∃𝑔 ∈ (𝒫 𝑡 ∩ Fin)((mrCls‘𝐶)‘𝑔) = 𝑡)) |
111 | 110 | adantlr 747 |
. . . . . . 7
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) ∧ 𝑡 ∈ 𝐶) → (𝑡 ∈ ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ↔ ∃𝑔 ∈ (𝒫 𝑡 ∩ Fin)((mrCls‘𝐶)‘𝑔) = 𝑡)) |
112 | 108, 111 | mpbid 221 |
. . . . . 6
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) ∧ 𝑡 ∈ 𝐶) → ∃𝑔 ∈ (𝒫 𝑡 ∩ Fin)((mrCls‘𝐶)‘𝑔) = 𝑡) |
113 | | eqcom 2617 |
. . . . . . 7
⊢ (𝑡 = ((mrCls‘𝐶)‘𝑔) ↔ ((mrCls‘𝐶)‘𝑔) = 𝑡) |
114 | 113 | rexbii 3023 |
. . . . . 6
⊢
(∃𝑔 ∈
(𝒫 𝑡 ∩
Fin)𝑡 = ((mrCls‘𝐶)‘𝑔) ↔ ∃𝑔 ∈ (𝒫 𝑡 ∩ Fin)((mrCls‘𝐶)‘𝑔) = 𝑡) |
115 | 112, 114 | sylibr 223 |
. . . . 5
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) ∧ 𝑡 ∈ 𝐶) → ∃𝑔 ∈ (𝒫 𝑡 ∩ Fin)𝑡 = ((mrCls‘𝐶)‘𝑔)) |
116 | 10 | mrefg2 36288 |
. . . . . 6
⊢ (𝐶 ∈ (Moore‘𝑋) → (∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑡 = ((mrCls‘𝐶)‘𝑔) ↔ ∃𝑔 ∈ (𝒫 𝑡 ∩ Fin)𝑡 = ((mrCls‘𝐶)‘𝑔))) |
117 | 116 | ad2antrr 758 |
. . . . 5
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) ∧ 𝑡 ∈ 𝐶) → (∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑡 = ((mrCls‘𝐶)‘𝑔) ↔ ∃𝑔 ∈ (𝒫 𝑡 ∩ Fin)𝑡 = ((mrCls‘𝐶)‘𝑔))) |
118 | 115, 117 | mpbird 246 |
. . . 4
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) ∧ 𝑡 ∈ 𝐶) → ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑡 = ((mrCls‘𝐶)‘𝑔)) |
119 | 118 | ralrimiva 2949 |
. . 3
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) →
∀𝑡 ∈ 𝐶 ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑡 = ((mrCls‘𝐶)‘𝑔)) |
120 | 10 | isnacs 36285 |
. . 3
⊢ (𝐶 ∈ (NoeACS‘𝑋) ↔ (𝐶 ∈ (ACS‘𝑋) ∧ ∀𝑡 ∈ 𝐶 ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑡 = ((mrCls‘𝐶)‘𝑔))) |
121 | 62, 119, 120 | sylanbrc 695 |
. 2
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) → 𝐶 ∈ (NoeACS‘𝑋)) |
122 | 54, 121 | impbii 198 |
1
⊢ (𝐶 ∈ (NoeACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠))) |