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 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 ∩ Y b ⊆ a → E ∈ a ↔ ∀ b ∈ X ∩ Y b ∈ 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 ∈ Y E ∈ X ∧ a ∈ 𝒫 X → a ∩ Y ⊆ X ∩ Y
15 ralss ⊢ a ∩ Y ⊆ X ∩ Y → ∀ b ∈ a ∩ Y E ∈ a ↔ ∀ b ∈ X ∩ Y b ∈ a ∩ Y → E ∈ a
16 14 15 syl ⊢ X ∈ V ∧ ∀ b ∈ Y E ∈ X ∧ a ∈ 𝒫 X → ∀ b ∈ a ∩ Y E ∈ a ↔ ∀ b ∈ X ∩ Y b ∈ a ∩ Y → E ∈ a
17 11 16 bitr4id ⊢ 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 eqtrid ⊢ 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 2 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