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

Proof

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

Metamath Proof Explorer

Theorem acsinfdimd

Proof