| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nacsacs 42725 | . . . 4
⊢ (𝐶 ∈ (NoeACS‘𝑋) → 𝐶 ∈ (ACS‘𝑋)) | 
| 2 | 1 | acsmred 17700 | . . 3
⊢ (𝐶 ∈ (NoeACS‘𝑋) → 𝐶 ∈ (Moore‘𝑋)) | 
| 3 |  | simpll 766 | . . . . . . . 8
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → 𝐶 ∈ (NoeACS‘𝑋)) | 
| 4 | 1 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → 𝐶 ∈ (ACS‘𝑋)) | 
| 5 |  | elpwi 4606 | . . . . . . . . . 10
⊢ (𝑠 ∈ 𝒫 𝐶 → 𝑠 ⊆ 𝐶) | 
| 6 | 5 | ad2antlr 727 | . . . . . . . . 9
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → 𝑠 ⊆ 𝐶) | 
| 7 |  | simpr 484 | . . . . . . . . 9
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → (toInc‘𝑠) ∈
Dirset) | 
| 8 |  | acsdrsel 18589 | . . . . . . . . 9
⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠 ⊆ 𝐶 ∧ (toInc‘𝑠) ∈ Dirset) → ∪ 𝑠
∈ 𝐶) | 
| 9 | 4, 6, 7, 8 | syl3anc 1372 | . . . . . . . 8
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → ∪ 𝑠
∈ 𝐶) | 
| 10 |  | eqid 2736 | . . . . . . . . 9
⊢
(mrCls‘𝐶) =
(mrCls‘𝐶) | 
| 11 | 10 | nacsfg 42721 | . . . . . . . 8
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ ∪ 𝑠
∈ 𝐶) →
∃𝑔 ∈ (𝒫
𝑋 ∩ Fin)∪ 𝑠 =
((mrCls‘𝐶)‘𝑔)) | 
| 12 | 3, 9, 11 | syl2anc 584 | . . . . . . 7
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑠 =
((mrCls‘𝐶)‘𝑔)) | 
| 13 | 10 | mrefg2 42723 | . . . . . . . . 9
⊢ (𝐶 ∈ (Moore‘𝑋) → (∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑠 =
((mrCls‘𝐶)‘𝑔) ↔ ∃𝑔 ∈ (𝒫 ∪ 𝑠
∩ Fin)∪ 𝑠 = ((mrCls‘𝐶)‘𝑔))) | 
| 14 | 2, 13 | syl 17 | . . . . . . . 8
⊢ (𝐶 ∈ (NoeACS‘𝑋) → (∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑠 =
((mrCls‘𝐶)‘𝑔) ↔ ∃𝑔 ∈ (𝒫 ∪ 𝑠
∩ Fin)∪ 𝑠 = ((mrCls‘𝐶)‘𝑔))) | 
| 15 | 14 | ad2antrr 726 | . . . . . . 7
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → (∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑠 =
((mrCls‘𝐶)‘𝑔) ↔ ∃𝑔 ∈ (𝒫 ∪ 𝑠
∩ Fin)∪ 𝑠 = ((mrCls‘𝐶)‘𝑔))) | 
| 16 | 12, 15 | mpbid 232 | . . . . . 6
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → ∃𝑔 ∈ (𝒫 ∪ 𝑠
∩ Fin)∪ 𝑠 = ((mrCls‘𝐶)‘𝑔)) | 
| 17 |  | elfpw 9395 | . . . . . . . . 9
⊢ (𝑔 ∈ (𝒫 ∪ 𝑠
∩ Fin) ↔ (𝑔
⊆ ∪ 𝑠 ∧ 𝑔 ∈ Fin)) | 
| 18 |  | fissuni 9398 | . . . . . . . . 9
⊢ ((𝑔 ⊆ ∪ 𝑠
∧ 𝑔 ∈ Fin) →
∃ℎ ∈ (𝒫
𝑠 ∩ Fin)𝑔 ⊆ ∪ ℎ) | 
| 19 | 17, 18 | sylbi 217 | . . . . . . . 8
⊢ (𝑔 ∈ (𝒫 ∪ 𝑠
∩ Fin) → ∃ℎ
∈ (𝒫 𝑠 ∩
Fin)𝑔 ⊆ ∪ ℎ) | 
| 20 |  | elfpw 9395 | . . . . . . . . . . . 12
⊢ (ℎ ∈ (𝒫 𝑠 ∩ Fin) ↔ (ℎ ⊆ 𝑠 ∧ ℎ ∈ Fin)) | 
| 21 |  | ipodrsfi 18585 | . . . . . . . . . . . . 13
⊢
(((toInc‘𝑠)
∈ Dirset ∧ ℎ
⊆ 𝑠 ∧ ℎ ∈ Fin) → ∃𝑖 ∈ 𝑠 ∪ ℎ ⊆ 𝑖) | 
| 22 | 21 | 3expb 1120 | . . . . . . . . . . . 12
⊢
(((toInc‘𝑠)
∈ Dirset ∧ (ℎ
⊆ 𝑠 ∧ ℎ ∈ Fin)) → ∃𝑖 ∈ 𝑠 ∪ ℎ ⊆ 𝑖) | 
| 23 | 20, 22 | sylan2b 594 | . . . . . . . . . . 11
⊢
(((toInc‘𝑠)
∈ Dirset ∧ ℎ ∈
(𝒫 𝑠 ∩ Fin))
→ ∃𝑖 ∈
𝑠 ∪ ℎ
⊆ 𝑖) | 
| 24 |  | sstr 3991 | . . . . . . . . . . . . . . 15
⊢ ((𝑔 ⊆ ∪ ℎ
∧ ∪ ℎ ⊆ 𝑖) → 𝑔 ⊆ 𝑖) | 
| 25 | 24 | ancoms 458 | . . . . . . . . . . . . . 14
⊢ ((∪ ℎ
⊆ 𝑖 ∧ 𝑔 ⊆ ∪ ℎ)
→ 𝑔 ⊆ 𝑖) | 
| 26 |  | simpr 484 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖 ∈ 𝑠 ∧ 𝑔 ⊆ 𝑖)) ∧ ∪ 𝑠 = ((mrCls‘𝐶)‘𝑔)) → ∪ 𝑠 = ((mrCls‘𝐶)‘𝑔)) | 
| 27 | 2 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖 ∈ 𝑠 ∧ 𝑔 ⊆ 𝑖)) → 𝐶 ∈ (Moore‘𝑋)) | 
| 28 |  | simprr 772 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖 ∈ 𝑠 ∧ 𝑔 ⊆ 𝑖)) → 𝑔 ⊆ 𝑖) | 
| 29 | 5 | ad2antlr 727 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖 ∈ 𝑠 ∧ 𝑔 ⊆ 𝑖)) → 𝑠 ⊆ 𝐶) | 
| 30 |  | simprl 770 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖 ∈ 𝑠 ∧ 𝑔 ⊆ 𝑖)) → 𝑖 ∈ 𝑠) | 
| 31 | 29, 30 | sseldd 3983 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖 ∈ 𝑠 ∧ 𝑔 ⊆ 𝑖)) → 𝑖 ∈ 𝐶) | 
| 32 | 10 | mrcsscl 17664 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑔 ⊆ 𝑖 ∧ 𝑖 ∈ 𝐶) → ((mrCls‘𝐶)‘𝑔) ⊆ 𝑖) | 
| 33 | 27, 28, 31, 32 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖 ∈ 𝑠 ∧ 𝑔 ⊆ 𝑖)) → ((mrCls‘𝐶)‘𝑔) ⊆ 𝑖) | 
| 34 | 33 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖 ∈ 𝑠 ∧ 𝑔 ⊆ 𝑖)) ∧ ∪ 𝑠 = ((mrCls‘𝐶)‘𝑔)) → ((mrCls‘𝐶)‘𝑔) ⊆ 𝑖) | 
| 35 | 26, 34 | eqsstrd 4017 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖 ∈ 𝑠 ∧ 𝑔 ⊆ 𝑖)) ∧ ∪ 𝑠 = ((mrCls‘𝐶)‘𝑔)) → ∪ 𝑠 ⊆ 𝑖) | 
| 36 |  | simplrl 776 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖 ∈ 𝑠 ∧ 𝑔 ⊆ 𝑖)) ∧ ∪ 𝑠 = ((mrCls‘𝐶)‘𝑔)) → 𝑖 ∈ 𝑠) | 
| 37 |  | elssuni 4936 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ 𝑠 → 𝑖 ⊆ ∪ 𝑠) | 
| 38 | 36, 37 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖 ∈ 𝑠 ∧ 𝑔 ⊆ 𝑖)) ∧ ∪ 𝑠 = ((mrCls‘𝐶)‘𝑔)) → 𝑖 ⊆ ∪ 𝑠) | 
| 39 | 35, 38 | eqssd 4000 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖 ∈ 𝑠 ∧ 𝑔 ⊆ 𝑖)) ∧ ∪ 𝑠 = ((mrCls‘𝐶)‘𝑔)) → ∪ 𝑠 = 𝑖) | 
| 40 | 39, 36 | eqeltrd 2840 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖 ∈ 𝑠 ∧ 𝑔 ⊆ 𝑖)) ∧ ∪ 𝑠 = ((mrCls‘𝐶)‘𝑔)) → ∪ 𝑠 ∈ 𝑠) | 
| 41 | 40 | ex 412 | . . . . . . . . . . . . . . 15
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖 ∈ 𝑠 ∧ 𝑔 ⊆ 𝑖)) → (∪ 𝑠 = ((mrCls‘𝐶)‘𝑔) → ∪ 𝑠 ∈ 𝑠)) | 
| 42 | 41 | expr 456 | . . . . . . . . . . . . . 14
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ 𝑖 ∈ 𝑠) → (𝑔 ⊆ 𝑖 → (∪ 𝑠 = ((mrCls‘𝐶)‘𝑔) → ∪ 𝑠 ∈ 𝑠))) | 
| 43 | 25, 42 | syl5 34 | . . . . . . . . . . . . 13
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ 𝑖 ∈ 𝑠) → ((∪ ℎ ⊆ 𝑖 ∧ 𝑔 ⊆ ∪ ℎ) → (∪ 𝑠 =
((mrCls‘𝐶)‘𝑔) → ∪ 𝑠 ∈ 𝑠))) | 
| 44 | 43 | expd 415 | . . . . . . . . . . . 12
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ 𝑖 ∈ 𝑠) → (∪ ℎ ⊆ 𝑖 → (𝑔 ⊆ ∪ ℎ → (∪ 𝑠 =
((mrCls‘𝐶)‘𝑔) → ∪ 𝑠 ∈ 𝑠)))) | 
| 45 | 44 | rexlimdva 3154 | . . . . . . . . . . 11
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) → (∃𝑖 ∈ 𝑠 ∪ ℎ ⊆ 𝑖 → (𝑔 ⊆ ∪ ℎ → (∪ 𝑠 =
((mrCls‘𝐶)‘𝑔) → ∪ 𝑠 ∈ 𝑠)))) | 
| 46 | 23, 45 | syl5 34 | . . . . . . . . . 10
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) → (((toInc‘𝑠) ∈ Dirset ∧ ℎ ∈ (𝒫 𝑠 ∩ Fin)) → (𝑔 ⊆ ∪ ℎ → (∪ 𝑠 =
((mrCls‘𝐶)‘𝑔) → ∪ 𝑠 ∈ 𝑠)))) | 
| 47 | 46 | expdimp 452 | . . . . . . . . 9
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → (ℎ ∈ (𝒫 𝑠 ∩ Fin) → (𝑔 ⊆ ∪ ℎ → (∪ 𝑠 =
((mrCls‘𝐶)‘𝑔) → ∪ 𝑠 ∈ 𝑠)))) | 
| 48 | 47 | rexlimdv 3152 | . . . . . . . 8
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → (∃ℎ ∈ (𝒫 𝑠 ∩ Fin)𝑔 ⊆ ∪ ℎ → (∪ 𝑠 =
((mrCls‘𝐶)‘𝑔) → ∪ 𝑠 ∈ 𝑠))) | 
| 49 | 19, 48 | syl5 34 | . . . . . . 7
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → (𝑔 ∈ (𝒫 ∪ 𝑠
∩ Fin) → (∪ 𝑠 = ((mrCls‘𝐶)‘𝑔) → ∪ 𝑠 ∈ 𝑠))) | 
| 50 | 49 | rexlimdv 3152 | . . . . . 6
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → (∃𝑔 ∈ (𝒫 ∪ 𝑠
∩ Fin)∪ 𝑠 = ((mrCls‘𝐶)‘𝑔) → ∪ 𝑠 ∈ 𝑠)) | 
| 51 | 16, 50 | mpd 15 | . . . . 5
⊢ (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → ∪ 𝑠
∈ 𝑠) | 
| 52 | 51 | ex 412 | . . . 4
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) → ((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) | 
| 53 | 52 | ralrimiva 3145 | . . 3
⊢ (𝐶 ∈ (NoeACS‘𝑋) → ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) | 
| 54 | 2, 53 | jca 511 | . 2
⊢ (𝐶 ∈ (NoeACS‘𝑋) → (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠))) | 
| 55 |  | simpl 482 | . . . 4
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) → 𝐶 ∈ (Moore‘𝑋)) | 
| 56 | 5 | adantl 481 | . . . . . . . 8
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) → 𝑠 ⊆ 𝐶) | 
| 57 | 56 | sseld 3981 | . . . . . . 7
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) → (∪ 𝑠 ∈ 𝑠 → ∪ 𝑠 ∈ 𝐶)) | 
| 58 | 57 | imim2d 57 | . . . . . 6
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) → (((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠) →
((toInc‘𝑠) ∈
Dirset → ∪ 𝑠 ∈ 𝐶))) | 
| 59 | 58 | ralimdva 3166 | . . . . 5
⊢ (𝐶 ∈ (Moore‘𝑋) → (∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠) →
∀𝑠 ∈ 𝒫
𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶))) | 
| 60 | 59 | imp 406 | . . . 4
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) →
∀𝑠 ∈ 𝒫
𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) | 
| 61 |  | isacs3 18596 | . . . 4
⊢ (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶))) | 
| 62 | 55, 60, 61 | sylanbrc 583 | . . 3
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) → 𝐶 ∈ (ACS‘𝑋)) | 
| 63 | 10 | mrcid 17657 | . . . . . . . . . 10
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡 ∈ 𝐶) → ((mrCls‘𝐶)‘𝑡) = 𝑡) | 
| 64 | 63 | adantlr 715 | . . . . . . . . 9
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) ∧ 𝑡 ∈ 𝐶) → ((mrCls‘𝐶)‘𝑡) = 𝑡) | 
| 65 | 62 | adantr 480 | . . . . . . . . . 10
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) ∧ 𝑡 ∈ 𝐶) → 𝐶 ∈ (ACS‘𝑋)) | 
| 66 |  | mress 17637 | . . . . . . . . . . 11
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡 ∈ 𝐶) → 𝑡 ⊆ 𝑋) | 
| 67 | 66 | adantlr 715 | . . . . . . . . . 10
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) ∧ 𝑡 ∈ 𝐶) → 𝑡 ⊆ 𝑋) | 
| 68 | 65, 10, 67 | acsficld 18597 | . . . . . . . . 9
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) ∧ 𝑡 ∈ 𝐶) → ((mrCls‘𝐶)‘𝑡) = ∪
((mrCls‘𝐶) “
(𝒫 𝑡 ∩
Fin))) | 
| 69 | 64, 68 | eqtr3d 2778 | . . . . . . . 8
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) ∧ 𝑡 ∈ 𝐶) → 𝑡 = ∪
((mrCls‘𝐶) “
(𝒫 𝑡 ∩
Fin))) | 
| 70 | 10 | mrcf 17653 | . . . . . . . . . . . . 13
⊢ (𝐶 ∈ (Moore‘𝑋) → (mrCls‘𝐶):𝒫 𝑋⟶𝐶) | 
| 71 | 70 | ffnd 6736 | . . . . . . . . . . . 12
⊢ (𝐶 ∈ (Moore‘𝑋) → (mrCls‘𝐶) Fn 𝒫 𝑋) | 
| 72 | 71 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡 ∈ 𝐶) → (mrCls‘𝐶) Fn 𝒫 𝑋) | 
| 73 | 10 | mrcss 17660 | . . . . . . . . . . . . 13
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑔 ⊆ ℎ ∧ ℎ ⊆ 𝑋) → ((mrCls‘𝐶)‘𝑔) ⊆ ((mrCls‘𝐶)‘ℎ)) | 
| 74 | 73 | 3expb 1120 | . . . . . . . . . . . 12
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ (𝑔 ⊆ ℎ ∧ ℎ ⊆ 𝑋)) → ((mrCls‘𝐶)‘𝑔) ⊆ ((mrCls‘𝐶)‘ℎ)) | 
| 75 | 74 | adantlr 715 | . . . . . . . . . . 11
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡 ∈ 𝐶) ∧ (𝑔 ⊆ ℎ ∧ ℎ ⊆ 𝑋)) → ((mrCls‘𝐶)‘𝑔) ⊆ ((mrCls‘𝐶)‘ℎ)) | 
| 76 |  | vex 3483 | . . . . . . . . . . . 12
⊢ 𝑡 ∈ V | 
| 77 |  | fpwipodrs 18586 | . . . . . . . . . . . 12
⊢ (𝑡 ∈ V →
(toInc‘(𝒫 𝑡
∩ Fin)) ∈ Dirset) | 
| 78 | 76, 77 | mp1i 13 | . . . . . . . . . . 11
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡 ∈ 𝐶) → (toInc‘(𝒫 𝑡 ∩ Fin)) ∈
Dirset) | 
| 79 |  | inss1 4236 | . . . . . . . . . . . 12
⊢
(𝒫 𝑡 ∩
Fin) ⊆ 𝒫 𝑡 | 
| 80 | 66 | sspwd 4612 | . . . . . . . . . . . 12
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡 ∈ 𝐶) → 𝒫 𝑡 ⊆ 𝒫 𝑋) | 
| 81 | 79, 80 | sstrid 3994 | . . . . . . . . . . 11
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡 ∈ 𝐶) → (𝒫 𝑡 ∩ Fin) ⊆ 𝒫 𝑋) | 
| 82 |  | fvex 6918 | . . . . . . . . . . . . 13
⊢
(mrCls‘𝐶)
∈ V | 
| 83 |  | imaexg 7936 | . . . . . . . . . . . . 13
⊢
((mrCls‘𝐶)
∈ V → ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ∈ V) | 
| 84 | 82, 83 | ax-mp 5 | . . . . . . . . . . . 12
⊢
((mrCls‘𝐶)
“ (𝒫 𝑡 ∩
Fin)) ∈ V | 
| 85 | 84 | a1i 11 | . . . . . . . . . . 11
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡 ∈ 𝐶) → ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ∈ V) | 
| 86 | 72, 75, 78, 81, 85 | ipodrsima 18587 | . . . . . . . . . 10
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡 ∈ 𝐶) → (toInc‘((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin))) ∈
Dirset) | 
| 87 | 86 | adantlr 715 | . . . . . . . . 9
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) ∧ 𝑡 ∈ 𝐶) → (toInc‘((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin))) ∈
Dirset) | 
| 88 |  | imassrn 6088 | . . . . . . . . . . . . . 14
⊢
((mrCls‘𝐶)
“ (𝒫 𝑡 ∩
Fin)) ⊆ ran (mrCls‘𝐶) | 
| 89 | 70 | frnd 6743 | . . . . . . . . . . . . . 14
⊢ (𝐶 ∈ (Moore‘𝑋) → ran (mrCls‘𝐶) ⊆ 𝐶) | 
| 90 | 88, 89 | sstrid 3994 | . . . . . . . . . . . . 13
⊢ (𝐶 ∈ (Moore‘𝑋) → ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝐶) | 
| 91 | 90 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡 ∈ 𝐶) → ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝐶) | 
| 92 | 84 | elpw 4603 | . . . . . . . . . . . 12
⊢
(((mrCls‘𝐶)
“ (𝒫 𝑡 ∩
Fin)) ∈ 𝒫 𝐶
↔ ((mrCls‘𝐶)
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝐶) | 
| 93 | 91, 92 | sylibr 234 | . . . . . . . . . . 11
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡 ∈ 𝐶) → ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ∈ 𝒫 𝐶) | 
| 94 | 93 | adantlr 715 | . . . . . . . . . 10
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) ∧ 𝑡 ∈ 𝐶) → ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ∈ 𝒫 𝐶) | 
| 95 |  | simplr 768 | . . . . . . . . . 10
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) ∧ 𝑡 ∈ 𝐶) → ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) | 
| 96 |  | fveq2 6905 | . . . . . . . . . . . . 13
⊢ (𝑠 = ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) →
(toInc‘𝑠) =
(toInc‘((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)))) | 
| 97 | 96 | eleq1d 2825 | . . . . . . . . . . . 12
⊢ (𝑠 = ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) →
((toInc‘𝑠) ∈
Dirset ↔ (toInc‘((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin))) ∈
Dirset)) | 
| 98 |  | unieq 4917 | . . . . . . . . . . . . 13
⊢ (𝑠 = ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) → ∪ 𝑠 =
∪ ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin))) | 
| 99 |  | id 22 | . . . . . . . . . . . . 13
⊢ (𝑠 = ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) → 𝑠 = ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin))) | 
| 100 | 98, 99 | eleq12d 2834 | . . . . . . . . . . . 12
⊢ (𝑠 = ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) → (∪ 𝑠
∈ 𝑠 ↔ ∪ ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ∈ ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)))) | 
| 101 | 97, 100 | imbi12d 344 | . . . . . . . . . . 11
⊢ (𝑠 = ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) →
(((toInc‘𝑠) ∈
Dirset → ∪ 𝑠 ∈ 𝑠) ↔ ((toInc‘((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin))) ∈ Dirset
→ ∪ ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ∈ ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin))))) | 
| 102 | 101 | rspcva 3619 | . . . . . . . . . 10
⊢
((((mrCls‘𝐶)
“ (𝒫 𝑡 ∩
Fin)) ∈ 𝒫 𝐶
∧ ∀𝑠 ∈
𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) →
((toInc‘((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin))) ∈ Dirset → ∪ ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ∈ ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)))) | 
| 103 | 94, 95, 102 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) ∧ 𝑡 ∈ 𝐶) → ((toInc‘((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin))) ∈ Dirset
→ ∪ ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ∈ ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)))) | 
| 104 | 87, 103 | mpd 15 | . . . . . . . 8
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) ∧ 𝑡 ∈ 𝐶) → ∪
((mrCls‘𝐶) “
(𝒫 𝑡 ∩ Fin))
∈ ((mrCls‘𝐶)
“ (𝒫 𝑡 ∩
Fin))) | 
| 105 | 69, 104 | eqeltrd 2840 | . . . . . . 7
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) ∧ 𝑡 ∈ 𝐶) → 𝑡 ∈ ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin))) | 
| 106 |  | fvelimab 6980 | . . . . . . . . 9
⊢
(((mrCls‘𝐶) Fn
𝒫 𝑋 ∧
(𝒫 𝑡 ∩ Fin)
⊆ 𝒫 𝑋) →
(𝑡 ∈
((mrCls‘𝐶) “
(𝒫 𝑡 ∩ Fin))
↔ ∃𝑔 ∈
(𝒫 𝑡 ∩
Fin)((mrCls‘𝐶)‘𝑔) = 𝑡)) | 
| 107 | 72, 81, 106 | syl2anc 584 | . . . . . . . 8
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡 ∈ 𝐶) → (𝑡 ∈ ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ↔ ∃𝑔 ∈ (𝒫 𝑡 ∩ Fin)((mrCls‘𝐶)‘𝑔) = 𝑡)) | 
| 108 | 107 | adantlr 715 | . . . . . . 7
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) ∧ 𝑡 ∈ 𝐶) → (𝑡 ∈ ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ↔ ∃𝑔 ∈ (𝒫 𝑡 ∩ Fin)((mrCls‘𝐶)‘𝑔) = 𝑡)) | 
| 109 | 105, 108 | mpbid 232 | . . . . . 6
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) ∧ 𝑡 ∈ 𝐶) → ∃𝑔 ∈ (𝒫 𝑡 ∩ Fin)((mrCls‘𝐶)‘𝑔) = 𝑡) | 
| 110 |  | eqcom 2743 | . . . . . . 7
⊢ (𝑡 = ((mrCls‘𝐶)‘𝑔) ↔ ((mrCls‘𝐶)‘𝑔) = 𝑡) | 
| 111 | 110 | rexbii 3093 | . . . . . 6
⊢
(∃𝑔 ∈
(𝒫 𝑡 ∩
Fin)𝑡 = ((mrCls‘𝐶)‘𝑔) ↔ ∃𝑔 ∈ (𝒫 𝑡 ∩ Fin)((mrCls‘𝐶)‘𝑔) = 𝑡) | 
| 112 | 109, 111 | sylibr 234 | . . . . 5
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) ∧ 𝑡 ∈ 𝐶) → ∃𝑔 ∈ (𝒫 𝑡 ∩ Fin)𝑡 = ((mrCls‘𝐶)‘𝑔)) | 
| 113 | 10 | mrefg2 42723 | . . . . . 6
⊢ (𝐶 ∈ (Moore‘𝑋) → (∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑡 = ((mrCls‘𝐶)‘𝑔) ↔ ∃𝑔 ∈ (𝒫 𝑡 ∩ Fin)𝑡 = ((mrCls‘𝐶)‘𝑔))) | 
| 114 | 113 | ad2antrr 726 | . . . . 5
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) ∧ 𝑡 ∈ 𝐶) → (∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑡 = ((mrCls‘𝐶)‘𝑔) ↔ ∃𝑔 ∈ (𝒫 𝑡 ∩ Fin)𝑡 = ((mrCls‘𝐶)‘𝑔))) | 
| 115 | 112, 114 | mpbird 257 | . . . 4
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) ∧ 𝑡 ∈ 𝐶) → ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑡 = ((mrCls‘𝐶)‘𝑔)) | 
| 116 | 115 | ralrimiva 3145 | . . 3
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) →
∀𝑡 ∈ 𝐶 ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑡 = ((mrCls‘𝐶)‘𝑔)) | 
| 117 | 10 | isnacs 42720 | . . 3
⊢ (𝐶 ∈ (NoeACS‘𝑋) ↔ (𝐶 ∈ (ACS‘𝑋) ∧ ∀𝑡 ∈ 𝐶 ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑡 = ((mrCls‘𝐶)‘𝑔))) | 
| 118 | 62, 116, 117 | sylanbrc 583 | . 2
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠)) → 𝐶 ∈ (NoeACS‘𝑋)) | 
| 119 | 54, 118 | impbii 209 | 1
⊢ (𝐶 ∈ (NoeACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝑠))) |