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 V b Y E X a 𝒫 X | b a Y E a ACS X

Proof

Step Hyp Ref Expression
1 riinrab 𝒫 X b X Y a 𝒫 X | b a E a = a 𝒫 X | b X Y b a E a
2 elpwi a 𝒫 X a X
3 2 ssrind a 𝒫 X a Y X Y
4 3 adantl X V b Y E X a 𝒫 X a Y X Y
5 ralss a Y X Y b a Y E a b X Y b a Y E a
6 4 5 syl X V b Y E X a 𝒫 X b a Y E a b X Y b a Y E a
7 inss2 X Y Y
8 7 sseli b X Y b Y
9 8 biantrud b X Y b a b a b Y
10 vex b V
11 10 snss b a b a
12 11 bicomi b a b a
13 elin b a Y b a b Y
14 9 12 13 3bitr4g b X Y b a b a Y
15 14 imbi1d b X Y b a E a b a Y E a
16 15 ralbiia b X Y b a E a b X Y b a Y E a
17 6 16 syl6rbbr X V b Y E X a 𝒫 X b X Y b a E a b a Y E a
18 17 rabbidva X V b Y E X a 𝒫 X | b X Y b a E a = a 𝒫 X | b a Y E a
19 1 18 syl5eq X V b Y E X 𝒫 X b X Y a 𝒫 X | b a E a = a 𝒫 X | b a Y E a
20 mreacs X V ACS X Moore 𝒫 X
21 20 adantr X V b Y E X ACS X Moore 𝒫 X
22 ssralv X Y Y b Y E X b X Y E X
23 7 22 ax-mp b Y E X b X Y E X
24 simpll X V b X Y E X X V
25 simpr X V b X Y E X E X
26 inss1 X Y X
27 26 sseli b X Y b X
28 27 ad2antlr X V b X Y E X b X
29 28 snssd X V b X Y E X b X
30 snfi b Fin
31 30 a1i X V b X Y E X b Fin
32 acsfn X V E X b X b Fin a 𝒫 X | b a E a ACS X
33 24 25 29 31 32 syl22anc X V b X Y E X a 𝒫 X | b a E a ACS X
34 33 ex X V b X Y E X a 𝒫 X | b a E a ACS X
35 34 ralimdva X V b X Y E X b X Y a 𝒫 X | b a E a ACS X
36 23 35 syl5 X V b Y E X b X Y a 𝒫 X | b a E a ACS X
37 36 imp X V b Y E X b X Y a 𝒫 X | b a E a ACS X
38 mreriincl ACS X Moore 𝒫 X b X Y a 𝒫 X | b a E a ACS X 𝒫 X b X Y a 𝒫 X | b a E a ACS X
39 21 37 38 syl2anc X V b Y E X 𝒫 X b X Y a 𝒫 X | b a E a ACS X
40 19 39 eqeltrrd X V b Y E X a 𝒫 X | b a Y E a ACS X