Metamath Proof Explorer

Theorem acsfn1

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

Ref Expression
Assertion acsfn1 
|- ( ( X e. V /\ A. b e. X E e. X ) -> { a e. ~P X | A. b e. a E e. a } e. ( ACS ` X ) )

Proof

Step Hyp Ref Expression
1 elpwi 
 |-  ( a e. ~P X -> a C_ X )
2 ralss 
 |-  ( a C_ X -> ( A. b e. a E e. a <-> A. b e. X ( b e. a -> E e. a ) ) )
3 1 2 syl 
 |-  ( a e. ~P X -> ( A. b e. a E e. a <-> A. b e. X ( b e. a -> E e. a ) ) )
4 vex 
 |-  b e. _V
5 4 snss 
 |-  ( b e. a <-> { b } C_ a )
6 5 imbi1i 
 |-  ( ( b e. a -> E e. a ) <-> ( { b } C_ a -> E e. a ) )
7 6 ralbii 
 |-  ( A. b e. X ( b e. a -> E e. a ) <-> A. b e. X ( { b } C_ a -> E e. a ) )
8 3 7 bitrdi 
 |-  ( a e. ~P X -> ( A. b e. a E e. a <-> A. b e. X ( { b } C_ a -> E e. a ) ) )
9 8 rabbiia 
 |-  { a e. ~P X | A. b e. a E e. a } = { a e. ~P X | A. b e. X ( { b } C_ a -> E e. a ) }
10 riinrab 
 |-  ( ~P X i^i |^|_ b e. X { a e. ~P X | ( { b } C_ a -> E e. a ) } ) = { a e. ~P X | A. b e. X ( { b } C_ a -> E e. a ) }
11 9 10 eqtr4i 
 |-  { a e. ~P X | A. b e. a E e. a } = ( ~P X i^i |^|_ b e. X { a e. ~P X | ( { b } C_ a -> E e. a ) } )
12 mreacs 
 |-  ( X e. V -> ( ACS ` X ) e. ( Moore ` ~P X ) )
13 simpll 
 |-  ( ( ( X e. V /\ b e. X ) /\ E e. X ) -> X e. V )
14 simpr 
 |-  ( ( ( X e. V /\ b e. X ) /\ E e. X ) -> E e. X )
15 snssi 
 |-  ( b e. X -> { b } C_ X )
16 15 ad2antlr 
 |-  ( ( ( X e. V /\ b e. X ) /\ E e. X ) -> { b } C_ X )
17 snfi 
 |-  { b } e. Fin
18 17 a1i 
 |-  ( ( ( X e. V /\ b e. X ) /\ E e. X ) -> { b } e. Fin )
19 acsfn 
 |-  ( ( ( X e. V /\ E e. X ) /\ ( { b } C_ X /\ { b } e. Fin ) ) -> { a e. ~P X | ( { b } C_ a -> E e. a ) } e. ( ACS ` X ) )
20 13 14 16 18 19 syl22anc 
 |-  ( ( ( X e. V /\ b e. X ) /\ E e. X ) -> { a e. ~P X | ( { b } C_ a -> E e. a ) } e. ( ACS ` X ) )
21 20 ex 
 |-  ( ( X e. V /\ b e. X ) -> ( E e. X -> { a e. ~P X | ( { b } C_ a -> E e. a ) } e. ( ACS ` X ) ) )
22 21 ralimdva 
 |-  ( X e. V -> ( A. b e. X E e. X -> A. b e. X { a e. ~P X | ( { b } C_ a -> E e. a ) } e. ( ACS ` X ) ) )
23 22 imp 
 |-  ( ( X e. V /\ A. b e. X E e. X ) -> A. b e. X { a e. ~P X | ( { b } C_ a -> E e. a ) } e. ( ACS ` X ) )
24 mreriincl 
 |-  ( ( ( ACS ` X ) e. ( Moore ` ~P X ) /\ A. b e. X { a e. ~P X | ( { b } C_ a -> E e. a ) } e. ( ACS ` X ) ) -> ( ~P X i^i |^|_ b e. X { a e. ~P X | ( { b } C_ a -> E e. a ) } ) e. ( ACS ` X ) )
25 12 23 24 syl2an2r 
 |-  ( ( X e. V /\ A. b e. X E e. X ) -> ( ~P X i^i |^|_ b e. X { a e. ~P X | ( { b } C_ a -> E e. a ) } ) e. ( ACS ` X ) )
26 11 25 eqeltrid 
 |-  ( ( X e. V /\ A. b e. X E e. X ) -> { a e. ~P X | A. b e. a E e. a } e. ( ACS ` X ) )