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 ) → ( 𝐹 ‘ ∪ 𝑌 ) = ∪ ( 𝐹 “ 𝑌 ) )