Theorem acsinfdimd

Description: In an algebraic closure system, if two independent sets have equal closure and one is infinite, then they are equinumerous. This is proven by using acsdomd twice with acsinfd . See Section II.5 in Cohn p. 81 to 82. (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	acsinfdimd.1	|- ( ph -> A e. ( ACS ` X ) )
	acsinfdimd.2	|- N = ( mrCls ` A )
	acsinfdimd.3	|- I = ( mrInd ` A )
	acsinfdimd.4	|- ( ph -> S e. I )
	acsinfdimd.5	|- ( ph -> T e. I )
	acsinfdimd.6	|- ( ph -> ( N ` S ) = ( N ` T ) )
	acsinfdimd.7	|- ( ph -> -. S e. Fin )
Assertion	acsinfdimd	|- ( ph -> S ~~ T )

Proof

Step	Hyp	Ref	Expression
1		acsinfdimd.1	|- ( ph -> A e. ( ACS ` X ) )
2		acsinfdimd.2	|- N = ( mrCls ` A )
3		acsinfdimd.3	|- I = ( mrInd ` A )
4		acsinfdimd.4	|- ( ph -> S e. I )
5		acsinfdimd.5	|- ( ph -> T e. I )
6		acsinfdimd.6	|- ( ph -> ( N ` S ) = ( N ` T ) )
7		acsinfdimd.7	|- ( ph -> -. S e. Fin )
8	1	acsmred	|- ( ph -> A e. ( Moore ` X ) )
9	3 8 5	mrissd	|- ( ph -> T C_ X )
10	1 2 3 4 9 6 7	acsdomd	|- ( ph -> S ~<_ T )
11	3 8 4	mrissd	|- ( ph -> S C_ X )
12	6	eqcomd	|- ( ph -> ( N ` T ) = ( N ` S ) )
13	1 2 3 4 9 6 7	acsinfd	|- ( ph -> -. T e. Fin )
14	1 2 3 5 11 12 13	acsdomd	|- ( ph -> T ~<_ S )
15		sbth	|- ( ( S ~<_ T /\ T ~<_ S ) -> S ~~ T )
16	10 14 15	syl2anc	|- ( ph -> S ~~ T )