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