Theorem acsinfd

Description: In an algebraic closure system, if S and T have the same closure and S is infinite independent, then T is infinite. This follows from applying unirnffid to the map given in acsmap2d . See Section II.5 in Cohn p. 81 to 82. (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	acsmap2d.1	⊢ ( 𝜑 → 𝐴 ∈ ( ACS ‘ 𝑋 ) )
	acsmap2d.2	⊢ 𝑁 = ( mrCls ‘ 𝐴 )
	acsmap2d.3	⊢ 𝐼 = ( mrInd ‘ 𝐴 )
	acsmap2d.4	⊢ ( 𝜑 → 𝑆 ∈ 𝐼 )
	acsmap2d.5	⊢ ( 𝜑 → 𝑇 ⊆ 𝑋 )
	acsmap2d.6	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑆 ) = ( 𝑁 ‘ 𝑇 ) )
	acsinfd.7	⊢ ( 𝜑 → ¬ 𝑆 ∈ Fin )
Assertion	acsinfd	⊢ ( 𝜑 → ¬ 𝑇 ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		acsmap2d.1	⊢ ( 𝜑 → 𝐴 ∈ ( ACS ‘ 𝑋 ) )
2		acsmap2d.2	⊢ 𝑁 = ( mrCls ‘ 𝐴 )
3		acsmap2d.3	⊢ 𝐼 = ( mrInd ‘ 𝐴 )
4		acsmap2d.4	⊢ ( 𝜑 → 𝑆 ∈ 𝐼 )
5		acsmap2d.5	⊢ ( 𝜑 → 𝑇 ⊆ 𝑋 )
6		acsmap2d.6	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑆 ) = ( 𝑁 ‘ 𝑇 ) )
7		acsinfd.7	⊢ ( 𝜑 → ¬ 𝑆 ∈ Fin )
8	1 2 3 4 5 6	acsmap2d	⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑆 = ∪ ran 𝑓 ) )
9		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑆 = ∪ ran 𝑓 ) ) ∧ 𝑇 ∈ Fin ) → 𝑆 = ∪ ran 𝑓 )
10		simplrl	⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑆 = ∪ ran 𝑓 ) ) ∧ 𝑇 ∈ Fin ) → 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) )
11		inss2	⊢ ( 𝒫 𝑆 ∩ Fin ) ⊆ Fin
12		fss	⊢ ( ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ( 𝒫 𝑆 ∩ Fin ) ⊆ Fin ) → 𝑓 : 𝑇 ⟶ Fin )
13	10 11 12	sylancl	⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑆 = ∪ ran 𝑓 ) ) ∧ 𝑇 ∈ Fin ) → 𝑓 : 𝑇 ⟶ Fin )
14		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑆 = ∪ ran 𝑓 ) ) ∧ 𝑇 ∈ Fin ) → 𝑇 ∈ Fin )
15	13 14	unirnffid	⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑆 = ∪ ran 𝑓 ) ) ∧ 𝑇 ∈ Fin ) → ∪ ran 𝑓 ∈ Fin )
16	9 15	eqeltrd	⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑆 = ∪ ran 𝑓 ) ) ∧ 𝑇 ∈ Fin ) → 𝑆 ∈ Fin )
17	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑆 = ∪ ran 𝑓 ) ) ∧ 𝑇 ∈ Fin ) → ¬ 𝑆 ∈ Fin )
18	16 17	pm2.65da	⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑆 = ∪ ran 𝑓 ) ) → ¬ 𝑇 ∈ Fin )
19	8 18	exlimddv	⊢ ( 𝜑 → ¬ 𝑇 ∈ Fin )