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∈XE∈X→a∈𝒫X|∀b∈K∀c∈aE∈a∈ACS⁡X

Proof

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