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

Metamath Proof Explorer

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 ‘ 𝑋 ) )