Theorem acsfiel

Description: A set is closed in an algebraic closure system iff it contains all closures of finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015)

	Ref	Expression
Hypothesis	isacs2.f	⊢ 𝐹 = ( mrCls ‘ 𝐶 )
Assertion	acsfiel	⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝑆 ∈ 𝐶 ↔ ( 𝑆 ⊆ 𝑋 ∧ ∀ 𝑦 ∈ ( 𝒫 𝑆 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑆 ) ) )

Proof

Step	Hyp	Ref	Expression
1		isacs2.f	⊢ 𝐹 = ( mrCls ‘ 𝐶 )
2		acsmre	⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) )
3		mress	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ∈ 𝐶 ) → 𝑆 ⊆ 𝑋 )
4	2 3	sylan	⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑆 ∈ 𝐶 ) → 𝑆 ⊆ 𝑋 )
5	4	ex	⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝑆 ∈ 𝐶 → 𝑆 ⊆ 𝑋 ) )
6	5	pm4.71rd	⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝑆 ∈ 𝐶 ↔ ( 𝑆 ⊆ 𝑋 ∧ 𝑆 ∈ 𝐶 ) ) )
7		eleq1	⊢ ( 𝑠 = 𝑆 → ( 𝑠 ∈ 𝐶 ↔ 𝑆 ∈ 𝐶 ) )
8		pweq	⊢ ( 𝑠 = 𝑆 → 𝒫 𝑠 = 𝒫 𝑆 )
9	8	ineq1d	⊢ ( 𝑠 = 𝑆 → ( 𝒫 𝑠 ∩ Fin ) = ( 𝒫 𝑆 ∩ Fin ) )
10		sseq2	⊢ ( 𝑠 = 𝑆 → ( ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ↔ ( 𝐹 ‘ 𝑦 ) ⊆ 𝑆 ) )
11	9 10	raleqbidv	⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑆 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑆 ) )
12	7 11	bibi12d	⊢ ( 𝑠 = 𝑆 → ( ( 𝑠 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ) ↔ ( 𝑆 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑆 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑆 ) ) )
13	1	isacs2	⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ) ) )
14	13	simprbi	⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ) )
15	14	adantr	⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑠 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑠 ) )
16		elfvdm	⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → 𝑋 ∈ dom ACS )
17		elpw2g	⊢ ( 𝑋 ∈ dom ACS → ( 𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋 ) )
18	16 17	syl	⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋 ) )
19	18	biimpar	⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 ∈ 𝒫 𝑋 )
20	12 15 19	rspcdva	⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑆 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑆 ) )
21	20	pm5.32da	⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( ( 𝑆 ⊆ 𝑋 ∧ 𝑆 ∈ 𝐶 ) ↔ ( 𝑆 ⊆ 𝑋 ∧ ∀ 𝑦 ∈ ( 𝒫 𝑆 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑆 ) ) )
22	6 21	bitrd	⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝑆 ∈ 𝐶 ↔ ( 𝑆 ⊆ 𝑋 ∧ ∀ 𝑦 ∈ ( 𝒫 𝑆 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑆 ) ) )