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

Proof

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