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 )