Metamath Proof Explorer

Theorem isnacs3

Description: A choice-free order equivalent to the Noetherian condition on a closure system. (Contributed by Stefan O'Rear, 4-Apr-2015)

Ref Expression
Assertion isnacs3 ⊢ C ∈ NoeACS ⁡ X ↔ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ s

Proof

Step Hyp Ref Expression
1 nacsacs ⊢ C ∈ NoeACS ⁡ X → C ∈ ACS ⁡ X
2 1 acsmred ⊢ C ∈ NoeACS ⁡ X → C ∈ Moore ⁡ X
3 simpll ⊢ C ∈ NoeACS ⁡ X ∧ s ∈ 𝒫 C ∧ toInc ⁡ s ∈ Dirset → C ∈ NoeACS ⁡ X
4 1 ad2antrr ⊢ C ∈ NoeACS ⁡ X ∧ s ∈ 𝒫 C ∧ toInc ⁡ s ∈ Dirset → C ∈ ACS ⁡ X
5 elpwi ⊢ s ∈ 𝒫 C → s ⊆ C
6 5 ad2antlr ⊢ C ∈ NoeACS ⁡ X ∧ s ∈ 𝒫 C ∧ toInc ⁡ s ∈ Dirset → s ⊆ C
7 simpr ⊢ C ∈ NoeACS ⁡ X ∧ s ∈ 𝒫 C ∧ toInc ⁡ s ∈ Dirset → toInc ⁡ s ∈ Dirset
8 acsdrsel ⊢ C ∈ ACS ⁡ X ∧ s ⊆ C ∧ toInc ⁡ s ∈ Dirset → ⋃ s ∈ C
9 4 6 7 8 syl3anc ⊢ C ∈ NoeACS ⁡ X ∧ s ∈ 𝒫 C ∧ toInc ⁡ s ∈ Dirset → ⋃ s ∈ C
10 eqid ⊢ mrCls ⁡ C = mrCls ⁡ C
11 10 nacsfg ⊢ C ∈ NoeACS ⁡ X ∧ ⋃ s ∈ C → ∃ g ∈ 𝒫 X ∩ Fin ⋃ s = mrCls ⁡ C ⁡ g
12 3 9 11 syl2anc ⊢ C ∈ NoeACS ⁡ X ∧ s ∈ 𝒫 C ∧ toInc ⁡ s ∈ Dirset → ∃ g ∈ 𝒫 X ∩ Fin ⋃ s = mrCls ⁡ C ⁡ g
13 10 mrefg2 ⊢ C ∈ Moore ⁡ X → ∃ g ∈ 𝒫 X ∩ Fin ⋃ s = mrCls ⁡ C ⁡ g ↔ ∃ g ∈ 𝒫 ⋃ s ∩ Fin ⋃ s = mrCls ⁡ C ⁡ g
14 2 13 syl ⊢ C ∈ NoeACS ⁡ X → ∃ g ∈ 𝒫 X ∩ Fin ⋃ s = mrCls ⁡ C ⁡ g ↔ ∃ g ∈ 𝒫 ⋃ s ∩ Fin ⋃ s = mrCls ⁡ C ⁡ g
15 14 ad2antrr ⊢ C ∈ NoeACS ⁡ X ∧ s ∈ 𝒫 C ∧ toInc ⁡ s ∈ Dirset → ∃ g ∈ 𝒫 X ∩ Fin ⋃ s = mrCls ⁡ C ⁡ g ↔ ∃ g ∈ 𝒫 ⋃ s ∩ Fin ⋃ s = mrCls ⁡ C ⁡ g
16 12 15 mpbid ⊢ C ∈ NoeACS ⁡ X ∧ s ∈ 𝒫 C ∧ toInc ⁡ s ∈ Dirset → ∃ g ∈ 𝒫 ⋃ s ∩ Fin ⋃ s = mrCls ⁡ C ⁡ g
17 elfpw ⊢ g ∈ 𝒫 ⋃ s ∩ Fin ↔ g ⊆ ⋃ s ∧ g ∈ Fin
18 fissuni ⊢ g ⊆ ⋃ s ∧ g ∈ Fin → ∃ h ∈ 𝒫 s ∩ Fin g ⊆ ⋃ h
19 17 18 sylbi ⊢ g ∈ 𝒫 ⋃ s ∩ Fin → ∃ h ∈ 𝒫 s ∩ Fin g ⊆ ⋃ h
20 elfpw ⊢ h ∈ 𝒫 s ∩ Fin ↔ h ⊆ s ∧ h ∈ Fin
21 ipodrsfi ⊢ toInc ⁡ s ∈ Dirset ∧ h ⊆ s ∧ h ∈ Fin → ∃ i ∈ s ⋃ h ⊆ i
22 21 3expb ⊢ toInc ⁡ s ∈ Dirset ∧ h ⊆ s ∧ h ∈ Fin → ∃ i ∈ s ⋃ h ⊆ i
23 20 22 sylan2b ⊢ toInc ⁡ s ∈ Dirset ∧ h ∈ 𝒫 s ∩ Fin → ∃ i ∈ s ⋃ h ⊆ i
24 sstr ⊢ g ⊆ ⋃ h ∧ ⋃ h ⊆ i → g ⊆ i
25 24 ancoms ⊢ ⋃ h ⊆ i ∧ g ⊆ ⋃ h → g ⊆ i
26 simpr ⊢ C ∈ NoeACS ⁡ X ∧ s ∈ 𝒫 C ∧ i ∈ s ∧ g ⊆ i ∧ ⋃ s = mrCls ⁡ C ⁡ g → ⋃ s = mrCls ⁡ C ⁡ g
27 2 ad2antrr ⊢ C ∈ NoeACS ⁡ X ∧ s ∈ 𝒫 C ∧ i ∈ s ∧ g ⊆ i → C ∈ Moore ⁡ X
28 simprr ⊢ C ∈ NoeACS ⁡ X ∧ s ∈ 𝒫 C ∧ i ∈ s ∧ g ⊆ i → g ⊆ i
29 5 ad2antlr ⊢ C ∈ NoeACS ⁡ X ∧ s ∈ 𝒫 C ∧ i ∈ s ∧ g ⊆ i → s ⊆ C
30 simprl ⊢ C ∈ NoeACS ⁡ X ∧ s ∈ 𝒫 C ∧ i ∈ s ∧ g ⊆ i → i ∈ s
31 29 30 sseldd ⊢ C ∈ NoeACS ⁡ X ∧ s ∈ 𝒫 C ∧ i ∈ s ∧ g ⊆ i → i ∈ C
32 10 mrcsscl ⊢ C ∈ Moore ⁡ X ∧ g ⊆ i ∧ i ∈ C → mrCls ⁡ C ⁡ g ⊆ i
33 27 28 31 32 syl3anc ⊢ C ∈ NoeACS ⁡ X ∧ s ∈ 𝒫 C ∧ i ∈ s ∧ g ⊆ i → mrCls ⁡ C ⁡ g ⊆ i
34 33 adantr ⊢ C ∈ NoeACS ⁡ X ∧ s ∈ 𝒫 C ∧ i ∈ s ∧ g ⊆ i ∧ ⋃ s = mrCls ⁡ C ⁡ g → mrCls ⁡ C ⁡ g ⊆ i
35 26 34 eqsstrd ⊢ C ∈ NoeACS ⁡ X ∧ s ∈ 𝒫 C ∧ i ∈ s ∧ g ⊆ i ∧ ⋃ s = mrCls ⁡ C ⁡ g → ⋃ s ⊆ i
36 simplrl ⊢ C ∈ NoeACS ⁡ X ∧ s ∈ 𝒫 C ∧ i ∈ s ∧ g ⊆ i ∧ ⋃ s = mrCls ⁡ C ⁡ g → i ∈ s
37 elssuni ⊢ i ∈ s → i ⊆ ⋃ s
38 36 37 syl ⊢ C ∈ NoeACS ⁡ X ∧ s ∈ 𝒫 C ∧ i ∈ s ∧ g ⊆ i ∧ ⋃ s = mrCls ⁡ C ⁡ g → i ⊆ ⋃ s
39 35 38 eqssd ⊢ C ∈ NoeACS ⁡ X ∧ s ∈ 𝒫 C ∧ i ∈ s ∧ g ⊆ i ∧ ⋃ s = mrCls ⁡ C ⁡ g → ⋃ s = i
40 39 36 eqeltrd ⊢ C ∈ NoeACS ⁡ X ∧ s ∈ 𝒫 C ∧ i ∈ s ∧ g ⊆ i ∧ ⋃ s = mrCls ⁡ C ⁡ g → ⋃ s ∈ s
41 40 ex ⊢ C ∈ NoeACS ⁡ X ∧ s ∈ 𝒫 C ∧ i ∈ s ∧ g ⊆ i → ⋃ s = mrCls ⁡ C ⁡ g → ⋃ s ∈ s
42 41 expr ⊢ C ∈ NoeACS ⁡ X ∧ s ∈ 𝒫 C ∧ i ∈ s → g ⊆ i → ⋃ s = mrCls ⁡ C ⁡ g → ⋃ s ∈ s
43 25 42 syl5 ⊢ C ∈ NoeACS ⁡ X ∧ s ∈ 𝒫 C ∧ i ∈ s → ⋃ h ⊆ i ∧ g ⊆ ⋃ h → ⋃ s = mrCls ⁡ C ⁡ g → ⋃ s ∈ s
44 43 expd ⊢ C ∈ NoeACS ⁡ X ∧ s ∈ 𝒫 C ∧ i ∈ s → ⋃ h ⊆ i → g ⊆ ⋃ h → ⋃ s = mrCls ⁡ C ⁡ g → ⋃ s ∈ s
45 44 rexlimdva ⊢ C ∈ NoeACS ⁡ X ∧ s ∈ 𝒫 C → ∃ i ∈ s ⋃ h ⊆ i → g ⊆ ⋃ h → ⋃ s = mrCls ⁡ C ⁡ g → ⋃ s ∈ s
46 23 45 syl5 ⊢ C ∈ NoeACS ⁡ X ∧ s ∈ 𝒫 C → toInc ⁡ s ∈ Dirset ∧ h ∈ 𝒫 s ∩ Fin → g ⊆ ⋃ h → ⋃ s = mrCls ⁡ C ⁡ g → ⋃ s ∈ s
47 46 expdimp ⊢ C ∈ NoeACS ⁡ X ∧ s ∈ 𝒫 C ∧ toInc ⁡ s ∈ Dirset → h ∈ 𝒫 s ∩ Fin → g ⊆ ⋃ h → ⋃ s = mrCls ⁡ C ⁡ g → ⋃ s ∈ s
48 47 rexlimdv ⊢ C ∈ NoeACS ⁡ X ∧ s ∈ 𝒫 C ∧ toInc ⁡ s ∈ Dirset → ∃ h ∈ 𝒫 s ∩ Fin g ⊆ ⋃ h → ⋃ s = mrCls ⁡ C ⁡ g → ⋃ s ∈ s
49 19 48 syl5 ⊢ C ∈ NoeACS ⁡ X ∧ s ∈ 𝒫 C ∧ toInc ⁡ s ∈ Dirset → g ∈ 𝒫 ⋃ s ∩ Fin → ⋃ s = mrCls ⁡ C ⁡ g → ⋃ s ∈ s
50 49 rexlimdv ⊢ C ∈ NoeACS ⁡ X ∧ s ∈ 𝒫 C ∧ toInc ⁡ s ∈ Dirset → ∃ g ∈ 𝒫 ⋃ s ∩ Fin ⋃ s = mrCls ⁡ C ⁡ g → ⋃ s ∈ s
51 16 50 mpd ⊢ C ∈ NoeACS ⁡ X ∧ s ∈ 𝒫 C ∧ toInc ⁡ s ∈ Dirset → ⋃ s ∈ s
52 51 ex ⊢ C ∈ NoeACS ⁡ X ∧ s ∈ 𝒫 C → toInc ⁡ s ∈ Dirset → ⋃ s ∈ s
53 52 ralrimiva ⊢ C ∈ NoeACS ⁡ X → ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ s
54 2 53 jca ⊢ C ∈ NoeACS ⁡ X → C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ s
55 simpl ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ s → C ∈ Moore ⁡ X
56 5 adantl ⊢ C ∈ Moore ⁡ X ∧ s ∈ 𝒫 C → s ⊆ C
57 56 sseld ⊢ C ∈ Moore ⁡ X ∧ s ∈ 𝒫 C → ⋃ s ∈ s → ⋃ s ∈ C
58 57 imim2d ⊢ C ∈ Moore ⁡ X ∧ s ∈ 𝒫 C → toInc ⁡ s ∈ Dirset → ⋃ s ∈ s → toInc ⁡ s ∈ Dirset → ⋃ s ∈ C
59 58 ralimdva ⊢ C ∈ Moore ⁡ X → ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ s → ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ C
60 59 imp ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ s → ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ C
61 isacs3 ⊢ C ∈ ACS ⁡ X ↔ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ C
62 55 60 61 sylanbrc ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ s → C ∈ ACS ⁡ X
63 10 mrcid ⊢ C ∈ Moore ⁡ X ∧ t ∈ C → mrCls ⁡ C ⁡ t = t
64 63 adantlr ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ s ∧ t ∈ C → mrCls ⁡ C ⁡ t = t
65 62 adantr ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ s ∧ t ∈ C → C ∈ ACS ⁡ X
66 mress ⊢ C ∈ Moore ⁡ X ∧ t ∈ C → t ⊆ X
67 66 adantlr ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ s ∧ t ∈ C → t ⊆ X
68 65 10 67 acsficld ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ s ∧ t ∈ C → mrCls ⁡ C ⁡ t = ⋃ mrCls ⁡ C 𝒫 t ∩ Fin
69 64 68 eqtr3d ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ s ∧ t ∈ C → t = ⋃ mrCls ⁡ C 𝒫 t ∩ Fin
70 10 mrcf ⊢ C ∈ Moore ⁡ X → mrCls ⁡ C : 𝒫 X ⟶ C
71 70 ffnd ⊢ C ∈ Moore ⁡ X → mrCls ⁡ C Fn 𝒫 X
72 71 adantr ⊢ C ∈ Moore ⁡ X ∧ t ∈ C → mrCls ⁡ C Fn 𝒫 X
73 10 mrcss ⊢ C ∈ Moore ⁡ X ∧ g ⊆ h ∧ h ⊆ X → mrCls ⁡ C ⁡ g ⊆ mrCls ⁡ C ⁡ h
74 73 3expb ⊢ C ∈ Moore ⁡ X ∧ g ⊆ h ∧ h ⊆ X → mrCls ⁡ C ⁡ g ⊆ mrCls ⁡ C ⁡ h
75 74 adantlr ⊢ C ∈ Moore ⁡ X ∧ t ∈ C ∧ g ⊆ h ∧ h ⊆ X → mrCls ⁡ C ⁡ g ⊆ mrCls ⁡ C ⁡ h
76 vex ⊢ t ∈ V
77 fpwipodrs ⊢ t ∈ V → toInc ⁡ 𝒫 t ∩ Fin ∈ Dirset
78 76 77 mp1i ⊢ C ∈ Moore ⁡ X ∧ t ∈ C → toInc ⁡ 𝒫 t ∩ Fin ∈ Dirset
79 inss1 ⊢ 𝒫 t ∩ Fin ⊆ 𝒫 t
80 66 sspwd ⊢ C ∈ Moore ⁡ X ∧ t ∈ C → 𝒫 t ⊆ 𝒫 X
81 79 80 sstrid ⊢ C ∈ Moore ⁡ X ∧ t ∈ C → 𝒫 t ∩ Fin ⊆ 𝒫 X
82 fvex ⊢ mrCls ⁡ C ∈ V
83 imaexg ⊢ mrCls ⁡ C ∈ V → mrCls ⁡ C 𝒫 t ∩ Fin ∈ V
84 82 83 ax-mp ⊢ mrCls ⁡ C 𝒫 t ∩ Fin ∈ V
85 84 a1i ⊢ C ∈ Moore ⁡ X ∧ t ∈ C → mrCls ⁡ C 𝒫 t ∩ Fin ∈ V
86 72 75 78 81 85 ipodrsima ⊢ C ∈ Moore ⁡ X ∧ t ∈ C → toInc ⁡ mrCls ⁡ C 𝒫 t ∩ Fin ∈ Dirset
87 86 adantlr ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ s ∧ t ∈ C → toInc ⁡ mrCls ⁡ C 𝒫 t ∩ Fin ∈ Dirset
88 imassrn ⊢ mrCls ⁡ C 𝒫 t ∩ Fin ⊆ ran ⁡ mrCls ⁡ C
89 70 frnd ⊢ C ∈ Moore ⁡ X → ran ⁡ mrCls ⁡ C ⊆ C
90 88 89 sstrid ⊢ C ∈ Moore ⁡ X → mrCls ⁡ C 𝒫 t ∩ Fin ⊆ C
91 90 adantr ⊢ C ∈ Moore ⁡ X ∧ t ∈ C → mrCls ⁡ C 𝒫 t ∩ Fin ⊆ C
92 84 elpw ⊢ mrCls ⁡ C 𝒫 t ∩ Fin ∈ 𝒫 C ↔ mrCls ⁡ C 𝒫 t ∩ Fin ⊆ C
93 91 92 sylibr ⊢ C ∈ Moore ⁡ X ∧ t ∈ C → mrCls ⁡ C 𝒫 t ∩ Fin ∈ 𝒫 C
94 93 adantlr ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ s ∧ t ∈ C → mrCls ⁡ C 𝒫 t ∩ Fin ∈ 𝒫 C
95 simplr ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ s ∧ t ∈ C → ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ s
96 fveq2 ⊢ s = mrCls ⁡ C 𝒫 t ∩ Fin → toInc ⁡ s = toInc ⁡ mrCls ⁡ C 𝒫 t ∩ Fin
97 96 eleq1d ⊢ s = mrCls ⁡ C 𝒫 t ∩ Fin → toInc ⁡ s ∈ Dirset ↔ toInc ⁡ mrCls ⁡ C 𝒫 t ∩ Fin ∈ Dirset
98 unieq ⊢ s = mrCls ⁡ C 𝒫 t ∩ Fin → ⋃ s = ⋃ mrCls ⁡ C 𝒫 t ∩ Fin
99 id ⊢ s = mrCls ⁡ C 𝒫 t ∩ Fin → s = mrCls ⁡ C 𝒫 t ∩ Fin
100 98 99 eleq12d ⊢ s = mrCls ⁡ C 𝒫 t ∩ Fin → ⋃ s ∈ s ↔ ⋃ mrCls ⁡ C 𝒫 t ∩ Fin ∈ mrCls ⁡ C 𝒫 t ∩ Fin
101 97 100 imbi12d ⊢ s = mrCls ⁡ C 𝒫 t ∩ Fin → toInc ⁡ s ∈ Dirset → ⋃ s ∈ s ↔ toInc ⁡ mrCls ⁡ C 𝒫 t ∩ Fin ∈ Dirset → ⋃ mrCls ⁡ C 𝒫 t ∩ Fin ∈ mrCls ⁡ C 𝒫 t ∩ Fin
102 101 rspcva ⊢ mrCls ⁡ C 𝒫 t ∩ Fin ∈ 𝒫 C ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ s → toInc ⁡ mrCls ⁡ C 𝒫 t ∩ Fin ∈ Dirset → ⋃ mrCls ⁡ C 𝒫 t ∩ Fin ∈ mrCls ⁡ C 𝒫 t ∩ Fin
103 94 95 102 syl2anc ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ s ∧ t ∈ C → toInc ⁡ mrCls ⁡ C 𝒫 t ∩ Fin ∈ Dirset → ⋃ mrCls ⁡ C 𝒫 t ∩ Fin ∈ mrCls ⁡ C 𝒫 t ∩ Fin
104 87 103 mpd ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ s ∧ t ∈ C → ⋃ mrCls ⁡ C 𝒫 t ∩ Fin ∈ mrCls ⁡ C 𝒫 t ∩ Fin
105 69 104 eqeltrd ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ s ∧ t ∈ C → t ∈ mrCls ⁡ C 𝒫 t ∩ Fin
106 fvelimab ⊢ mrCls ⁡ C Fn 𝒫 X ∧ 𝒫 t ∩ Fin ⊆ 𝒫 X → t ∈ mrCls ⁡ C 𝒫 t ∩ Fin ↔ ∃ g ∈ 𝒫 t ∩ Fin mrCls ⁡ C ⁡ g = t
107 72 81 106 syl2anc ⊢ C ∈ Moore ⁡ X ∧ t ∈ C → t ∈ mrCls ⁡ C 𝒫 t ∩ Fin ↔ ∃ g ∈ 𝒫 t ∩ Fin mrCls ⁡ C ⁡ g = t
108 107 adantlr ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ s ∧ t ∈ C → t ∈ mrCls ⁡ C 𝒫 t ∩ Fin ↔ ∃ g ∈ 𝒫 t ∩ Fin mrCls ⁡ C ⁡ g = t
109 105 108 mpbid ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ s ∧ t ∈ C → ∃ g ∈ 𝒫 t ∩ Fin mrCls ⁡ C ⁡ g = t
110 eqcom ⊢ t = mrCls ⁡ C ⁡ g ↔ mrCls ⁡ C ⁡ g = t
111 110 rexbii ⊢ ∃ g ∈ 𝒫 t ∩ Fin t = mrCls ⁡ C ⁡ g ↔ ∃ g ∈ 𝒫 t ∩ Fin mrCls ⁡ C ⁡ g = t
112 109 111 sylibr ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ s ∧ t ∈ C → ∃ g ∈ 𝒫 t ∩ Fin t = mrCls ⁡ C ⁡ g
113 10 mrefg2 ⊢ C ∈ Moore ⁡ X → ∃ g ∈ 𝒫 X ∩ Fin t = mrCls ⁡ C ⁡ g ↔ ∃ g ∈ 𝒫 t ∩ Fin t = mrCls ⁡ C ⁡ g
114 113 ad2antrr ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ s ∧ t ∈ C → ∃ g ∈ 𝒫 X ∩ Fin t = mrCls ⁡ C ⁡ g ↔ ∃ g ∈ 𝒫 t ∩ Fin t = mrCls ⁡ C ⁡ g
115 112 114 mpbird ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ s ∧ t ∈ C → ∃ g ∈ 𝒫 X ∩ Fin t = mrCls ⁡ C ⁡ g
116 115 ralrimiva ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ s → ∀ t ∈ C ∃ g ∈ 𝒫 X ∩ Fin t = mrCls ⁡ C ⁡ g
117 10 isnacs ⊢ C ∈ NoeACS ⁡ X ↔ C ∈ ACS ⁡ X ∧ ∀ t ∈ C ∃ g ∈ 𝒫 X ∩ Fin t = mrCls ⁡ C ⁡ g
118 62 116 117 sylanbrc ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ s → C ∈ NoeACS ⁡ X
119 54 118 impbii ⊢ C ∈ NoeACS ⁡ X ↔ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ s