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

Metamath Proof Explorer

Theorem acsdrsel

Description: An algebraic closure system contains all directed unions of closed sets. (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Assertion acsdrsel ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝐶 ∧ ( toInc ‘ 𝑌 ) ∈ Dirset ) → ∪ 𝑌 ∈ 𝐶 )

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ ( 𝑠 = 𝑌 → ( toInc ‘ 𝑠 ) = ( toInc ‘ 𝑌 ) )
2 1 eleq1d ⊢ ( 𝑠 = 𝑌 → ( ( toInc ‘ 𝑠 ) ∈ Dirset ↔ ( toInc ‘ 𝑌 ) ∈ Dirset ) )
3 unieq ⊢ ( 𝑠 = 𝑌 → ∪ 𝑠 = ∪ 𝑌 )
4 3 eleq1d ⊢ ( 𝑠 = 𝑌 → ( ∪ 𝑠 ∈ 𝐶 ↔ ∪ 𝑌 ∈ 𝐶 ) )
5 2 4 imbi12d ⊢ ( 𝑠 = 𝑌 → ( ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) ↔ ( ( toInc ‘ 𝑌 ) ∈ Dirset → ∪ 𝑌 ∈ 𝐶 ) ) )
6 isacs3lem ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) ) )
7 6 simprd ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) )
8 7 adantr ⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝐶 ) → ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) )
9 elpw2g ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝑌 ∈ 𝒫 𝐶 ↔ 𝑌 ⊆ 𝐶 ) )
10 9 biimpar ⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝐶 ) → 𝑌 ∈ 𝒫 𝐶 )
11 5 8 10 rspcdva ⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝐶 ) → ( ( toInc ‘ 𝑌 ) ∈ Dirset → ∪ 𝑌 ∈ 𝐶 ) )
12 11 3impia ⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝐶 ∧ ( toInc ‘ 𝑌 ) ∈ Dirset ) → ∪ 𝑌 ∈ 𝐶 )