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 i^i ~P D ) )
Assertion submrc 
|- ( ( C e. ( Moore ` X ) /\ D e. C /\ U C_ D ) -> ( G ` U ) = ( F ` U ) )

Proof

Step Hyp Ref Expression
1 submrc.f 
 |-  F = ( mrCls ` C )
2 submrc.g 
 |-  G = ( mrCls ` ( C i^i ~P D ) )
3 submre 
 |-  ( ( C e. ( Moore ` X ) /\ D e. C ) -> ( C i^i ~P D ) e. ( Moore ` D ) )
4 3 3adant3 
 |-  ( ( C e. ( Moore ` X ) /\ D e. C /\ U C_ D ) -> ( C i^i ~P D ) e. ( Moore ` D ) )
5 simp1 
 |-  ( ( C e. ( Moore ` X ) /\ D e. C /\ U C_ D ) -> C e. ( Moore ` X ) )
6 simp3 
 |-  ( ( C e. ( Moore ` X ) /\ D e. C /\ U C_ D ) -> U C_ D )
7 mress 
 |-  ( ( C e. ( Moore ` X ) /\ D e. C ) -> D C_ X )
8 7 3adant3 
 |-  ( ( C e. ( Moore ` X ) /\ D e. C /\ U C_ D ) -> D C_ X )
9 6 8 sstrd 
 |-  ( ( C e. ( Moore ` X ) /\ D e. C /\ U C_ D ) -> U C_ X )
10 5 1 9 mrcssidd 
 |-  ( ( C e. ( Moore ` X ) /\ D e. C /\ U C_ D ) -> U C_ ( F ` U ) )
11 1 mrccl 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ X ) -> ( F ` U ) e. C )
12 5 9 11 syl2anc 
 |-  ( ( C e. ( Moore ` X ) /\ D e. C /\ U C_ D ) -> ( F ` U ) e. C )
13 1 mrcsscl 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ D /\ D e. C ) -> ( F ` U ) C_ D )
14 13 3com23 
 |-  ( ( C e. ( Moore ` X ) /\ D e. C /\ U C_ D ) -> ( F ` U ) C_ D )
15 fvex 
 |-  ( F ` U ) e. _V
16 15 elpw 
 |-  ( ( F ` U ) e. ~P D <-> ( F ` U ) C_ D )
17 14 16 sylibr 
 |-  ( ( C e. ( Moore ` X ) /\ D e. C /\ U C_ D ) -> ( F ` U ) e. ~P D )
18 12 17 elind 
 |-  ( ( C e. ( Moore ` X ) /\ D e. C /\ U C_ D ) -> ( F ` U ) e. ( C i^i ~P D ) )
19 2 mrcsscl 
 |-  ( ( ( C i^i ~P D ) e. ( Moore ` D ) /\ U C_ ( F ` U ) /\ ( F ` U ) e. ( C i^i ~P D ) ) -> ( G ` U ) C_ ( F ` U ) )
20 4 10 18 19 syl3anc 
 |-  ( ( C e. ( Moore ` X ) /\ D e. C /\ U C_ D ) -> ( G ` U ) C_ ( F ` U ) )
21 4 2 6 mrcssidd 
 |-  ( ( C e. ( Moore ` X ) /\ D e. C /\ U C_ D ) -> U C_ ( G ` U ) )
22 2 mrccl 
 |-  ( ( ( C i^i ~P D ) e. ( Moore ` D ) /\ U C_ D ) -> ( G ` U ) e. ( C i^i ~P D ) )
23 4 6 22 syl2anc 
 |-  ( ( C e. ( Moore ` X ) /\ D e. C /\ U C_ D ) -> ( G ` U ) e. ( C i^i ~P D ) )
24 23 elin1d 
 |-  ( ( C e. ( Moore ` X ) /\ D e. C /\ U C_ D ) -> ( G ` U ) e. C )
25 1 mrcsscl 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ ( G ` U ) /\ ( G ` U ) e. C ) -> ( F ` U ) C_ ( G ` U ) )
26 5 21 24 25 syl3anc 
 |-  ( ( C e. ( Moore ` X ) /\ D e. C /\ U C_ D ) -> ( F ` U ) C_ ( G ` U ) )
27 20 26 eqssd 
 |-  ( ( C e. ( Moore ` X ) /\ D e. C /\ U C_ D ) -> ( G ` U ) = ( F ` U ) )