Theorem acsfn1c

Description: Algebraicity of a one-argument closure condition with additional constant. (Contributed by Stefan O'Rear, 3-Apr-2015)

	Ref	Expression
Assertion	acsfn1c	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑏 ∈ 𝐾 ∀ 𝑐 ∈ 𝑋 𝐸 ∈ 𝑋 ) → { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑏 ∈ 𝐾 ∀ 𝑐 ∈ 𝑎 𝐸 ∈ 𝑎 } ∈ ( ACS ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		riinrab	⊢ ( 𝒫 𝑋 ∩ ∩ 𝑏 ∈ 𝐾 { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑐 ∈ 𝑎 𝐸 ∈ 𝑎 } ) = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑏 ∈ 𝐾 ∀ 𝑐 ∈ 𝑎 𝐸 ∈ 𝑎 }
2		mreacs	⊢ ( 𝑋 ∈ 𝑉 → ( ACS ‘ 𝑋 ) ∈ ( Moore ‘ 𝒫 𝑋 ) )
3		acsfn1	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑐 ∈ 𝑋 𝐸 ∈ 𝑋 ) → { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑐 ∈ 𝑎 𝐸 ∈ 𝑎 } ∈ ( ACS ‘ 𝑋 ) )
4	3	ex	⊢ ( 𝑋 ∈ 𝑉 → ( ∀ 𝑐 ∈ 𝑋 𝐸 ∈ 𝑋 → { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑐 ∈ 𝑎 𝐸 ∈ 𝑎 } ∈ ( ACS ‘ 𝑋 ) ) )
5	4	ralimdv	⊢ ( 𝑋 ∈ 𝑉 → ( ∀ 𝑏 ∈ 𝐾 ∀ 𝑐 ∈ 𝑋 𝐸 ∈ 𝑋 → ∀ 𝑏 ∈ 𝐾 { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑐 ∈ 𝑎 𝐸 ∈ 𝑎 } ∈ ( ACS ‘ 𝑋 ) ) )
6	5	imp	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑏 ∈ 𝐾 ∀ 𝑐 ∈ 𝑋 𝐸 ∈ 𝑋 ) → ∀ 𝑏 ∈ 𝐾 { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑐 ∈ 𝑎 𝐸 ∈ 𝑎 } ∈ ( ACS ‘ 𝑋 ) )
7		mreriincl	⊢ ( ( ( ACS ‘ 𝑋 ) ∈ ( Moore ‘ 𝒫 𝑋 ) ∧ ∀ 𝑏 ∈ 𝐾 { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑐 ∈ 𝑎 𝐸 ∈ 𝑎 } ∈ ( ACS ‘ 𝑋 ) ) → ( 𝒫 𝑋 ∩ ∩ 𝑏 ∈ 𝐾 { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑐 ∈ 𝑎 𝐸 ∈ 𝑎 } ) ∈ ( ACS ‘ 𝑋 ) )
8	2 6 7	syl2an2r	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑏 ∈ 𝐾 ∀ 𝑐 ∈ 𝑋 𝐸 ∈ 𝑋 ) → ( 𝒫 𝑋 ∩ ∩ 𝑏 ∈ 𝐾 { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑐 ∈ 𝑎 𝐸 ∈ 𝑎 } ) ∈ ( ACS ‘ 𝑋 ) )
9	1 8	eqeltrrid	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑏 ∈ 𝐾 ∀ 𝑐 ∈ 𝑋 𝐸 ∈ 𝑋 ) → { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑏 ∈ 𝐾 ∀ 𝑐 ∈ 𝑎 𝐸 ∈ 𝑎 } ∈ ( ACS ‘ 𝑋 ) )