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