Metamath Proof Explorer

Theorem isacs2

Description: In the definition of an algebraic closure system, we may always take the operation being closed over as the Moore closure. (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Hypothesis isacs2.f ⊢ F = mrCls ⁡ C
Assertion isacs2 ⊢ C ∈ ACS ⁡ X ↔ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 X s ∈ C ↔ ∀ y ∈ 𝒫 s ∩ Fin F ⁡ y ⊆ s

Proof

Step Hyp Ref Expression
1 isacs2.f ⊢ F = mrCls ⁡ C
2 isacs ⊢ C ∈ ACS ⁡ X ↔ C ∈ Moore ⁡ X ∧ ∃ f f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ⋃ f 𝒫 t ∩ Fin ⊆ t
3 ffun ⊢ f : 𝒫 X ⟶ 𝒫 X → Fun ⁡ f
4 funiunfv ⊢ Fun ⁡ f → ⋃ z ∈ 𝒫 t ∩ Fin f ⁡ z = ⋃ f 𝒫 t ∩ Fin
5 3 4 syl ⊢ f : 𝒫 X ⟶ 𝒫 X → ⋃ z ∈ 𝒫 t ∩ Fin f ⁡ z = ⋃ f 𝒫 t ∩ Fin
6 5 sseq1d ⊢ f : 𝒫 X ⟶ 𝒫 X → ⋃ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ↔ ⋃ f 𝒫 t ∩ Fin ⊆ t
7 iunss ⊢ ⋃ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t
8 6 7 bitr3di ⊢ f : 𝒫 X ⟶ 𝒫 X → ⋃ f 𝒫 t ∩ Fin ⊆ t ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t
9 8 bibi2d ⊢ f : 𝒫 X ⟶ 𝒫 X → t ∈ C ↔ ⋃ f 𝒫 t ∩ Fin ⊆ t ↔ t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t
10 9 ralbidv ⊢ f : 𝒫 X ⟶ 𝒫 X → ∀ t ∈ 𝒫 X t ∈ C ↔ ⋃ f 𝒫 t ∩ Fin ⊆ t ↔ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t
11 10 pm5.32i ⊢ f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ⋃ f 𝒫 t ∩ Fin ⊆ t ↔ f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t
12 11 exbii ⊢ ∃ f f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ⋃ f 𝒫 t ∩ Fin ⊆ t ↔ ∃ f f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t
13 simpll ⊢ C ∈ Moore ⁡ X ∧ s ∈ C ∧ y ∈ 𝒫 s ∩ Fin → C ∈ Moore ⁡ X
14 elinel1 ⊢ y ∈ 𝒫 s ∩ Fin → y ∈ 𝒫 s
15 14 elpwid ⊢ y ∈ 𝒫 s ∩ Fin → y ⊆ s
16 15 adantl ⊢ C ∈ Moore ⁡ X ∧ s ∈ C ∧ y ∈ 𝒫 s ∩ Fin → y ⊆ s
17 simplr ⊢ C ∈ Moore ⁡ X ∧ s ∈ C ∧ y ∈ 𝒫 s ∩ Fin → s ∈ C
18 1 mrcsscl ⊢ C ∈ Moore ⁡ X ∧ y ⊆ s ∧ s ∈ C → F ⁡ y ⊆ s
19 13 16 17 18 syl3anc ⊢ C ∈ Moore ⁡ X ∧ s ∈ C ∧ y ∈ 𝒫 s ∩ Fin → F ⁡ y ⊆ s
20 19 ralrimiva ⊢ C ∈ Moore ⁡ X ∧ s ∈ C → ∀ y ∈ 𝒫 s ∩ Fin F ⁡ y ⊆ s
21 20 ad4ant14 ⊢ C ∈ Moore ⁡ X ∧ f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ∧ s ∈ 𝒫 X ∧ s ∈ C → ∀ y ∈ 𝒫 s ∩ Fin F ⁡ y ⊆ s
22 fveq2 ⊢ z = y → f ⁡ z = f ⁡ y
23 22 sseq1d ⊢ z = y → f ⁡ z ⊆ F ⁡ y ↔ f ⁡ y ⊆ F ⁡ y
24 simplll ⊢ C ∈ Moore ⁡ X ∧ f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ∧ s ∈ 𝒫 X ∧ y ∈ 𝒫 s ∩ Fin → C ∈ Moore ⁡ X
25 15 adantl ⊢ C ∈ Moore ⁡ X ∧ f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ∧ s ∈ 𝒫 X ∧ y ∈ 𝒫 s ∩ Fin → y ⊆ s
26 elpwi ⊢ s ∈ 𝒫 X → s ⊆ X
27 26 ad2antlr ⊢ C ∈ Moore ⁡ X ∧ f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ∧ s ∈ 𝒫 X ∧ y ∈ 𝒫 s ∩ Fin → s ⊆ X
28 25 27 sstrd ⊢ C ∈ Moore ⁡ X ∧ f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ∧ s ∈ 𝒫 X ∧ y ∈ 𝒫 s ∩ Fin → y ⊆ X
29 1 mrccl ⊢ C ∈ Moore ⁡ X ∧ y ⊆ X → F ⁡ y ∈ C
30 24 28 29 syl2anc ⊢ C ∈ Moore ⁡ X ∧ f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ∧ s ∈ 𝒫 X ∧ y ∈ 𝒫 s ∩ Fin → F ⁡ y ∈ C
31 eleq1 ⊢ t = F ⁡ y → t ∈ C ↔ F ⁡ y ∈ C
32 pweq ⊢ t = F ⁡ y → 𝒫 t = 𝒫 F ⁡ y
33 32 ineq1d ⊢ t = F ⁡ y → 𝒫 t ∩ Fin = 𝒫 F ⁡ y ∩ Fin
34 sseq2 ⊢ t = F ⁡ y → f ⁡ z ⊆ t ↔ f ⁡ z ⊆ F ⁡ y
35 33 34 raleqbidv ⊢ t = F ⁡ y → ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ↔ ∀ z ∈ 𝒫 F ⁡ y ∩ Fin f ⁡ z ⊆ F ⁡ y
36 31 35 bibi12d ⊢ t = F ⁡ y → t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ↔ F ⁡ y ∈ C ↔ ∀ z ∈ 𝒫 F ⁡ y ∩ Fin f ⁡ z ⊆ F ⁡ y
37 simprr ⊢ C ∈ Moore ⁡ X ∧ f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t → ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t
38 37 ad2antrr ⊢ C ∈ Moore ⁡ X ∧ f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ∧ s ∈ 𝒫 X ∧ y ∈ 𝒫 s ∩ Fin → ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t
39 mresspw ⊢ C ∈ Moore ⁡ X → C ⊆ 𝒫 X
40 39 ad3antrrr ⊢ C ∈ Moore ⁡ X ∧ f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ∧ s ∈ 𝒫 X ∧ y ∈ 𝒫 s ∩ Fin → C ⊆ 𝒫 X
41 40 30 sseldd ⊢ C ∈ Moore ⁡ X ∧ f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ∧ s ∈ 𝒫 X ∧ y ∈ 𝒫 s ∩ Fin → F ⁡ y ∈ 𝒫 X
42 36 38 41 rspcdva ⊢ C ∈ Moore ⁡ X ∧ f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ∧ s ∈ 𝒫 X ∧ y ∈ 𝒫 s ∩ Fin → F ⁡ y ∈ C ↔ ∀ z ∈ 𝒫 F ⁡ y ∩ Fin f ⁡ z ⊆ F ⁡ y
43 30 42 mpbid ⊢ C ∈ Moore ⁡ X ∧ f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ∧ s ∈ 𝒫 X ∧ y ∈ 𝒫 s ∩ Fin → ∀ z ∈ 𝒫 F ⁡ y ∩ Fin f ⁡ z ⊆ F ⁡ y
44 24 1 28 mrcssidd ⊢ C ∈ Moore ⁡ X ∧ f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ∧ s ∈ 𝒫 X ∧ y ∈ 𝒫 s ∩ Fin → y ⊆ F ⁡ y
45 vex ⊢ y ∈ V
46 45 elpw ⊢ y ∈ 𝒫 F ⁡ y ↔ y ⊆ F ⁡ y
47 44 46 sylibr ⊢ C ∈ Moore ⁡ X ∧ f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ∧ s ∈ 𝒫 X ∧ y ∈ 𝒫 s ∩ Fin → y ∈ 𝒫 F ⁡ y
48 elinel2 ⊢ y ∈ 𝒫 s ∩ Fin → y ∈ Fin
49 48 adantl ⊢ C ∈ Moore ⁡ X ∧ f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ∧ s ∈ 𝒫 X ∧ y ∈ 𝒫 s ∩ Fin → y ∈ Fin
50 47 49 elind ⊢ C ∈ Moore ⁡ X ∧ f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ∧ s ∈ 𝒫 X ∧ y ∈ 𝒫 s ∩ Fin → y ∈ 𝒫 F ⁡ y ∩ Fin
51 23 43 50 rspcdva ⊢ C ∈ Moore ⁡ X ∧ f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ∧ s ∈ 𝒫 X ∧ y ∈ 𝒫 s ∩ Fin → f ⁡ y ⊆ F ⁡ y
52 sstr2 ⊢ f ⁡ y ⊆ F ⁡ y → F ⁡ y ⊆ s → f ⁡ y ⊆ s
53 51 52 syl ⊢ C ∈ Moore ⁡ X ∧ f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ∧ s ∈ 𝒫 X ∧ y ∈ 𝒫 s ∩ Fin → F ⁡ y ⊆ s → f ⁡ y ⊆ s
54 53 ralimdva ⊢ C ∈ Moore ⁡ X ∧ f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ∧ s ∈ 𝒫 X → ∀ y ∈ 𝒫 s ∩ Fin F ⁡ y ⊆ s → ∀ y ∈ 𝒫 s ∩ Fin f ⁡ y ⊆ s
55 54 imp ⊢ C ∈ Moore ⁡ X ∧ f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ∧ s ∈ 𝒫 X ∧ ∀ y ∈ 𝒫 s ∩ Fin F ⁡ y ⊆ s → ∀ y ∈ 𝒫 s ∩ Fin f ⁡ y ⊆ s
56 fveq2 ⊢ y = z → f ⁡ y = f ⁡ z
57 56 sseq1d ⊢ y = z → f ⁡ y ⊆ s ↔ f ⁡ z ⊆ s
58 57 cbvralvw ⊢ ∀ y ∈ 𝒫 s ∩ Fin f ⁡ y ⊆ s ↔ ∀ z ∈ 𝒫 s ∩ Fin f ⁡ z ⊆ s
59 55 58 sylib ⊢ C ∈ Moore ⁡ X ∧ f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ∧ s ∈ 𝒫 X ∧ ∀ y ∈ 𝒫 s ∩ Fin F ⁡ y ⊆ s → ∀ z ∈ 𝒫 s ∩ Fin f ⁡ z ⊆ s
60 eleq1 ⊢ t = s → t ∈ C ↔ s ∈ C
61 pweq ⊢ t = s → 𝒫 t = 𝒫 s
62 61 ineq1d ⊢ t = s → 𝒫 t ∩ Fin = 𝒫 s ∩ Fin
63 sseq2 ⊢ t = s → f ⁡ z ⊆ t ↔ f ⁡ z ⊆ s
64 62 63 raleqbidv ⊢ t = s → ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ↔ ∀ z ∈ 𝒫 s ∩ Fin f ⁡ z ⊆ s
65 60 64 bibi12d ⊢ t = s → t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ↔ s ∈ C ↔ ∀ z ∈ 𝒫 s ∩ Fin f ⁡ z ⊆ s
66 37 ad2antrr ⊢ C ∈ Moore ⁡ X ∧ f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ∧ s ∈ 𝒫 X ∧ ∀ y ∈ 𝒫 s ∩ Fin F ⁡ y ⊆ s → ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t
67 simplr ⊢ C ∈ Moore ⁡ X ∧ f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ∧ s ∈ 𝒫 X ∧ ∀ y ∈ 𝒫 s ∩ Fin F ⁡ y ⊆ s → s ∈ 𝒫 X
68 65 66 67 rspcdva ⊢ C ∈ Moore ⁡ X ∧ f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ∧ s ∈ 𝒫 X ∧ ∀ y ∈ 𝒫 s ∩ Fin F ⁡ y ⊆ s → s ∈ C ↔ ∀ z ∈ 𝒫 s ∩ Fin f ⁡ z ⊆ s
69 59 68 mpbird ⊢ C ∈ Moore ⁡ X ∧ f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ∧ s ∈ 𝒫 X ∧ ∀ y ∈ 𝒫 s ∩ Fin F ⁡ y ⊆ s → s ∈ C
70 21 69 impbida ⊢ C ∈ Moore ⁡ X ∧ f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ∧ s ∈ 𝒫 X → s ∈ C ↔ ∀ y ∈ 𝒫 s ∩ Fin F ⁡ y ⊆ s
71 70 ralrimiva ⊢ C ∈ Moore ⁡ X ∧ f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t → ∀ s ∈ 𝒫 X s ∈ C ↔ ∀ y ∈ 𝒫 s ∩ Fin F ⁡ y ⊆ s
72 71 ex ⊢ C ∈ Moore ⁡ X → f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t → ∀ s ∈ 𝒫 X s ∈ C ↔ ∀ y ∈ 𝒫 s ∩ Fin F ⁡ y ⊆ s
73 72 exlimdv ⊢ C ∈ Moore ⁡ X → ∃ f f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t → ∀ s ∈ 𝒫 X s ∈ C ↔ ∀ y ∈ 𝒫 s ∩ Fin F ⁡ y ⊆ s
74 1 mrcf ⊢ C ∈ Moore ⁡ X → F : 𝒫 X ⟶ C
75 74 39 fssd ⊢ C ∈ Moore ⁡ X → F : 𝒫 X ⟶ 𝒫 X
76 1 fvexi ⊢ F ∈ V
77 feq1 ⊢ f = F → f : 𝒫 X ⟶ 𝒫 X ↔ F : 𝒫 X ⟶ 𝒫 X
78 fveq1 ⊢ f = F → f ⁡ z = F ⁡ z
79 78 sseq1d ⊢ f = F → f ⁡ z ⊆ t ↔ F ⁡ z ⊆ t
80 79 ralbidv ⊢ f = F → ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ↔ ∀ z ∈ 𝒫 t ∩ Fin F ⁡ z ⊆ t
81 fveq2 ⊢ z = y → F ⁡ z = F ⁡ y
82 81 sseq1d ⊢ z = y → F ⁡ z ⊆ t ↔ F ⁡ y ⊆ t
83 82 cbvralvw ⊢ ∀ z ∈ 𝒫 t ∩ Fin F ⁡ z ⊆ t ↔ ∀ y ∈ 𝒫 t ∩ Fin F ⁡ y ⊆ t
84 80 83 bitrdi ⊢ f = F → ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ↔ ∀ y ∈ 𝒫 t ∩ Fin F ⁡ y ⊆ t
85 84 bibi2d ⊢ f = F → t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ↔ t ∈ C ↔ ∀ y ∈ 𝒫 t ∩ Fin F ⁡ y ⊆ t
86 85 ralbidv ⊢ f = F → ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ↔ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ y ∈ 𝒫 t ∩ Fin F ⁡ y ⊆ t
87 sseq2 ⊢ t = s → F ⁡ y ⊆ t ↔ F ⁡ y ⊆ s
88 62 87 raleqbidv ⊢ t = s → ∀ y ∈ 𝒫 t ∩ Fin F ⁡ y ⊆ t ↔ ∀ y ∈ 𝒫 s ∩ Fin F ⁡ y ⊆ s
89 60 88 bibi12d ⊢ t = s → t ∈ C ↔ ∀ y ∈ 𝒫 t ∩ Fin F ⁡ y ⊆ t ↔ s ∈ C ↔ ∀ y ∈ 𝒫 s ∩ Fin F ⁡ y ⊆ s
90 89 cbvralvw ⊢ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ y ∈ 𝒫 t ∩ Fin F ⁡ y ⊆ t ↔ ∀ s ∈ 𝒫 X s ∈ C ↔ ∀ y ∈ 𝒫 s ∩ Fin F ⁡ y ⊆ s
91 86 90 bitrdi ⊢ f = F → ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ↔ ∀ s ∈ 𝒫 X s ∈ C ↔ ∀ y ∈ 𝒫 s ∩ Fin F ⁡ y ⊆ s
92 77 91 anbi12d ⊢ f = F → f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ↔ F : 𝒫 X ⟶ 𝒫 X ∧ ∀ s ∈ 𝒫 X s ∈ C ↔ ∀ y ∈ 𝒫 s ∩ Fin F ⁡ y ⊆ s
93 76 92 spcev ⊢ F : 𝒫 X ⟶ 𝒫 X ∧ ∀ s ∈ 𝒫 X s ∈ C ↔ ∀ y ∈ 𝒫 s ∩ Fin F ⁡ y ⊆ s → ∃ f f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t
94 75 93 sylan ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 X s ∈ C ↔ ∀ y ∈ 𝒫 s ∩ Fin F ⁡ y ⊆ s → ∃ f f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t
95 94 ex ⊢ C ∈ Moore ⁡ X → ∀ s ∈ 𝒫 X s ∈ C ↔ ∀ y ∈ 𝒫 s ∩ Fin F ⁡ y ⊆ s → ∃ f f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t
96 73 95 impbid ⊢ C ∈ Moore ⁡ X → ∃ f f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ∀ z ∈ 𝒫 t ∩ Fin f ⁡ z ⊆ t ↔ ∀ s ∈ 𝒫 X s ∈ C ↔ ∀ y ∈ 𝒫 s ∩ Fin F ⁡ y ⊆ s
97 12 96 syl5bb ⊢ C ∈ Moore ⁡ X → ∃ f f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ⋃ f 𝒫 t ∩ Fin ⊆ t ↔ ∀ s ∈ 𝒫 X s ∈ C ↔ ∀ y ∈ 𝒫 s ∩ Fin F ⁡ y ⊆ s
98 97 pm5.32i ⊢ C ∈ Moore ⁡ X ∧ ∃ f f : 𝒫 X ⟶ 𝒫 X ∧ ∀ t ∈ 𝒫 X t ∈ C ↔ ⋃ f 𝒫 t ∩ Fin ⊆ t ↔ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 X s ∈ C ↔ ∀ y ∈ 𝒫 s ∩ Fin F ⁡ y ⊆ s
99 2 98 bitri ⊢ C ∈ ACS ⁡ X ↔ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 X s ∈ C ↔ ∀ y ∈ 𝒫 s ∩ Fin F ⁡ y ⊆ s