Metamath Proof Explorer

Theorem acsfn1p

Description: Construction of a closure rule from a one-parameterpartial operation. (Contributed by Stefan O'Rear, 12-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 riinrab 
 |-  ( ~P X i^i |^|_ b e. ( X i^i Y ) { a e. ~P X | ( { b } C_ a -> E e. a ) } ) = { a e. ~P X | A. b e. ( X i^i Y ) ( { b } C_ a -> E e. a ) }
2 inss2 
 |-  ( X i^i Y ) C_ Y
3 2 sseli 
 |-  ( b e. ( X i^i Y ) -> b e. Y )
4 3 biantrud 
 |-  ( b e. ( X i^i Y ) -> ( b e. a <-> ( b e. a /\ b e. Y ) ) )
5 vex 
 |-  b e. _V
6 5 snss 
 |-  ( b e. a <-> { b } C_ a )
7 6 bicomi 
 |-  ( { b } C_ a <-> b e. a )
8 elin 
 |-  ( b e. ( a i^i Y ) <-> ( b e. a /\ b e. Y ) )
9 4 7 8 3bitr4g 
 |-  ( b e. ( X i^i Y ) -> ( { b } C_ a <-> b e. ( a i^i Y ) ) )
10 9 imbi1d 
 |-  ( b e. ( X i^i Y ) -> ( ( { b } C_ a -> E e. a ) <-> ( b e. ( a i^i Y ) -> E e. a ) ) )
11 10 ralbiia 
 |-  ( A. b e. ( X i^i Y ) ( { b } C_ a -> E e. a ) <-> A. b e. ( X i^i Y ) ( b e. ( a i^i Y ) -> E e. a ) )
12 elpwi 
 |-  ( a e. ~P X -> a C_ X )
13 12 ssrind 
 |-  ( a e. ~P X -> ( a i^i Y ) C_ ( X i^i Y ) )
14 13 adantl 
 |-  ( ( ( X e. V /\ A. b e. Y E e. X ) /\ a e. ~P X ) -> ( a i^i Y ) C_ ( X i^i Y ) )
15 ralss 
 |-  ( ( a i^i Y ) C_ ( X i^i Y ) -> ( A. b e. ( a i^i Y ) E e. a <-> A. b e. ( X i^i Y ) ( b e. ( a i^i Y ) -> E e. a ) ) )
16 14 15 syl 
 |-  ( ( ( X e. V /\ A. b e. Y E e. X ) /\ a e. ~P X ) -> ( A. b e. ( a i^i Y ) E e. a <-> A. b e. ( X i^i Y ) ( b e. ( a i^i Y ) -> E e. a ) ) )
17 11 16 bitr4id 
 |-  ( ( ( X e. V /\ A. b e. Y E e. X ) /\ a e. ~P X ) -> ( A. b e. ( X i^i Y ) ( { b } C_ a -> E e. a ) <-> A. b e. ( a i^i Y ) E e. a ) )
18 17 rabbidva 
 |-  ( ( X e. V /\ A. b e. Y E e. X ) -> { a e. ~P X | A. b e. ( X i^i Y ) ( { b } C_ a -> E e. a ) } = { a e. ~P X | A. b e. ( a i^i Y ) E e. a } )
19 1 18 eqtrid 
 |-  ( ( X e. V /\ A. b e. Y E e. X ) -> ( ~P X i^i |^|_ b e. ( X i^i Y ) { a e. ~P X | ( { b } C_ a -> E e. a ) } ) = { a e. ~P X | A. b e. ( a i^i Y ) E e. a } )
20 mreacs 
 |-  ( X e. V -> ( ACS ` X ) e. ( Moore ` ~P X ) )
21 20 adantr 
 |-  ( ( X e. V /\ A. b e. Y E e. X ) -> ( ACS ` X ) e. ( Moore ` ~P X ) )
22 ssralv 
 |-  ( ( X i^i Y ) C_ Y -> ( A. b e. Y E e. X -> A. b e. ( X i^i Y ) E e. X ) )
23 2 22 ax-mp 
 |-  ( A. b e. Y E e. X -> A. b e. ( X i^i Y ) E e. X )
24 simpll 
 |-  ( ( ( X e. V /\ b e. ( X i^i Y ) ) /\ E e. X ) -> X e. V )
25 simpr 
 |-  ( ( ( X e. V /\ b e. ( X i^i Y ) ) /\ E e. X ) -> E e. X )
26 inss1 
 |-  ( X i^i Y ) C_ X
27 26 sseli 
 |-  ( b e. ( X i^i Y ) -> b e. X )
28 27 ad2antlr 
 |-  ( ( ( X e. V /\ b e. ( X i^i Y ) ) /\ E e. X ) -> b e. X )
29 28 snssd 
 |-  ( ( ( X e. V /\ b e. ( X i^i Y ) ) /\ E e. X ) -> { b } C_ X )
30 snfi 
 |-  { b } e. Fin
31 30 a1i 
 |-  ( ( ( X e. V /\ b e. ( X i^i Y ) ) /\ E e. X ) -> { b } e. Fin )
32 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 ) )
33 24 25 29 31 32 syl22anc 
 |-  ( ( ( X e. V /\ b e. ( X i^i Y ) ) /\ E e. X ) -> { a e. ~P X | ( { b } C_ a -> E e. a ) } e. ( ACS ` X ) )
34 33 ex 
 |-  ( ( X e. V /\ b e. ( X i^i Y ) ) -> ( E e. X -> { a e. ~P X | ( { b } C_ a -> E e. a ) } e. ( ACS ` X ) ) )
35 34 ralimdva 
 |-  ( X e. V -> ( A. b e. ( X i^i Y ) E e. X -> A. b e. ( X i^i Y ) { a e. ~P X | ( { b } C_ a -> E e. a ) } e. ( ACS ` X ) ) )
36 23 35 syl5 
 |-  ( X e. V -> ( A. b e. Y E e. X -> A. b e. ( X i^i Y ) { a e. ~P X | ( { b } C_ a -> E e. a ) } e. ( ACS ` X ) ) )
37 36 imp 
 |-  ( ( X e. V /\ A. b e. Y E e. X ) -> A. b e. ( X i^i Y ) { a e. ~P X | ( { b } C_ a -> E e. a ) } e. ( ACS ` X ) )
38 mreriincl 
 |-  ( ( ( ACS ` X ) e. ( Moore ` ~P X ) /\ A. b e. ( X i^i Y ) { a e. ~P X | ( { b } C_ a -> E e. a ) } e. ( ACS ` X ) ) -> ( ~P X i^i |^|_ b e. ( X i^i Y ) { a e. ~P X | ( { b } C_ a -> E e. a ) } ) e. ( ACS ` X ) )
39 21 37 38 syl2anc 
 |-  ( ( X e. V /\ A. b e. Y E e. X ) -> ( ~P X i^i |^|_ b e. ( X i^i Y ) { a e. ~P X | ( { b } C_ a -> E e. a ) } ) e. ( ACS ` X ) )
40 19 39 eqeltrrd 
 |-  ( ( X e. V /\ A. b e. Y E e. X ) -> { a e. ~P X | A. b e. ( a i^i Y ) E e. a } e. ( ACS ` X ) )