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 ⊢ 𝐹 = ( mrCls ‘ 𝐶 )
submrc.g ⊢ 𝐺 = ( mrCls ‘ ( 𝐶 ∩ 𝒫 𝐷 ) )
Assertion submrc ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝐷 ∈ 𝐶 ∧ 𝑈 ⊆ 𝐷 ) → ( 𝐺 ‘ 𝑈 ) = ( 𝐹 ‘ 𝑈 ) )

Proof

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