acsdomd

Description: In an algebraic closure system, if S and T have the same closure and S is infinite independent, then T dominates S . This follows from applying acsinfd and then applying unirnfdomd 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	acsdomd	$⊢ φ \to S ≼ T$

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		simprr	$⊢ (φ \land (f : T ⟶ 𝒫 S \cap Fin \land S = ⋃ ran f)) \to S = ⋃ ran f$
10		simprl	$⊢ (φ \land (f : T ⟶ 𝒫 S \cap Fin \land S = ⋃ ran f)) \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)) \to f : T ⟶ Fin$
14	1 2 3 4 5 6 7	acsinfd	$⊢ φ \to \neg T \in Fin$
15	14	adantr	$⊢ (φ \land (f : T ⟶ 𝒫 S \cap Fin \land S = ⋃ ran f)) \to \neg T \in Fin$
16	1	adantr	$⊢ (φ \land (f : T ⟶ 𝒫 S \cap Fin \land S = ⋃ ran f)) \to A \in ACS (X)$
17	16	elfvexd	$⊢ (φ \land (f : T ⟶ 𝒫 S \cap Fin \land S = ⋃ ran f)) \to X \in V$
18	5	adantr	$⊢ (φ \land (f : T ⟶ 𝒫 S \cap Fin \land S = ⋃ ran f)) \to T \subseteq X$
19	17 18	ssexd	$⊢ (φ \land (f : T ⟶ 𝒫 S \cap Fin \land S = ⋃ ran f)) \to T \in V$
20	13 15 19	unirnfdomd	$⊢ (φ \land (f : T ⟶ 𝒫 S \cap Fin \land S = ⋃ ran f)) \to ⋃ ran f ≼ T$
21	9 20	eqbrtrd	$⊢ (φ \land (f : T ⟶ 𝒫 S \cap Fin \land S = ⋃ ran f)) \to S ≼ T$
22	8 21	exlimddv	$⊢ φ \to S ≼ T$

Metamath Proof Explorer

Theorem acsdomd

Proof