Metamath Proof Explorer

Theorem acsfn2

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

Ref Expression
Assertion acsfn2 
|- ( ( X e. V /\ A. b e. X A. c e. X E e. X ) -> { a e. ~P X | A. b e. a A. c 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 A. c e. a E e. a <-> A. b e. X ( b e. a -> A. c e. a E e. a ) ) )
3 ralss 
 |-  ( a C_ X -> ( A. c e. a ( b e. a -> E e. a ) <-> A. c e. X ( c e. a -> ( b e. a -> E e. a ) ) ) )
4 r19.21v 
 |-  ( A. c e. a ( b e. a -> E e. a ) <-> ( b e. a -> A. c e. a E e. a ) )
5 impexp 
 |-  ( ( ( c e. a /\ b e. a ) -> E e. a ) <-> ( c e. a -> ( b e. a -> E e. a ) ) )
6 vex 
 |-  c e. _V
7 vex 
 |-  b e. _V
8 6 7 prss 
 |-  ( ( c e. a /\ b e. a ) <-> { c , b } C_ a )
9 8 imbi1i 
 |-  ( ( ( c e. a /\ b e. a ) -> E e. a ) <-> ( { c , b } C_ a -> E e. a ) )
10 5 9 bitr3i 
 |-  ( ( c e. a -> ( b e. a -> E e. a ) ) <-> ( { c , b } C_ a -> E e. a ) )
11 10 ralbii 
 |-  ( A. c e. X ( c e. a -> ( b e. a -> E e. a ) ) <-> A. c e. X ( { c , b } C_ a -> E e. a ) )
12 3 4 11 3bitr3g 
 |-  ( a C_ X -> ( ( b e. a -> A. c e. a E e. a ) <-> A. c e. X ( { c , b } C_ a -> E e. a ) ) )
13 12 ralbidv 
 |-  ( a C_ X -> ( A. b e. X ( b e. a -> A. c e. a E e. a ) <-> A. b e. X A. c e. X ( { c , b } C_ a -> E e. a ) ) )
14 2 13 bitrd 
 |-  ( a C_ X -> ( A. b e. a A. c e. a E e. a <-> A. b e. X A. c e. X ( { c , b } C_ a -> E e. a ) ) )
15 1 14 syl 
 |-  ( a e. ~P X -> ( A. b e. a A. c e. a E e. a <-> A. b e. X A. c e. X ( { c , b } C_ a -> E e. a ) ) )
16 15 rabbiia 
 |-  { a e. ~P X | A. b e. a A. c e. a E e. a } = { a e. ~P X | A. b e. X A. c e. X ( { c , b } C_ a -> E e. a ) }
17 riinrab 
 |-  ( ~P X i^i |^|_ b e. X { a e. ~P X | A. c e. X ( { c , b } C_ a -> E e. a ) } ) = { a e. ~P X | A. b e. X A. c e. X ( { c , b } C_ a -> E e. a ) }
18 16 17 eqtr4i 
 |-  { a e. ~P X | A. b e. a A. c e. a E e. a } = ( ~P X i^i |^|_ b e. X { a e. ~P X | A. c e. X ( { c , b } C_ a -> E e. a ) } )
19 mreacs 
 |-  ( X e. V -> ( ACS ` X ) e. ( Moore ` ~P X ) )
20 riinrab 
 |-  ( ~P X i^i |^|_ c e. X { a e. ~P X | ( { c , b } C_ a -> E e. a ) } ) = { a e. ~P X | A. c e. X ( { c , b } C_ a -> E e. a ) }
21 19 ad2antrr 
 |-  ( ( ( X e. V /\ b e. X ) /\ A. c e. X E e. X ) -> ( ACS ` X ) e. ( Moore ` ~P X ) )
22 simpll 
 |-  ( ( ( X e. V /\ b e. X ) /\ ( c e. X /\ E e. X ) ) -> X e. V )
23 simprr 
 |-  ( ( ( X e. V /\ b e. X ) /\ ( c e. X /\ E e. X ) ) -> E e. X )
24 prssi 
 |-  ( ( c e. X /\ b e. X ) -> { c , b } C_ X )
25 24 ancoms 
 |-  ( ( b e. X /\ c e. X ) -> { c , b } C_ X )
