This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isacs4

Description: A closure system is algebraic iff closure commutes with directed unions. (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Hypothesis acsdrscl.f ⊢ 𝐹 = ( mrCls ‘ 𝐶 )
Assertion isacs4 ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ( 𝐹 ‘ ∪ 𝑠 ) = ∪ ( 𝐹 “ 𝑠 ) ) ) )

Proof

Step Hyp Ref Expression
1 acsdrscl.f ⊢ 𝐹 = ( mrCls ‘ 𝐶 )
2 isacs3lem ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑡 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑡 ) ∈ Dirset → ∪ 𝑡 ∈ 𝐶 ) ) )
3 1 isacs4lem ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑡 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑡 ) ∈ Dirset → ∪ 𝑡 ∈ 𝐶 ) ) → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ( 𝐹 ‘ ∪ 𝑠 ) = ∪ ( 𝐹 “ 𝑠 ) ) ) )
4 2 3 syl ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ( 𝐹 ‘ ∪ 𝑠 ) = ∪ ( 𝐹 “ 𝑠 ) ) ) )
5 1 isacs5lem ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ( 𝐹 ‘ ∪ 𝑠 ) = ∪ ( 𝐹 “ 𝑠 ) ) ) → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝐹 ‘ 𝑡 ) = ∪ ( 𝐹 “ ( 𝒫 𝑡 ∩ Fin ) ) ) )
6 1 isacs5 ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑡 ∈ 𝒫 𝑋 ( 𝐹 ‘ 𝑡 ) = ∪ ( 𝐹 “ ( 𝒫 𝑡 ∩ Fin ) ) ) )
7 5 6 sylibr ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ( 𝐹 ‘ ∪ 𝑠 ) = ∪ ( 𝐹 “ 𝑠 ) ) ) → 𝐶 ∈ ( ACS ‘ 𝑋 ) )
8 4 7 impbii ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ( 𝐹 ‘ ∪ 𝑠 ) = ∪ ( 𝐹 “ 𝑠 ) ) ) )