This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝑆 ≈ 𝑇 )