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)

	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	4	sseld	$⊢ φ \to (x \in T \to x \in N (S))$
9	1 2 3	acsficl2d	$⊢ φ \to (x \in N (S) \leftrightarrow \exists y \in (𝒫 S \cap Fin) x \in N (y))$
10	8 9	sylibd	$⊢ φ \to (x \in T \to \exists y \in (𝒫 S \cap Fin) x \in N (y))$
11	10	ralrimiv	$⊢ φ \to \forall x \in T \exists y \in (𝒫 S \cap Fin) x \in N (y)$
12		fveq2	$⊢ y = f (x) \to N (y) = N (f (x))$
13	12	eleq2d	$⊢ y = f (x) \to (x \in N (y) \leftrightarrow x \in N (f (x)))$
14	13	ac6sg	$⊢ T \in V \to (\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))))$
15	7 11 14	sylc	$⊢ φ \to \exists f (f : T ⟶ 𝒫 S \cap Fin \land \forall x \in T x \in N (f (x)))$
16		simprl	$⊢ (φ \land (f : T ⟶ 𝒫 S \cap Fin \land \forall x \in T x \in N (f (x)))) \to f : T ⟶ 𝒫 S \cap Fin$
17		nfv	$⊢ Ⅎ x φ$
18		nfv	$⊢ Ⅎ x f : T ⟶ 𝒫 S \cap Fin$
19		nfra1	$⊢ Ⅎ x \forall x \in T x \in N (f (x))$
20	18 19	nfan	$⊢ Ⅎ x (f : T ⟶ 𝒫 S \cap Fin \land \forall x \in T x \in N (f (x)))$
21	17 20	nfan	$⊢ Ⅎ x (φ \land (f : T ⟶ 𝒫 S \cap Fin \land \forall x \in T x \in N (f (x))))$
22	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)$
23	22	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)$
24		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$
25	24	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$
26		fnfvelrn	$⊢ (f Fn T \land x \in T) \to f (x) \in ran f$
27	25 26	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$
28	27	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$
29	28	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$
30		frn	$⊢ f : T ⟶ 𝒫 S \cap Fin \to ran f \subseteq 𝒫 S \cap Fin$
31	30	unissd	$⊢ f : T ⟶ 𝒫 S \cap Fin \to ⋃ ran f \subseteq ⋃ (𝒫 S \cap Fin)$
32		unifpw	$⊢ ⋃ (𝒫 S \cap Fin) = S$
33	31 32	sseqtrdi	$⊢ f : T ⟶ 𝒫 S \cap Fin \to ⋃ ran f \subseteq S$
34	24 33	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$
35	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$
36	34 35	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$
37	23 2 29 36	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)$
38		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))$
39	38	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))$
40		fvex	$⊢ f (x) \in V$
41	40	unisn	$⊢ ⋃ \{f (x)\} = f (x)$
42	41	fveq2i	$⊢ N (⋃ \{f (x)\}) = N (f (x))$
43	39 42	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)\})$
44	37 43	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)$
45	44	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))$
46	21 45	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))$
47		df-ss	$⊢ T \subseteq N (⋃ ran f) \leftrightarrow \forall x (x \in T \to x \in N (⋃ ran f))$
48	46 47	sylibr	$⊢ (φ \land (f : T ⟶ 𝒫 S \cap Fin \land \forall x \in T x \in N (f (x)))) \to T \subseteq N (⋃ ran f)$
49	16 48	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))$
50	49	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)))$
51	50	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)))$
52	15 51	mpd	$⊢ φ \to \exists f (f : T ⟶ 𝒫 S \cap Fin \land T \subseteq N (⋃ ran f))$

Metamath Proof Explorer

Theorem acsmapd

Proof