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 )

Metamath Proof Explorer

Theorem acsinfdimd

Proof