Step |
Hyp |
Ref |
Expression |
1 |
|
isacs3lem |
⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) ) ) |
2 |
|
eqid |
⊢ ( mrCls ‘ 𝐶 ) = ( mrCls ‘ 𝐶 ) |
3 |
2
|
isacs4lem |
⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) ) → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑡 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑡 ) ∈ Dirset → ( ( mrCls ‘ 𝐶 ) ‘ ∪ 𝑡 ) = ∪ ( ( mrCls ‘ 𝐶 ) “ 𝑡 ) ) ) ) |
4 |
2
|
isacs4 |
⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑡 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑡 ) ∈ Dirset → ( ( mrCls ‘ 𝐶 ) ‘ ∪ 𝑡 ) = ∪ ( ( mrCls ‘ 𝐶 ) “ 𝑡 ) ) ) ) |
5 |
3 4
|
sylibr |
⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) ) → 𝐶 ∈ ( ACS ‘ 𝑋 ) ) |
6 |
1 5
|
impbii |
⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) ) ) |