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	$$⊢\phi \to A\in \mathrm{ACS}\left(X\right)$$
	acsinfdimd.2	$$⊢N=\mathrm{mrCls}\left(A\right)$$
	acsinfdimd.3	$$⊢I=\mathrm{mrInd}\left(A\right)$$
	acsinfdimd.4	$$⊢\phi \to S\in I$$
	acsinfdimd.5	$$⊢\phi \to T\in I$$
	acsinfdimd.6	$$⊢\phi \to N\left(S\right)=N\left(T\right)$$
	acsinfdimd.7	$$⊢\phi \to \neg S\in \mathrm{Fin}$$
Assertion	acsinfdimd	$$⊢\phi \to S\approx T$$

Proof

Step	Hyp	Ref	Expression
1		acsinfdimd.1	$$⊢\phi \to A\in \mathrm{ACS}\left(X\right)$$
2		acsinfdimd.2	$$⊢N=\mathrm{mrCls}\left(A\right)$$
3		acsinfdimd.3	$$⊢I=\mathrm{mrInd}\left(A\right)$$
4		acsinfdimd.4	$$⊢\phi \to S\in I$$
5		acsinfdimd.5	$$⊢\phi \to T\in I$$
6		acsinfdimd.6	$$⊢\phi \to N\left(S\right)=N\left(T\right)$$
7		acsinfdimd.7	$$⊢\phi \to \neg S\in \mathrm{Fin}$$
8	1	acsmred	$$⊢\phi \to A\in \mathrm{Moore}\left(X\right)$$
9	3 8 5	mrissd	$$⊢\phi \to T\subseteq X$$
10	1 2 3 4 9 6 7	acsdomd	$$⊢\phi \to S\preccurlyeq T$$
11	3 8 4	mrissd	$$⊢\phi \to S\subseteq X$$
12	6	eqcomd	$$⊢\phi \to N\left(T\right)=N\left(S\right)$$
13	1 2 3 4 9 6 7	acsinfd	$$⊢\phi \to \neg T\in \mathrm{Fin}$$
14	1 2 3 5 11 12 13	acsdomd	$$⊢\phi \to T\preccurlyeq S$$
15		sbth	$$⊢\left(S\preccurlyeq T\wedge T\preccurlyeq S\right)\to S\approx T$$
16	10 14 15	syl2anc	$$⊢\phi \to S\approx T$$