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

Proof

Step Hyp Ref Expression
1 elpwi ⊢a∈𝒫X→a⊆X
2 ralss ⊢a⊆X→∀b∈aE∈a↔∀b∈Xb∈a→E∈a
3 1 2 syl ⊢a∈𝒫X→∀b∈aE∈a↔∀b∈Xb∈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∈Xb∈a→E∈a↔∀b∈Xb⊆a→E∈a
8 3 7 bitrdi ⊢a∈𝒫X→∀b∈aE∈a↔∀b∈Xb⊆a→E∈a
9 8 rabbiia ⊢a∈𝒫X|∀b∈aE∈a=a∈𝒫X|∀b∈Xb⊆a→E∈a
10 riinrab ⊢𝒫X∩⋂b∈Xa∈𝒫X|b⊆a→E∈a=a∈𝒫X|∀b∈Xb⊆a→E∈a
11 9 10 eqtr4i ⊢a∈𝒫X|∀b∈aE∈a=𝒫X∩⋂b∈Xa∈𝒫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∈XE∈X→∀b∈Xa∈𝒫X|b⊆a→E∈a∈ACS⁡X
23 22 imp ⊢X∈V∧∀b∈XE∈X→∀b∈Xa∈𝒫X|b⊆a→E∈a∈ACS⁡X
24 mreriincl ⊢ACS⁡X∈Moore⁡𝒫X∧∀b∈Xa∈𝒫X|b⊆a→E∈a∈ACS⁡X→𝒫X∩⋂b∈Xa∈𝒫X|b⊆a→E∈a∈ACS⁡X
25 12 23 24 syl2an2r ⊢X∈V∧∀b∈XE∈X→𝒫X∩⋂b∈Xa∈𝒫X|b⊆a→E∈a∈ACS⁡X
26 11 25 eqeltrid ⊢X∈V∧∀b∈XE∈X→a∈𝒫X|∀b∈aE∈a∈ACS⁡X