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

Proof

Step Hyp Ref Expression
1 elpwi a 𝒫 X a X
2 ralss a X b a E a b X b a E a
3 1 2 syl a 𝒫 X b a E a b X b a E a
4 vex b V
5 4 snss b a b a
6 5 imbi1i b a E a b a E a
7 6 ralbii b X b a E a b X b a E a
8 3 7 bitrdi a 𝒫 X b a E a b X b a E a
9 8 rabbiia a 𝒫 X | b a E a = a 𝒫 X | b X b a E a
10 riinrab 𝒫 X b X a 𝒫 X | b a E a = a 𝒫 X | b X b a E a
11 9 10 eqtr4i a 𝒫 X | b a E a = 𝒫 X b X a 𝒫 X | b a E a
12 mreacs X V ACS X Moore 𝒫 X
13 simpll X V b X E X X V
14 simpr X V b X E X E X
15 snssi b X b X
16 15 ad2antlr X V b X E X b X
17 snfi b Fin
18 17 a1i X V b X E X b Fin
19 acsfn X V E X b X b Fin a 𝒫 X | b a E a ACS X
20 13 14 16 18 19 syl22anc X V b X E X a 𝒫 X | b a E a ACS X
21 20 ex X V b X E X a 𝒫 X | b a E a ACS X
22 21 ralimdva X V b X E X b X a 𝒫 X | b a E a ACS X
23 22 imp X V b X E X b X a 𝒫 X | b a E a ACS X
24 mreriincl ACS X Moore 𝒫 X b X a 𝒫 X | b a E a ACS X 𝒫 X b X a 𝒫 X | b a E a ACS X
25 12 23 24 syl2an2r X V b X E X 𝒫 X b X a 𝒫 X | b a E a ACS X
26 11 25 eqeltrid X V b X E X a 𝒫 X | b a E a ACS X