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∈V∧∀b∈X∀c∈XE∈X→a∈𝒫X|∀b∈a∀c∈aE∈a∈ACS⁡X

Proof

Step Hyp Ref Expression
1 elpwi ⊢a∈𝒫X→a⊆X
2 ralss ⊢a⊆X→∀b∈a∀c∈aE∈a↔∀b∈Xb∈a→∀c∈aE∈a
3 ralss ⊢a⊆X→∀c∈ab∈a→E∈a↔∀c∈Xc∈a→b∈a→E∈a
4 r19.21v ⊢∀c∈ab∈a→E∈a↔b∈a→∀c∈aE∈a
5 impexp ⊢c∈a∧b∈a→E∈a↔c∈a→b∈a→E∈a
6 vex ⊢c∈V
7 vex ⊢b∈V
8 6 7 prss ⊢c∈a∧b∈a↔cb⊆a
9 8 imbi1i ⊢c∈a∧b∈a→E∈a↔cb⊆a→E∈a
10 5 9 bitr3i ⊢c∈a→b∈a→E∈a↔cb⊆a→E∈a
11 10 ralbii ⊢∀c∈Xc∈a→b∈a→E∈a↔∀c∈Xcb⊆a→E∈a
12 3 4 11 3bitr3g ⊢a⊆X→b∈a→∀c∈aE∈a↔∀c∈Xcb⊆a→E∈a
13 12 ralbidv ⊢a⊆X→∀b∈Xb∈a→∀c∈aE∈a↔∀b∈X∀c∈Xcb⊆a→E∈a
14 2 13 bitrd ⊢a⊆X→∀b∈a∀c∈aE∈a↔∀b∈X∀c∈Xcb⊆a→E∈a
15 1 14 syl ⊢a∈𝒫X→∀b∈a∀c∈aE∈a↔∀b∈X∀c∈Xcb⊆a→E∈a
16 15 rabbiia ⊢a∈𝒫X|∀b∈a∀c∈aE∈a=a∈𝒫X|∀b∈X∀c∈Xcb⊆a→E∈a
17 riinrab ⊢𝒫X∩⋂b∈Xa∈𝒫X|∀c∈Xcb⊆a→E∈a=a∈𝒫X|∀b∈X∀c∈Xcb⊆a→E∈a
18 16 17 eqtr4i ⊢a∈𝒫X|∀b∈a∀c∈aE∈a=𝒫X∩⋂b∈Xa∈𝒫X|∀c∈Xcb⊆a→E∈a
19 mreacs ⊢X∈V→ACS⁡X∈Moore⁡𝒫X
20 riinrab ⊢𝒫X∩⋂c∈Xa∈𝒫X|cb⊆a→E∈a=a∈𝒫X|∀c∈Xcb⊆a→E∈a
21 19 ad2antrr ⊢X∈V∧b∈X∧∀c∈XE∈X→ACS⁡X∈Moore⁡𝒫X
22 simpll ⊢X∈V∧b∈X∧c∈X∧E∈X→X∈V
23 simprr ⊢X∈V∧b∈X∧c∈X∧E∈X→E∈X
24 prssi ⊢c∈X∧b∈X→cb⊆X
25 24 ancoms ⊢b∈X∧c∈X→cb⊆X
26 25 ad2ant2lr ⊢X∈V∧b∈X∧c∈X∧E∈X→cb⊆X
27 prfi ⊢cb∈Fin
28 27 a1i ⊢X∈V∧b∈X∧c∈X∧E∈X→cb∈Fin
29 acsfn ⊢X∈V∧E∈X∧cb⊆X∧cb∈Fin→a∈𝒫X|cb⊆a→E∈a∈ACS⁡X
30 22 23 26 28 29 syl22anc ⊢X∈V∧b∈X∧c∈X∧E∈X→a∈𝒫X|cb⊆a→E∈a∈ACS⁡X
31 30 expr ⊢X∈V∧b∈X∧c∈X→E∈X→a∈𝒫X|cb⊆a→E∈a∈ACS⁡X
32 31 ralimdva ⊢X∈V∧b∈X→∀c∈XE∈X→∀c∈Xa∈𝒫X|cb⊆a→E∈a∈ACS⁡X
33 32 imp ⊢X∈V∧b∈X∧∀c∈XE∈X→∀c∈Xa∈𝒫X|cb⊆a→E∈a∈ACS⁡X
34 mreriincl ⊢ACS⁡X∈Moore⁡𝒫X∧∀c∈Xa∈𝒫X|cb⊆a→E∈a∈ACS⁡X→𝒫X∩⋂c∈Xa∈𝒫X|cb⊆a→E∈a∈ACS⁡X
35 21 33 34 syl2anc ⊢X∈V∧b∈X∧∀c∈XE∈X→𝒫X∩⋂c∈Xa∈𝒫X|cb⊆a→E∈a∈ACS⁡X
36 20 35 eqeltrrid ⊢X∈V∧b∈X∧∀c∈XE∈X→a∈𝒫X|∀c∈Xcb⊆a→E∈a∈ACS⁡X
37 36 ex ⊢X∈V∧b∈X→∀c∈XE∈X→a∈𝒫X|∀c∈Xcb⊆a→E∈a∈ACS⁡X
38 37 ralimdva ⊢X∈V→∀b∈X∀c∈XE∈X→∀b∈Xa∈𝒫X|∀c∈Xcb⊆a→E∈a∈ACS⁡X
39 38 imp ⊢X∈V∧∀b∈X∀c∈XE∈X→∀b∈Xa∈𝒫X|∀c∈Xcb⊆a→E∈a∈ACS⁡X
40 mreriincl ⊢ACS⁡X∈Moore⁡𝒫X∧∀b∈Xa∈𝒫X|∀c∈Xcb⊆a→E∈a∈ACS⁡X→𝒫X∩⋂b∈Xa∈𝒫X|∀c∈Xcb⊆a→E∈a∈ACS⁡X
41 19 39 40 syl2an2r ⊢X∈V∧∀b∈X∀c∈XE∈X→𝒫X∩⋂b∈Xa∈𝒫X|∀c∈Xcb⊆a→E∈a∈ACS⁡X
42 18 41 eqeltrid ⊢X∈V∧∀b∈X∀c∈XE∈X→a∈𝒫X|∀b∈a∀c∈aE∈a∈ACS⁡X