This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mrissmrid

Description: In a Moore system, subsets of independent sets are independent. (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses mrissmrid.1 
|- ( ph -> A e. ( Moore ` X ) )
mrissmrid.2 
|- N = ( mrCls ` A )
mrissmrid.3 
|- I = ( mrInd ` A )
mrissmrid.4 
|- ( ph -> S e. I )
mrissmrid.5 
|- ( ph -> T C_ S )
Assertion mrissmrid 
|- ( ph -> T e. I )

Proof

Step Hyp Ref Expression
1 mrissmrid.1 
 |-  ( ph -> A e. ( Moore ` X ) )
2 mrissmrid.2 
 |-  N = ( mrCls ` A )
3 mrissmrid.3 
 |-  I = ( mrInd ` A )
4 mrissmrid.4 
 |-  ( ph -> S e. I )
5 mrissmrid.5 
 |-  ( ph -> T C_ S )
6 3 1 4 mrissd 
 |-  ( ph -> S C_ X )
7 5 6 sstrd 
 |-  ( ph -> T C_ X )
8 2 3 1 6 ismri2d 
 |-  ( ph -> ( S e. I <-> A. x e. S -. x e. ( N ` ( S \ { x } ) ) ) )
9 4 8 mpbid 
 |-  ( ph -> A. x e. S -. x e. ( N ` ( S \ { x } ) ) )
10 5 sseld 
 |-  ( ph -> ( x e. T -> x e. S ) )
11 5 ssdifd 
 |-  ( ph -> ( T \ { x } ) C_ ( S \ { x } ) )
12 6 ssdifssd 
 |-  ( ph -> ( S \ { x } ) C_ X )
13 1 2 11 12 mrcssd 
 |-  ( ph -> ( N ` ( T \ { x } ) ) C_ ( N ` ( S \ { x } ) ) )
14 13 ssneld 
 |-  ( ph -> ( -. x e. ( N ` ( S \ { x } ) ) -> -. x e. ( N ` ( T \ { x } ) ) ) )
15 10 14 imim12d 
 |-  ( ph -> ( ( x e. S -> -. x e. ( N ` ( S \ { x } ) ) ) -> ( x e. T -> -. x e. ( N ` ( T \ { x } ) ) ) ) )
16 15 ralimdv2 
 |-  ( ph -> ( A. x e. S -. x e. ( N ` ( S \ { x } ) ) -> A. x e. T -. x e. ( N ` ( T \ { x } ) ) ) )
17 9 16 mpd 
 |-  ( ph -> A. x e. T -. x e. ( N ` ( T \ { x } ) ) )
18 2 3 1 7 17 ismri2dd 
 |-  ( ph -> T e. I )