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∈𝒫CtoInc⁡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∩Fing⊆⋃h
19 17 18 sylbi ⊢g∈𝒫⋃s∩Fin→∃h∈𝒫s∩Fing⊆⋃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∩Fing⊆⋃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∈𝒫CtoInc⁡s∈Dirset→⋃s∈s
54 2 53 jca ⊢C∈NoeACS⁡X→C∈Moore⁡X∧∀s∈𝒫CtoInc⁡s∈Dirset→⋃s∈s
55 simpl ⊢C∈Moore⁡X∧∀s∈𝒫CtoInc⁡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∈𝒫CtoInc⁡s∈Dirset→⋃s∈s→∀s∈𝒫CtoInc⁡s∈Dirset→⋃s∈C
60 59 imp ⊢C∈Moore⁡X∧∀s∈𝒫CtoInc⁡s∈Dirset→⋃s∈s→∀s∈𝒫CtoInc⁡s∈Dirset→⋃s∈C
61 isacs3 ⊢C∈ACS⁡X↔C∈Moore⁡X∧∀s∈𝒫CtoInc⁡s∈Dirset→⋃s∈C
62 55 60 61 sylanbrc ⊢C∈Moore⁡X∧∀s∈𝒫CtoInc⁡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∈𝒫CtoInc⁡s∈Dirset→⋃s∈s∧t∈C→mrCls⁡C⁡t=t
65 62 adantr ⊢C∈Moore⁡X∧∀s∈𝒫CtoInc⁡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∈𝒫CtoInc⁡s∈Dirset→⋃s∈s∧t∈C→t⊆X
68 65 10 67 acsficld ⊢C∈Moore⁡X∧∀s∈𝒫CtoInc⁡s∈Dirset→⋃s∈s∧t∈C→mrCls⁡C⁡t=⋃mrCls⁡C𝒫t∩Fin
69 64 68 eqtr3d ⊢C∈Moore⁡X∧∀s∈𝒫CtoInc⁡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⁡CFn𝒫X
72 71 adantr ⊢C∈Moore⁡X∧t∈C→mrCls⁡CFn𝒫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∈𝒫CtoInc⁡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∈𝒫CtoInc⁡s∈Dirset→⋃s∈s∧t∈C→mrCls⁡C𝒫t∩Fin∈𝒫C
95 simplr ⊢C∈Moore⁡X∧∀s∈𝒫CtoInc⁡s∈Dirset→⋃s∈s∧t∈C→∀s∈𝒫CtoInc⁡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∈𝒫CtoInc⁡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∈𝒫CtoInc⁡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∈𝒫CtoInc⁡s∈Dirset→⋃s∈s∧t∈C→⋃mrCls⁡C𝒫t∩Fin∈mrCls⁡C𝒫t∩Fin
105 69 104 eqeltrd ⊢C∈Moore⁡X∧∀s∈𝒫CtoInc⁡s∈Dirset→⋃s∈s∧t∈C→t∈mrCls⁡C𝒫t∩Fin
106 fvelimab ⊢mrCls⁡CFn𝒫X∧𝒫t∩Fin⊆𝒫X→t∈mrCls⁡C𝒫t∩Fin↔∃g∈𝒫t∩FinmrCls⁡C⁡g=t
107 72 81 106 syl2anc ⊢C∈Moore⁡X∧t∈C→t∈mrCls⁡C𝒫t∩Fin↔∃g∈𝒫t∩FinmrCls⁡C⁡g=t
108 107 adantlr ⊢C∈Moore⁡X∧∀s∈𝒫CtoInc⁡s∈Dirset→⋃s∈s∧t∈C→t∈mrCls⁡C𝒫t∩Fin↔∃g∈𝒫t∩FinmrCls⁡C⁡g=t
109 105 108 mpbid ⊢C∈Moore⁡X∧∀s∈𝒫CtoInc⁡s∈Dirset→⋃s∈s∧t∈C→∃g∈𝒫t∩FinmrCls⁡C⁡g=t
110 eqcom ⊢t=mrCls⁡C⁡g↔mrCls⁡C⁡g=t
111 110 rexbii ⊢∃g∈𝒫t∩Fint=mrCls⁡C⁡g↔∃g∈𝒫t∩FinmrCls⁡C⁡g=t
112 109 111 sylibr ⊢C∈Moore⁡X∧∀s∈𝒫CtoInc⁡s∈Dirset→⋃s∈s∧t∈C→∃g∈𝒫t∩Fint=mrCls⁡C⁡g
113 10 mrefg2 ⊢C∈Moore⁡X→∃g∈𝒫X∩Fint=mrCls⁡C⁡g↔∃g∈𝒫t∩Fint=mrCls⁡C⁡g
114 113 ad2antrr ⊢C∈Moore⁡X∧∀s∈𝒫CtoInc⁡s∈Dirset→⋃s∈s∧t∈C→∃g∈𝒫X∩Fint=mrCls⁡C⁡g↔∃g∈𝒫t∩Fint=mrCls⁡C⁡g
115 112 114 mpbird ⊢C∈Moore⁡X∧∀s∈𝒫CtoInc⁡s∈Dirset→⋃s∈s∧t∈C→∃g∈𝒫X∩Fint=mrCls⁡C⁡g
116 115 ralrimiva ⊢C∈Moore⁡X∧∀s∈𝒫CtoInc⁡s∈Dirset→⋃s∈s→∀t∈C∃g∈𝒫X∩Fint=mrCls⁡C⁡g
117 10 isnacs ⊢C∈NoeACS⁡X↔C∈ACS⁡X∧∀t∈C∃g∈𝒫X∩Fint=mrCls⁡C⁡g
118 62 116 117 sylanbrc ⊢C∈Moore⁡X∧∀s∈𝒫CtoInc⁡s∈Dirset→⋃s∈s→C∈NoeACS⁡X
119 54 118 impbii ⊢C∈NoeACS⁡X↔C∈Moore⁡X∧∀s∈𝒫CtoInc⁡s∈Dirset→⋃s∈s