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 e. V /\ A. b e. K A. c e. X E e. X ) -> { a e. ~P X | A. b e. K A. c e. a E e. a } e. ( ACS ` X ) )

Proof

Step Hyp Ref Expression
1 riinrab 
 |-  ( ~P X i^i |^|_ b e. K { a e. ~P X | A. c e. a E e. a } ) = { a e. ~P X | A. b e. K A. c e. a E e. a }
2 mreacs 
 |-  ( X e. V -> ( ACS ` X ) e. ( Moore ` ~P X ) )
3 acsfn1 
 |-  ( ( X e. V /\ A. c e. X E e. X ) -> { a e. ~P X | A. c e. a E e. a } e. ( ACS ` X ) )
4 3 ex 
 |-  ( X e. V -> ( A. c e. X E e. X -> { a e. ~P X | A. c e. a E e. a } e. ( ACS ` X ) ) )
5 4 ralimdv 
 |-  ( X e. V -> ( A. b e. K A. c e. X E e. X -> A. b e. K { a e. ~P X | A. c e. a E e. a } e. ( ACS ` X ) ) )
6 5 imp 
 |-  ( ( X e. V /\ A. b e. K A. c e. X E e. X ) -> A. b e. K { a e. ~P X | A. c e. a E e. a } e. ( ACS ` X ) )
7 mreriincl 
 |-  ( ( ( ACS ` X ) e. ( Moore ` ~P X ) /\ A. b e. K { a e. ~P X | A. c e. a E e. a } e. ( ACS ` X ) ) -> ( ~P X i^i |^|_ b e. K { a e. ~P X | A. c e. a E e. a } ) e. ( ACS ` X ) )
8 2 6 7 syl2an2r 
 |-  ( ( X e. V /\ A. b e. K A. c e. X E e. X ) -> ( ~P X i^i |^|_ b e. K { a e. ~P X | A. c e. a E e. a } ) e. ( ACS ` X ) )
9 1 8 eqeltrrid 
 |-  ( ( X e. V /\ A. b e. K A. c e. X E e. X ) -> { a e. ~P X | A. b e. K A. c e. a E e. a } e. ( ACS ` X ) )