acsmap2d

Description: In an algebraic closure system, if S and T have the same closure and S is independent, then there is a map f from T into the set of finite subsets of S such that S equals the union of ran f . This is proven by taking the map f from acsmapd and observing that, since S and T have the same closure, the closure of U. ran f must contain S . Since S is independent, by mrissmrcd , U. ran f must equal S . 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)$
Assertion	acsmap2d	$⊢ φ \to \exists f (f : T ⟶ 𝒫 S \cap Fin \land S = ⋃ ran f)$

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	1	acsmred	$⊢ φ \to A \in Moore (X)$
8	3 7 4	mrissd	$⊢ φ \to S \subseteq X$
9	7 2 5	mrcssidd	$⊢ φ \to T \subseteq N (T)$
10	9 6	sseqtrrd	$⊢ φ \to T \subseteq N (S)$
11	1 2 8 10	acsmapd	$⊢ φ \to \exists f (f : T ⟶ 𝒫 S \cap Fin \land T \subseteq N (⋃ ran f))$
12		simprl	$⊢ (φ \land (f : T ⟶ 𝒫 S \cap Fin \land T \subseteq N (⋃ ran f))) \to f : T ⟶ 𝒫 S \cap Fin$
13	7	adantr	$⊢ (φ \land (f : T ⟶ 𝒫 S \cap Fin \land T \subseteq N (⋃ ran f))) \to A \in Moore (X)$
14	4	adantr	$⊢ (φ \land (f : T ⟶ 𝒫 S \cap Fin \land T \subseteq N (⋃ ran f))) \to S \in I$
15	3 13 14	mrissd	$⊢ (φ \land (f : T ⟶ 𝒫 S \cap Fin \land T \subseteq N (⋃ ran f))) \to S \subseteq X$
16	13 2 15	mrcssidd	$⊢ (φ \land (f : T ⟶ 𝒫 S \cap Fin \land T \subseteq N (⋃ ran f))) \to S \subseteq N (S)$
17	6	adantr	$⊢ (φ \land (f : T ⟶ 𝒫 S \cap Fin \land T \subseteq N (⋃ ran f))) \to N (S) = N (T)$
18		simprr	$⊢ (φ \land (f : T ⟶ 𝒫 S \cap Fin \land T \subseteq N (⋃ ran f))) \to T \subseteq N (⋃ ran f)$
19	13 2	mrcssvd	$⊢ (φ \land (f : T ⟶ 𝒫 S \cap Fin \land T \subseteq N (⋃ ran f))) \to N (⋃ ran f) \subseteq X$
20	13 2 18 19	mrcssd	$⊢ (φ \land (f : T ⟶ 𝒫 S \cap Fin \land T \subseteq N (⋃ ran f))) \to N (T) \subseteq N (N (⋃ ran f))$
21		frn	$⊢ f : T ⟶ 𝒫 S \cap Fin \to ran f \subseteq 𝒫 S \cap Fin$
22	21	unissd	$⊢ f : T ⟶ 𝒫 S \cap Fin \to ⋃ ran f \subseteq ⋃ (𝒫 S \cap Fin)$
23		unifpw	$⊢ ⋃ (𝒫 S \cap Fin) = S$
24	22 23	sseqtrdi	$⊢ f : T ⟶ 𝒫 S \cap Fin \to ⋃ ran f \subseteq S$
25	24	ad2antrl	$⊢ (φ \land (f : T ⟶ 𝒫 S \cap Fin \land T \subseteq N (⋃ ran f))) \to ⋃ ran f \subseteq S$
26	25 15	sstrd	$⊢ (φ \land (f : T ⟶ 𝒫 S \cap Fin \land T \subseteq N (⋃ ran f))) \to ⋃ ran f \subseteq X$
27	13 2 26	mrcidmd	$⊢ (φ \land (f : T ⟶ 𝒫 S \cap Fin \land T \subseteq N (⋃ ran f))) \to N (N (⋃ ran f)) = N (⋃ ran f)$
28	20 27	sseqtrd	$⊢ (φ \land (f : T ⟶ 𝒫 S \cap Fin \land T \subseteq N (⋃ ran f))) \to N (T) \subseteq N (⋃ ran f)$
29	17 28	eqsstrd	$⊢ (φ \land (f : T ⟶ 𝒫 S \cap Fin \land T \subseteq N (⋃ ran f))) \to N (S) \subseteq N (⋃ ran f)$
30	16 29	sstrd	$⊢ (φ \land (f : T ⟶ 𝒫 S \cap Fin \land T \subseteq N (⋃ ran f))) \to S \subseteq N (⋃ ran f)$
31	13 2 3 30 25 14	mrissmrcd	$⊢ (φ \land (f : T ⟶ 𝒫 S \cap Fin \land T \subseteq N (⋃ ran f))) \to S = ⋃ ran f$
32	12 31	jca	$⊢ (φ \land (f : T ⟶ 𝒫 S \cap Fin \land T \subseteq N (⋃ ran f))) \to (f : T ⟶ 𝒫 S \cap Fin \land S = ⋃ ran f)$
33	32	ex	$⊢ φ \to ((f : T ⟶ 𝒫 S \cap Fin \land T \subseteq N (⋃ ran f)) \to (f : T ⟶ 𝒫 S \cap Fin \land S = ⋃ ran f))$
34	33	eximdv	$⊢ φ \to (\exists f (f : T ⟶ 𝒫 S \cap Fin \land T \subseteq N (⋃ ran f)) \to \exists f (f : T ⟶ 𝒫 S \cap Fin \land S = ⋃ ran f))$
35	11 34	mpd	$⊢ φ \to \exists f (f : T ⟶ 𝒫 S \cap Fin \land S = ⋃ ran f)$

Metamath Proof Explorer

Theorem acsmap2d

Proof