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

Proof

Step Hyp Ref Expression
1 riinrab ⊢𝒫X∩⋂b∈X∩Ya∈𝒫X|b⊆a→E∈a=a∈𝒫X|∀b∈X∩Yb⊆a→E∈a
2 inss2 ⊢X∩Y⊆Y
3 2 sseli ⊢b∈X∩Y→b∈Y
4 3 biantrud ⊢b∈X∩Y→b∈a↔b∈a∧b∈Y
5 vex ⊢b∈V
6 5 snss ⊢b∈a↔b⊆a
7 6 bicomi ⊢b⊆a↔b∈a
8 elin ⊢b∈a∩Y↔b∈a∧b∈Y
9 4 7 8 3bitr4g ⊢b∈X∩Y→b⊆a↔b∈a∩Y
10 9 imbi1d ⊢b∈X∩Y→b⊆a→E∈a↔b∈a∩Y→E∈a
11 10 ralbiia ⊢∀b∈X∩Yb⊆a→E∈a↔∀b∈X∩Yb∈a∩Y→E∈a
12 elpwi ⊢a∈𝒫X→a⊆X
13 12 ssrind ⊢a∈𝒫X→a∩Y⊆X∩Y
14 13 adantl ⊢X∈V∧∀b∈YE∈X∧a∈𝒫X→a∩Y⊆X∩Y
15 ralss ⊢a∩Y⊆X∩Y→∀b∈a∩YE∈a↔∀b∈X∩Yb∈a∩Y→E∈a
16 14 15 syl ⊢X∈V∧∀b∈YE∈X∧a∈𝒫X→∀b∈a∩YE∈a↔∀b∈X∩Yb∈a∩Y→E∈a
17 11 16 bitr4id ⊢X∈V∧∀b∈YE∈X∧a∈𝒫X→∀b∈X∩Yb⊆a→E∈a↔∀b∈a∩YE∈a
18 17 rabbidva ⊢X∈V∧∀b∈YE∈X→a∈𝒫X|∀b∈X∩Yb⊆a→E∈a=a∈𝒫X|∀b∈a∩YE∈a
19 1 18 eqtrid ⊢X∈V∧∀b∈YE∈X→𝒫X∩⋂b∈X∩Ya∈𝒫X|b⊆a→E∈a=a∈𝒫X|∀b∈a∩YE∈a
20 mreacs ⊢X∈V→ACS⁡X∈Moore⁡𝒫X
21 20 adantr ⊢X∈V∧∀b∈YE∈X→ACS⁡X∈Moore⁡𝒫X
22 ssralv ⊢X∩Y⊆Y→∀b∈YE∈X→∀b∈X∩YE∈X
23 2 22 ax-mp ⊢∀b∈YE∈X→∀b∈X∩YE∈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∩YE∈X→∀b∈X∩Ya∈𝒫X|b⊆a→E∈a∈ACS⁡X
36 23 35 syl5 ⊢X∈V→∀b∈YE∈X→∀b∈X∩Ya∈𝒫X|b⊆a→E∈a∈ACS⁡X
37 36 imp ⊢X∈V∧∀b∈YE∈X→∀b∈X∩Ya∈𝒫X|b⊆a→E∈a∈ACS⁡X
38 mreriincl ⊢ACS⁡X∈Moore⁡𝒫X∧∀b∈X∩Ya∈𝒫X|b⊆a→E∈a∈ACS⁡X→𝒫X∩⋂b∈X∩Ya∈𝒫X|b⊆a→E∈a∈ACS⁡X
39 21 37 38 syl2anc ⊢X∈V∧∀b∈YE∈X→𝒫X∩⋂b∈X∩Ya∈𝒫X|b⊆a→E∈a∈ACS⁡X
40 19 39 eqeltrrd ⊢X∈V∧∀b∈YE∈X→a∈𝒫X|∀b∈a∩YE∈a∈ACS⁡X