acsmapd

Description: In an algebraic closure system, if T is contained in the closure of S , there is a map f from T into the set of finite subsets of S such that the closure of U. ran f contains T . This is proven by applying acsficl2d to each element of T . See Section II.5 in Cohn p. 81 to 82. (Contributed by David Moews, 1-May-2017) Remove dependency on ax-reg and ax-inf2 . (Revised by Timothy J. O'Malley, 15-Oct-2026)

	Ref	Expression
Hypotheses	acsmapd.1	$⊢ φ \to A \in ACS (X)$
	acsmapd.2	$⊢ N = mrCls (A)$
	acsmapd.3	$⊢ φ \to S \subseteq X$
	acsmapd.4	$⊢ φ \to T \subseteq N (S)$
Assertion	acsmapd	$⊢ φ \to \exists f (f : T ⟶ 𝒫 S \cap Fin \land T \subseteq N (⋃ ran f))$

Proof

Step	Hyp	Ref	Expression
1		acsmapd.1	$⊢ φ \to A \in ACS (X)$
2		acsmapd.2	$⊢ N = mrCls (A)$
3		acsmapd.3	$⊢ φ \to S \subseteq X$
4		acsmapd.4	$⊢ φ \to T \subseteq N (S)$
5		fvex	$⊢ N (S) \in V$
6	5	ssex	$⊢ T \subseteq N (S) \to T \in V$
7	4 6	syl	$⊢ φ \to T \in V$
8	1	elfvexd	$⊢ φ \to X \in V$
9	8 3	ssexd	$⊢ φ \to S \in V$
10	9	pwexd	$⊢ φ \to 𝒫 S \in V$
11		inex1g	$⊢ 𝒫 S \in V \to 𝒫 S \cap Fin \in V$
12	10 11	syl	$⊢ φ \to 𝒫 S \cap Fin \in V$
13	4	sseld	$⊢ φ \to (x \in T \to x \in N (S))$
14	1 2 3	acsficl2d	$⊢ φ \to (x \in N (S) \leftrightarrow \exists y \in (𝒫 S \cap Fin) x \in N (y))$
15	13 14	sylibd	$⊢ φ \to (x \in T \to \exists y \in (𝒫 S \cap Fin) x \in N (y))$
16	15	ralrimiv	$⊢ φ \to \forall x \in T \exists y \in (𝒫 S \cap Fin) x \in N (y)$
17		fveq2	$⊢ y = f (x) \to N (y) = N (f (x))$
18	17	eleq2d	$⊢ y = f (x) \to (x \in N (y) \leftrightarrow x \in N (f (x)))$
19	18	ac6	$⊢ (T \in V \land 𝒫 S \cap Fin \in V \land \forall x \in T \exists y \in (𝒫 S \cap Fin) x \in N (y)) \to \exists f (f : T ⟶ 𝒫 S \cap Fin \land \forall x \in T x \in N (f (x)))$
20	7 12 16 19	syl3anc	$⊢ φ \to \exists f (f : T ⟶ 𝒫 S \cap Fin \land \forall x \in T x \in N (f (x)))$
21		simprl	$⊢ (φ \land (f : T ⟶ 𝒫 S \cap Fin \land \forall x \in T x \in N (f (x)))) \to f : T ⟶ 𝒫 S \cap Fin$
22		nfv	$⊢ Ⅎ x φ$
23		nfv	$⊢ Ⅎ x f : T ⟶ 𝒫 S \cap Fin$
24		nfra1	$⊢ Ⅎ x \forall x \in T x \in N (f (x))$
25	23 24	nfan	$⊢ Ⅎ x (f : T ⟶ 𝒫 S \cap Fin \land \forall x \in T x \in N (f (x)))$
26	22 25	nfan	$⊢ Ⅎ x (φ \land (f : T ⟶ 𝒫 S \cap Fin \land \forall x \in T x \in N (f (x))))$
27	1	ad2antrr	$⊢ ((φ \land (f : T ⟶ 𝒫 S \cap Fin \land \forall x \in T x \in N (f (x)))) \land x \in T) \to A \in ACS (X)$
28	27	acsmred	$⊢ ((φ \land (f : T ⟶ 𝒫 S \cap Fin \land \forall x \in T x \in N (f (x)))) \land x \in T) \to A \in Moore (X)$
29		simplrl	$⊢ ((φ \land (f : T ⟶ 𝒫 S \cap Fin \land \forall x \in T x \in N (f (x)))) \land x \in T) \to f : T ⟶ 𝒫 S \cap Fin$
30	29	ffnd	$⊢ ((φ \land (f : T ⟶ 𝒫 S \cap Fin \land \forall x \in T x \in N (f (x)))) \land x \in T) \to f Fn T$
31		fnfvelrn	$⊢ (f Fn T \land x \in T) \to f (x) \in ran f$
32	30 31	sylancom	$⊢ ((φ \land (f : T ⟶ 𝒫 S \cap Fin \land \forall x \in T x \in N (f (x)))) \land x \in T) \to f (x) \in ran f$
33	32	snssd	$⊢ ((φ \land (f : T ⟶ 𝒫 S \cap Fin \land \forall x \in T x \in N (f (x)))) \land x \in T) \to \{f (x)\} \subseteq ran f$
34	33	unissd	$⊢ ((φ \land (f : T ⟶ 𝒫 S \cap Fin \land \forall x \in T x \in N (f (x)))) \land x \in T) \to ⋃ \{f (x)\} \subseteq ⋃ ran f$
35		frn	$⊢ f : T ⟶ 𝒫 S \cap Fin \to ran f \subseteq 𝒫 S \cap Fin$
36	35	unissd	$⊢ f : T ⟶ 𝒫 S \cap Fin \to ⋃ ran f \subseteq ⋃ (𝒫 S \cap Fin)$
37		unifpw	$⊢ ⋃ (𝒫 S \cap Fin) = S$
38	36 37	sseqtrdi	$⊢ f : T ⟶ 𝒫 S \cap Fin \to ⋃ ran f \subseteq S$
39	29 38	syl	$⊢ ((φ \land (f : T ⟶ 𝒫 S \cap Fin \land \forall x \in T x \in N (f (x)))) \land x \in T) \to ⋃ ran f \subseteq S$
40	3	ad2antrr	$⊢ ((φ \land (f : T ⟶ 𝒫 S \cap Fin \land \forall x \in T x \in N (f (x)))) \land x \in T) \to S \subseteq X$
41	39 40	sstrd	$⊢ ((φ \land (f : T ⟶ 𝒫 S \cap Fin \land \forall x \in T x \in N (f (x)))) \land x \in T) \to ⋃ ran f \subseteq X$
42	28 2 34 41	mrcssd	$⊢ ((φ \land (f : T ⟶ 𝒫 S \cap Fin \land \forall x \in T x \in N (f (x)))) \land x \in T) \to N (⋃ \{f (x)\}) \subseteq N (⋃ ran f)$
43		simprr	$⊢ (φ \land (f : T ⟶ 𝒫 S \cap Fin \land \forall x \in T x \in N (f (x)))) \to \forall x \in T x \in N (f (x))$
44	43	r19.21bi	$⊢ ((φ \land (f : T ⟶ 𝒫 S \cap Fin \land \forall x \in T x \in N (f (x)))) \land x \in T) \to x \in N (f (x))$
45		fvex	$⊢ f (x) \in V$
46	45	unisn	$⊢ ⋃ \{f (x)\} = f (x)$
47	46	fveq2i	$⊢ N (⋃ \{f (x)\}) = N (f (x))$
48	44 47	eleqtrrdi	$⊢ ((φ \land (f : T ⟶ 𝒫 S \cap Fin \land \forall x \in T x \in N (f (x)))) \land x \in T) \to x \in N (⋃ \{f (x)\})$
49	42 48	sseldd	$⊢ ((φ \land (f : T ⟶ 𝒫 S \cap Fin \land \forall x \in T x \in N (f (x)))) \land x \in T) \to x \in N (⋃ ran f)$
50	49	ex	$⊢ (φ \land (f : T ⟶ 𝒫 S \cap Fin \land \forall x \in T x \in N (f (x)))) \to (x \in T \to x \in N (⋃ ran f))$
51	26 50	alrimi	$⊢ (φ \land (f : T ⟶ 𝒫 S \cap Fin \land \forall x \in T x \in N (f (x)))) \to \forall x (x \in T \to x \in N (⋃ ran f))$
52		df-ss	$⊢ T \subseteq N (⋃ ran f) \leftrightarrow \forall x (x \in T \to x \in N (⋃ ran f))$
53	51 52	sylibr	$⊢ (φ \land (f : T ⟶ 𝒫 S \cap Fin \land \forall x \in T x \in N (f (x)))) \to T \subseteq N (⋃ ran f)$
54	21 53	jca	$⊢ (φ \land (f : T ⟶ 𝒫 S \cap Fin \land \forall x \in T x \in N (f (x)))) \to (f : T ⟶ 𝒫 S \cap Fin \land T \subseteq N (⋃ ran f))$
55	54	ex	$⊢ φ \to ((f : T ⟶ 𝒫 S \cap Fin \land \forall x \in T x \in N (f (x))) \to (f : T ⟶ 𝒫 S \cap Fin \land T \subseteq N (⋃ ran f)))$
56	55	eximdv	$⊢ φ \to (\exists f (f : T ⟶ 𝒫 S \cap Fin \land \forall x \in T x \in N (f (x))) \to \exists f (f : T ⟶ 𝒫 S \cap Fin \land T \subseteq N (⋃ ran f)))$
57	20 56	mpd	$⊢ φ \to \exists f (f : T ⟶ 𝒫 S \cap Fin \land T \subseteq N (⋃ ran f))$

Metamath Proof Explorer

Theorem acsmapd

Proof