Metamath Proof Explorer

Theorem submrc

Description: In a closure system which is cut off above some level, closures below that level act as normal. (Contributed by Stefan O'Rear, 9-Mar-2015)

Ref Expression
Hypotheses submrc.f ⊢ F = mrCls ⁡ C
submrc.g ⊢ G = mrCls ⁡ C ∩ 𝒫 D
Assertion submrc ⊢ C ∈ Moore ⁡ X ∧ D ∈ C ∧ U ⊆ D → G ⁡ U = F ⁡ U

Proof

Step Hyp Ref Expression
1 submrc.f ⊢ F = mrCls ⁡ C
2 submrc.g ⊢ G = mrCls ⁡ C ∩ 𝒫 D
3 submre ⊢ C ∈ Moore ⁡ X ∧ D ∈ C → C ∩ 𝒫 D ∈ Moore ⁡ D
4 3 3adant3 ⊢ C ∈ Moore ⁡ X ∧ D ∈ C ∧ U ⊆ D → C ∩ 𝒫 D ∈ Moore ⁡ D
5 simp1 ⊢ C ∈ Moore ⁡ X ∧ D ∈ C ∧ U ⊆ D → C ∈ Moore ⁡ X
6 simp3 ⊢ C ∈ Moore ⁡ X ∧ D ∈ C ∧ U ⊆ D → U ⊆ D
7 mress ⊢ C ∈ Moore ⁡ X ∧ D ∈ C → D ⊆ X
8 7 3adant3 ⊢ C ∈ Moore ⁡ X ∧ D ∈ C ∧ U ⊆ D → D ⊆ X
9 6 8 sstrd ⊢ C ∈ Moore ⁡ X ∧ D ∈ C ∧ U ⊆ D → U ⊆ X
10 5 1 9 mrcssidd ⊢ C ∈ Moore ⁡ X ∧ D ∈ C ∧ U ⊆ D → U ⊆ F ⁡ U
11 1 mrccl ⊢ C ∈ Moore ⁡ X ∧ U ⊆ X → F ⁡ U ∈ C
12 5 9 11 syl2anc ⊢ C ∈ Moore ⁡ X ∧ D ∈ C ∧ U ⊆ D → F ⁡ U ∈ C
13 1 mrcsscl ⊢ C ∈ Moore ⁡ X ∧ U ⊆ D ∧ D ∈ C → F ⁡ U ⊆ D
14 13 3com23 ⊢ C ∈ Moore ⁡ X ∧ D ∈ C ∧ U ⊆ D → F ⁡ U ⊆ D
15 fvex ⊢ F ⁡ U ∈ V
16 15 elpw ⊢ F ⁡ U ∈ 𝒫 D ↔ F ⁡ U ⊆ D
17 14 16 sylibr ⊢ C ∈ Moore ⁡ X ∧ D ∈ C ∧ U ⊆ D → F ⁡ U ∈ 𝒫 D
18 12 17 elind ⊢ C ∈ Moore ⁡ X ∧ D ∈ C ∧ U ⊆ D → F ⁡ U ∈ C ∩ 𝒫 D
19 2 mrcsscl ⊢ C ∩ 𝒫 D ∈ Moore ⁡ D ∧ U ⊆ F ⁡ U ∧ F ⁡ U ∈ C ∩ 𝒫 D → G ⁡ U ⊆ F ⁡ U
20 4 10 18 19 syl3anc ⊢ C ∈ Moore ⁡ X ∧ D ∈ C ∧ U ⊆ D → G ⁡ U ⊆ F ⁡ U
21 4 2 6 mrcssidd ⊢ C ∈ Moore ⁡ X ∧ D ∈ C ∧ U ⊆ D → U ⊆ G ⁡ U
22 2 mrccl ⊢ C ∩ 𝒫 D ∈ Moore ⁡ D ∧ U ⊆ D → G ⁡ U ∈ C ∩ 𝒫 D
23 4 6 22 syl2anc ⊢ C ∈ Moore ⁡ X ∧ D ∈ C ∧ U ⊆ D → G ⁡ U ∈ C ∩ 𝒫 D
24 23 elin1d ⊢ C ∈ Moore ⁡ X ∧ D ∈ C ∧ U ⊆ D → G ⁡ U ∈ C
25 1 mrcsscl ⊢ C ∈ Moore ⁡ X ∧ U ⊆ G ⁡ U ∧ G ⁡ U ∈ C → F ⁡ U ⊆ G ⁡ U
26 5 21 24 25 syl3anc ⊢ C ∈ Moore ⁡ X ∧ D ∈ C ∧ U ⊆ D → F ⁡ U ⊆ G ⁡ U
27 20 26 eqssd ⊢ C ∈ Moore ⁡ X ∧ D ∈ C ∧ U ⊆ D → G ⁡ U = F ⁡ U