Metamath Proof Explorer

Theorem isacs4lem

Description: In a closure system in which directed unions of closed sets are closed, closure commutes with directed unions. (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Hypothesis acsdrscl.f ⊢ F = mrCls ⁡ C
Assertion isacs4lem ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ C → C ∈ Moore ⁡ X ∧ ∀ t ∈ 𝒫 𝒫 X toInc ⁡ t ∈ Dirset → F ⁡ ⋃ t = ⋃ F t

Proof

Step Hyp Ref Expression
1 acsdrscl.f ⊢ F = mrCls ⁡ C
2 simpll ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ C ∧ t ∈ 𝒫 𝒫 X ∧ toInc ⁡ t ∈ Dirset → C ∈ Moore ⁡ X
3 elpwi ⊢ t ∈ 𝒫 𝒫 X → t ⊆ 𝒫 X
4 3 ad2antrl ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ C ∧ t ∈ 𝒫 𝒫 X ∧ toInc ⁡ t ∈ Dirset → t ⊆ 𝒫 X
5 1 mrcuni ⊢ C ∈ Moore ⁡ X ∧ t ⊆ 𝒫 X → F ⁡ ⋃ t = F ⁡ ⋃ F t
6 2 4 5 syl2anc ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ C ∧ t ∈ 𝒫 𝒫 X ∧ toInc ⁡ t ∈ Dirset → F ⁡ ⋃ t = F ⁡ ⋃ F t
7 1 mrcf ⊢ C ∈ Moore ⁡ X → F : 𝒫 X ⟶ C
8 7 ffnd ⊢ C ∈ Moore ⁡ X → F Fn 𝒫 X
9 8 adantr ⊢ C ∈ Moore ⁡ X ∧ t ∈ 𝒫 𝒫 X ∧ toInc ⁡ t ∈ Dirset → F Fn 𝒫 X
10 simpll ⊢ C ∈ Moore ⁡ X ∧ t ∈ 𝒫 𝒫 X ∧ toInc ⁡ t ∈ Dirset ∧ x ⊆ y ∧ y ⊆ X → C ∈ Moore ⁡ X
11 simprl ⊢ C ∈ Moore ⁡ X ∧ t ∈ 𝒫 𝒫 X ∧ toInc ⁡ t ∈ Dirset ∧ x ⊆ y ∧ y ⊆ X → x ⊆ y
12 simprr ⊢ C ∈ Moore ⁡ X ∧ t ∈ 𝒫 𝒫 X ∧ toInc ⁡ t ∈ Dirset ∧ x ⊆ y ∧ y ⊆ X → y ⊆ X
13 10 1 11 12 mrcssd ⊢ C ∈ Moore ⁡ X ∧ t ∈ 𝒫 𝒫 X ∧ toInc ⁡ t ∈ Dirset ∧ x ⊆ y ∧ y ⊆ X → F ⁡ x ⊆ F ⁡ y
14 simprr ⊢ C ∈ Moore ⁡ X ∧ t ∈ 𝒫 𝒫 X ∧ toInc ⁡ t ∈ Dirset → toInc ⁡ t ∈ Dirset
15 3 ad2antrl ⊢ C ∈ Moore ⁡ X ∧ t ∈ 𝒫 𝒫 X ∧ toInc ⁡ t ∈ Dirset → t ⊆ 𝒫 X
16 1 fvexi ⊢ F ∈ V
17 16 imaex ⊢ F t ∈ V
18 17 a1i ⊢ C ∈ Moore ⁡ X ∧ t ∈ 𝒫 𝒫 X ∧ toInc ⁡ t ∈ Dirset → F t ∈ V
19 9 13 14 15 18 ipodrsima ⊢ C ∈ Moore ⁡ X ∧ t ∈ 𝒫 𝒫 X ∧ toInc ⁡ t ∈ Dirset → toInc ⁡ F t ∈ Dirset
20 19 adantlr ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ C ∧ t ∈ 𝒫 𝒫 X ∧ toInc ⁡ t ∈ Dirset → toInc ⁡ F t ∈ Dirset
21 fveq2 ⊢ s = F t → toInc ⁡ s = toInc ⁡ F t
22 21 eleq1d ⊢ s = F t → toInc ⁡ s ∈ Dirset ↔ toInc ⁡ F t ∈ Dirset
23 unieq ⊢ s = F t → ⋃ s = ⋃ F t
24 23 eleq1d ⊢ s = F t → ⋃ s ∈ C ↔ ⋃ F t ∈ C
25 22 24 imbi12d ⊢ s = F t → toInc ⁡ s ∈ Dirset → ⋃ s ∈ C ↔ toInc ⁡ F t ∈ Dirset → ⋃ F t ∈ C
26 simplr ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ C ∧ t ∈ 𝒫 𝒫 X ∧ toInc ⁡ t ∈ Dirset → ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ C
27 imassrn ⊢ F t ⊆ ran ⁡ F
28 7 frnd ⊢ C ∈ Moore ⁡ X → ran ⁡ F ⊆ C
29 27 28 sstrid ⊢ C ∈ Moore ⁡ X → F t ⊆ C
30 17 elpw ⊢ F t ∈ 𝒫 C ↔ F t ⊆ C
31 29 30 sylibr ⊢ C ∈ Moore ⁡ X → F t ∈ 𝒫 C
32 31 ad2antrr ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ C ∧ t ∈ 𝒫 𝒫 X ∧ toInc ⁡ t ∈ Dirset → F t ∈ 𝒫 C
33 25 26 32 rspcdva ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ C ∧ t ∈ 𝒫 𝒫 X ∧ toInc ⁡ t ∈ Dirset → toInc ⁡ F t ∈ Dirset → ⋃ F t ∈ C
34 20 33 mpd ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ C ∧ t ∈ 𝒫 𝒫 X ∧ toInc ⁡ t ∈ Dirset → ⋃ F t ∈ C
35 1 mrcid ⊢ C ∈ Moore ⁡ X ∧ ⋃ F t ∈ C → F ⁡ ⋃ F t = ⋃ F t
36 2 34 35 syl2anc ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ C ∧ t ∈ 𝒫 𝒫 X ∧ toInc ⁡ t ∈ Dirset → F ⁡ ⋃ F t = ⋃ F t
37 6 36 eqtrd ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ C ∧ t ∈ 𝒫 𝒫 X ∧ toInc ⁡ t ∈ Dirset → F ⁡ ⋃ t = ⋃ F t
38 37 exp32 ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ C → t ∈ 𝒫 𝒫 X → toInc ⁡ t ∈ Dirset → F ⁡ ⋃ t = ⋃ F t
39 38 ralrimiv ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ C → ∀ t ∈ 𝒫 𝒫 X toInc ⁡ t ∈ Dirset → F ⁡ ⋃ t = ⋃ F t
40 39 ex ⊢ C ∈ Moore ⁡ X → ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ C → ∀ t ∈ 𝒫 𝒫 X toInc ⁡ t ∈ Dirset → F ⁡ ⋃ t = ⋃ F t
41 40 imdistani ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ C → C ∈ Moore ⁡ X ∧ ∀ t ∈ 𝒫 𝒫 X toInc ⁡ t ∈ Dirset → F ⁡ ⋃ t = ⋃ F t