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

Proof

Step	Hyp	Ref	Expression
1		acsmap2d.1	$⊢ φ \to A \in ACS (X)$
2		acsmap2d.2	$⊢ N = mrCls (A)$
3		acsmap2d.3	$⊢ I = mrInd (A)$
4		acsmap2d.4	$⊢ φ \to S \in I$
5		acsmap2d.5	$⊢ φ \to T \subseteq X$
6		acsmap2d.6	$⊢ φ \to N (S) = N (T)$
7		acsinfd.7	$⊢ φ \to \neg S \in Fin$
8	1 2 3 4 5 6	acsmap2d	$⊢ φ \to \exists f (f : T ⟶ 𝒫 S \cap Fin \land S = ⋃ ran f)$
9		simplrr	$⊢ ((φ \land (f : T ⟶ 𝒫 S \cap Fin \land S = ⋃ ran f)) \land T \in Fin) \to S = ⋃ ran f$
10		simplrl	$⊢ ((φ \land (f : T ⟶ 𝒫 S \cap Fin \land S = ⋃ ran f)) \land T \in Fin) \to f : T ⟶ 𝒫 S \cap Fin$
11		inss2	$⊢ 𝒫 S \cap Fin \subseteq Fin$
12		fss	$⊢ (f : T ⟶ 𝒫 S \cap Fin \land 𝒫 S \cap Fin \subseteq Fin) \to f : T ⟶ Fin$
13	10 11 12	sylancl	$⊢ ((φ \land (f : T ⟶ 𝒫 S \cap Fin \land S = ⋃ ran f)) \land T \in Fin) \to f : T ⟶ Fin$
14		simpr	$⊢ ((φ \land (f : T ⟶ 𝒫 S \cap Fin \land S = ⋃ ran f)) \land T \in Fin) \to T \in Fin$
15	13 14	unirnffid	$⊢ ((φ \land (f : T ⟶ 𝒫 S \cap Fin \land S = ⋃ ran f)) \land T \in Fin) \to ⋃ ran f \in Fin$
16	9 15	eqeltrd	$⊢ ((φ \land (f : T ⟶ 𝒫 S \cap Fin \land S = ⋃ ran f)) \land T \in Fin) \to S \in Fin$
17	7	ad2antrr	$⊢ ((φ \land (f : T ⟶ 𝒫 S \cap Fin \land S = ⋃ ran f)) \land T \in Fin) \to \neg S \in Fin$
18	16 17	pm2.65da	$⊢ (φ \land (f : T ⟶ 𝒫 S \cap Fin \land S = ⋃ ran f)) \to \neg T \in Fin$
19	8 18	exlimddv	$⊢ φ \to \neg T \in Fin$

Metamath Proof Explorer

Theorem acsinfd

Proof