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

Metamath Proof Explorer

Theorem acsdrscl

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

Ref Expression
Hypothesis acsdrscl.f ⊢ 𝐹 = ( mrCls ‘ 𝐶 )
Assertion acsdrscl ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝒫 𝑋 ∧ ( toInc ‘ 𝑌 ) ∈ Dirset ) → ( 𝐹 ‘ ∪ 𝑌 ) = ∪ ( 𝐹 “ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 acsdrscl.f ⊢ 𝐹 = ( mrCls ‘ 𝐶 )
2 fveq2 ⊢ ( 𝑡 = 𝑌 → ( toInc ‘ 𝑡 ) = ( toInc ‘ 𝑌 ) )
3 2 eleq1d ⊢ ( 𝑡 = 𝑌 → ( ( toInc ‘ 𝑡 ) ∈ Dirset ↔ ( toInc ‘ 𝑌 ) ∈ Dirset ) )
4 unieq ⊢ ( 𝑡 = 𝑌 → ∪ 𝑡 = ∪ 𝑌 )
5 4 fveq2d ⊢ ( 𝑡 = 𝑌 → ( 𝐹 ‘ ∪ 𝑡 ) = ( 𝐹 ‘ ∪ 𝑌 ) )
6 imaeq2 ⊢ ( 𝑡 = 𝑌 → ( 𝐹 “ 𝑡 ) = ( 𝐹 “ 𝑌 ) )
7 6 unieqd ⊢ ( 𝑡 = 𝑌 → ∪ ( 𝐹 “ 𝑡 ) = ∪ ( 𝐹 “ 𝑌 ) )
8 5 7 eqeq12d ⊢ ( 𝑡 = 𝑌 → ( ( 𝐹 ‘ ∪ 𝑡 ) = ∪ ( 𝐹 “ 𝑡 ) ↔ ( 𝐹 ‘ ∪ 𝑌 ) = ∪ ( 𝐹 “ 𝑌 ) ) )
9 3 8 imbi12d ⊢ ( 𝑡 = 𝑌 → ( ( ( toInc ‘ 𝑡 ) ∈ Dirset → ( 𝐹 ‘ ∪ 𝑡 ) = ∪ ( 𝐹 “ 𝑡 ) ) ↔ ( ( toInc ‘ 𝑌 ) ∈ Dirset → ( 𝐹 ‘ ∪ 𝑌 ) = ∪ ( 𝐹 “ 𝑌 ) ) ) )
10 isacs3lem ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) ) )
11 1 isacs4lem ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) ) → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑡 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑡 ) ∈ Dirset → ( 𝐹 ‘ ∪ 𝑡 ) = ∪ ( 𝐹 “ 𝑡 ) ) ) )
12 10 11 syl ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑡 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑡 ) ∈ Dirset → ( 𝐹 ‘ ∪ 𝑡 ) = ∪ ( 𝐹 “ 𝑡 ) ) ) )
13 12 simprd ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ∀ 𝑡 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑡 ) ∈ Dirset → ( 𝐹 ‘ ∪ 𝑡 ) = ∪ ( 𝐹 “ 𝑡 ) ) )
14 13 adantr ⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝒫 𝑋 ) → ∀ 𝑡 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑡 ) ∈ Dirset → ( 𝐹 ‘ ∪ 𝑡 ) = ∪ ( 𝐹 “ 𝑡 ) ) )
15 elfvdm ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → 𝑋 ∈ dom ACS )
16 pwexg ⊢ ( 𝑋 ∈ dom ACS → 𝒫 𝑋 ∈ V )
17 elpw2g ⊢ ( 𝒫 𝑋 ∈ V → ( 𝑌 ∈ 𝒫 𝒫 𝑋 ↔ 𝑌 ⊆ 𝒫 𝑋 ) )
18 15 16 17 3syl ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝑌 ∈ 𝒫 𝒫 𝑋 ↔ 𝑌 ⊆ 𝒫 𝑋 ) )
19 18 biimpar ⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝒫 𝑋 ) → 𝑌 ∈ 𝒫 𝒫 𝑋 )
20 9 14 19 rspcdva ⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝒫 𝑋 ) → ( ( toInc ‘ 𝑌 ) ∈ Dirset → ( 𝐹 ‘ ∪ 𝑌 ) = ∪ ( 𝐹 “ 𝑌 ) ) )
21 20 3impia ⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝒫 𝑋 ∧ ( toInc ‘ 𝑌 ) ∈ Dirset ) → ( 𝐹 ‘ ∪ 𝑌 ) = ∪ ( 𝐹 “ 𝑌 ) )