26 25 ad2ant2lr 
 |-  ( ( ( X e. V /\ b e. X ) /\ ( c e. X /\ E e. X ) ) -> { c , b } C_ X )
27 prfi 
 |-  { c , b } e. Fin
28 27 a1i 
 |-  ( ( ( X e. V /\ b e. X ) /\ ( c e. X /\ E e. X ) ) -> { c , b } e. Fin )
29 acsfn 
 |-  ( ( ( X e. V /\ E e. X ) /\ ( { c , b } C_ X /\ { c , b } e. Fin ) ) -> { a e. ~P X | ( { c , b } C_ a -> E e. a ) } e. ( ACS ` X ) )
30 22 23 26 28 29 syl22anc 
 |-  ( ( ( X e. V /\ b e. X ) /\ ( c e. X /\ E e. X ) ) -> { a e. ~P X | ( { c , b } C_ a -> E e. a ) } e. ( ACS ` X ) )
31 30 expr 
 |-  ( ( ( X e. V /\ b e. X ) /\ c e. X ) -> ( E e. X -> { a e. ~P X | ( { c , b } C_ a -> E e. a ) } e. ( ACS ` X ) ) )
32 31 ralimdva 
 |-  ( ( X e. V /\ b e. X ) -> ( A. c e. X E e. X -> A. c e. X { a e. ~P X | ( { c , b } C_ a -> E e. a ) } e. ( ACS ` X ) ) )
33 32 imp 
 |-  ( ( ( X e. V /\ b e. X ) /\ A. c e. X E e. X ) -> A. c e. X { a e. ~P X | ( { c , b } C_ a -> E e. a ) } e. ( ACS ` X ) )
34 mreriincl 
 |-  ( ( ( ACS ` X ) e. ( Moore ` ~P X ) /\ A. c e. X { a e. ~P X | ( { c , b } C_ a -> E e. a ) } e. ( ACS ` X ) ) -> ( ~P X i^i |^|_ c e. X { a e. ~P X | ( { c , b } C_ a -> E e. a ) } ) e. ( ACS ` X ) )
35 21 33 34 syl2anc 
 |-  ( ( ( X e. V /\ b e. X ) /\ A. c e. X E e. X ) -> ( ~P X i^i |^|_ c e. X { a e. ~P X | ( { c , b } C_ a -> E e. a ) } ) e. ( ACS ` X ) )
36 20 35 eqeltrrid 
 |-  ( ( ( X e. V /\ b e. X ) /\ A. c e. X E e. X ) -> { a e. ~P X | A. c e. X ( { c , b } C_ a -> E e. a ) } e. ( ACS ` X ) )
37 36 ex 
 |-  ( ( X e. V /\ b e. X ) -> ( A. c e. X E e. X -> { a e. ~P X | A. c e. X ( { c , b } C_ a -> E e. a ) } e. ( ACS ` X ) ) )
38 37 ralimdva 
 |-  ( X e. V -> ( A. b e. X A. c e. X E e. X -> A. b e. X { a e. ~P X | A. c e. X ( { c , b } C_ a -> E e. a ) } e. ( ACS ` X ) ) )
39 38 imp 
 |-  ( ( X e. V /\ A. b e. X A. c e. X E e. X ) -> A. b e. X { a e. ~P X | A. c e. X ( { c , b } C_ a -> E e. a ) } e. ( ACS ` X ) )
40 mreriincl 
 |-  ( ( ( ACS ` X ) e. ( Moore ` ~P X ) /\ A. b e. X { a e. ~P X | A. c e. X ( { c , b } C_ a -> E e. a ) } e. ( ACS ` X ) ) -> ( ~P X i^i |^|_ b e. X { a e. ~P X | A. c e. X ( { c , b } C_ a -> E e. a ) } ) e. ( ACS ` X ) )
41 19 39 40 syl2an2r 
 |-  ( ( X e. V /\ A. b e. X A. c e. X E e. X ) -> ( ~P X i^i |^|_ b e. X { a e. ~P X | A. c e. X ( { c , b } C_ a -> E e. a ) } ) e. ( ACS ` X ) )
42 18 41 eqeltrid 
 |-  ( ( X e. V /\ A. b e. X A. c e. X E e. X ) -> { a e. ~P X | A. b e. a A. c e. a E e. a } e. ( ACS ` X ) )