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	⊢ ( 𝜑 → 𝐴 ∈ ( ACS ‘ 𝑋 ) )
	acsinfdimd.2	⊢ 𝑁 = ( mrCls ‘ 𝐴 )
	acsinfdimd.3	⊢ 𝐼 = ( mrInd ‘ 𝐴 )
	acsinfdimd.4	⊢ ( 𝜑 → 𝑆 ∈ 𝐼 )
	acsinfdimd.5	⊢ ( 𝜑 → 𝑇 ∈ 𝐼 )
	acsinfdimd.6	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑆 ) = ( 𝑁 ‘ 𝑇 ) )
	acsinfdimd.7	⊢ ( 𝜑 → ¬ 𝑆 ∈ Fin )
Assertion	acsinfdimd	⊢ ( 𝜑 → 𝑆 ≈ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		acsinfdimd.1	⊢ ( 𝜑 → 𝐴 ∈ ( ACS ‘ 𝑋 ) )
2		acsinfdimd.2	⊢ 𝑁 = ( mrCls ‘ 𝐴 )
3		acsinfdimd.3	⊢ 𝐼 = ( mrInd ‘ 𝐴 )
4		acsinfdimd.4	⊢ ( 𝜑 → 𝑆 ∈ 𝐼 )
5		acsinfdimd.5	⊢ ( 𝜑 → 𝑇 ∈ 𝐼 )
6		acsinfdimd.6	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑆 ) = ( 𝑁 ‘ 𝑇 ) )
7		acsinfdimd.7	⊢ ( 𝜑 → ¬ 𝑆 ∈ Fin )
8	1	acsmred	⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
9	3 8 5	mrissd	⊢ ( 𝜑 → 𝑇 ⊆ 𝑋 )
10	1 2 3 4 9 6 7	acsdomd	⊢ ( 𝜑 → 𝑆 ≼ 𝑇 )
11	3 8 4	mrissd	⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )
12	6	eqcomd	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑇 ) = ( 𝑁 ‘ 𝑆 ) )
13	1 2 3 4 9 6 7	acsinfd	⊢ ( 𝜑 → ¬ 𝑇 ∈ Fin )
14	1 2 3 5 11 12 13	acsdomd	⊢ ( 𝜑 → 𝑇 ≼ 𝑆 )
15		sbth	⊢ ( ( 𝑆 ≼ 𝑇 ∧ 𝑇 ≼ 𝑆 ) → 𝑆 ≈ 𝑇 )
16	10 14 15	syl2anc	⊢ ( 𝜑 → 𝑆 ≈ 𝑇 )