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 ⊢ X ∈ V ∧ ∀ b ∈ K ∀ c ∈ X E ∈ X → a ∈ 𝒫 X | ∀ b ∈ K ∀ c ∈ a E ∈ a ∈ ACS ⁡ X

Proof

Step Hyp Ref Expression
1 riinrab ⊢ 𝒫 X ∩ ⋂ b ∈ K a ∈ 𝒫 X | ∀ c ∈ a E ∈ a = a ∈ 𝒫 X | ∀ b ∈ K ∀ c ∈ a E ∈ a
2 mreacs ⊢ X ∈ V → ACS ⁡ X ∈ Moore ⁡ 𝒫 X
3 acsfn1 ⊢ X ∈ V ∧ ∀ c ∈ X E ∈ X → a ∈ 𝒫 X | ∀ c ∈ a E ∈ a ∈ ACS ⁡ X
4 3 ex ⊢ X ∈ V → ∀ c ∈ X E ∈ X → a ∈ 𝒫 X | ∀ c ∈ a E ∈ a ∈ ACS ⁡ X
5 4 ralimdv ⊢ X ∈ V → ∀ b ∈ K ∀ c ∈ X E ∈ X → ∀ b ∈ K a ∈ 𝒫 X | ∀ c ∈ a E ∈ a ∈ ACS ⁡ X
6 5 imp ⊢ X ∈ V ∧ ∀ b ∈ K ∀ c ∈ X E ∈ X → ∀ b ∈ K a ∈ 𝒫 X | ∀ c ∈ a E ∈ a ∈ ACS ⁡ X
7 mreriincl ⊢ ACS ⁡ X ∈ Moore ⁡ 𝒫 X ∧ ∀ b ∈ K a ∈ 𝒫 X | ∀ c ∈ a E ∈ a ∈ ACS ⁡ X → 𝒫 X ∩ ⋂ b ∈ K a ∈ 𝒫 X | ∀ c ∈ a E ∈ a ∈ ACS ⁡ X
8 2 6 7 syl2an2r ⊢ X ∈ V ∧ ∀ b ∈ K ∀ c ∈ X E ∈ X → 𝒫 X ∩ ⋂ b ∈ K a ∈ 𝒫 X | ∀ c ∈ a E ∈ a ∈ ACS ⁡ X
9 1 8 eqeltrrid ⊢ X ∈ V ∧ ∀ b ∈ K ∀ c ∈ X E ∈ X → a ∈ 𝒫 X | ∀ b ∈ K ∀ c ∈ a E ∈ a ∈ ACS ⁡ X