Theorem 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	⊢ ( 𝜑 → 𝐴 ∈ ( ACS ‘ 𝑋 ) )
	acsmapd.2	⊢ 𝑁 = ( mrCls ‘ 𝐴 )
	acsmapd.3	⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )
	acsmapd.4	⊢ ( 𝜑 → 𝑇 ⊆ ( 𝑁 ‘ 𝑆 ) )
Assertion	acsmapd	⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		acsmapd.1	⊢ ( 𝜑 → 𝐴 ∈ ( ACS ‘ 𝑋 ) )
2		acsmapd.2	⊢ 𝑁 = ( mrCls ‘ 𝐴 )
3		acsmapd.3	⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )
4		acsmapd.4	⊢ ( 𝜑 → 𝑇 ⊆ ( 𝑁 ‘ 𝑆 ) )
5		fvex	⊢ ( 𝑁 ‘ 𝑆 ) ∈ V
6	5	ssex	⊢ ( 𝑇 ⊆ ( 𝑁 ‘ 𝑆 ) → 𝑇 ∈ V )
7	4 6	syl	⊢ ( 𝜑 → 𝑇 ∈ V )
8	4	sseld	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑇 → 𝑥 ∈ ( 𝑁 ‘ 𝑆 ) ) )
9	1 2 3	acsficl2d	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑁 ‘ 𝑆 ) ↔ ∃ 𝑦 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑥 ∈ ( 𝑁 ‘ 𝑦 ) ) )
10	8 9	sylibd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑇 → ∃ 𝑦 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑥 ∈ ( 𝑁 ‘ 𝑦 ) ) )
11	10	ralrimiv	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑥 ∈ ( 𝑁 ‘ 𝑦 ) )
12		fveq2	⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑁 ‘ 𝑦 ) = ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) )
13	12	eleq2d	⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑥 ∈ ( 𝑁 ‘ 𝑦 ) ↔ 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) )
14	13	ac6sg	⊢ ( 𝑇 ∈ V → ( ∀ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑥 ∈ ( 𝑁 ‘ 𝑦 ) → ∃ 𝑓 ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) )
15	7 11 14	sylc	⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) )
16		simprl	⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) → 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) )
17		nfv	⊢ Ⅎ 𝑥 𝜑
18		nfv	⊢ Ⅎ 𝑥 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin )
19		nfra1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) )
20	18 19	nfan	⊢ Ⅎ 𝑥 ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) )
21	17 20	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) )
22	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → 𝐴 ∈ ( ACS ‘ 𝑋 ) )
23	22	acsmred	⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
24		simplrl	⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) )
25	24	ffnd	⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → 𝑓 Fn 𝑇 )
26		fnfvelrn	⊢ ( ( 𝑓 Fn 𝑇 ∧ 𝑥 ∈ 𝑇 ) → ( 𝑓 ‘ 𝑥 ) ∈ ran 𝑓 )
27	25 26	sylancom	⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → ( 𝑓 ‘ 𝑥 ) ∈ ran 𝑓 )
28	27	snssd	⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → { ( 𝑓 ‘ 𝑥 ) } ⊆ ran 𝑓 )
29	28	unissd	⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → ∪ { ( 𝑓 ‘ 𝑥 ) } ⊆ ∪ ran 𝑓 )
30		frn	⊢ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) → ran 𝑓 ⊆ ( 𝒫 𝑆 ∩ Fin ) )
31	30	unissd	⊢ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) → ∪ ran 𝑓 ⊆ ∪ ( 𝒫 𝑆 ∩ Fin ) )
32		unifpw	⊢ ∪ ( 𝒫 𝑆 ∩ Fin ) = 𝑆
33	31 32	sseqtrdi	⊢ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) → ∪ ran 𝑓 ⊆ 𝑆 )
34	24 33	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → ∪ ran 𝑓 ⊆ 𝑆 )
35	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → 𝑆 ⊆ 𝑋 )
36	34 35	sstrd	⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → ∪ ran 𝑓 ⊆ 𝑋 )
37	23 2 29 36	mrcssd	⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → ( 𝑁 ‘ ∪ { ( 𝑓 ‘ 𝑥 ) } ) ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) )
38		simprr	⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) → ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) )
39	38	r19.21bi	⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) )
40		fvex	⊢ ( 𝑓 ‘ 𝑥 ) ∈ V
41	40	unisn	⊢ ∪ { ( 𝑓 ‘ 𝑥 ) } = ( 𝑓 ‘ 𝑥 )
42	41	fveq2i	⊢ ( 𝑁 ‘ ∪ { ( 𝑓 ‘ 𝑥 ) } ) = ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) )
43	39 42	eleqtrrdi	⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → 𝑥 ∈ ( 𝑁 ‘ ∪ { ( 𝑓 ‘ 𝑥 ) } ) )
44	37 43	sseldd	⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → 𝑥 ∈ ( 𝑁 ‘ ∪ ran 𝑓 ) )
45	44	ex	⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) → ( 𝑥 ∈ 𝑇 → 𝑥 ∈ ( 𝑁 ‘ ∪ ran 𝑓 ) ) )
46	21 45	alrimi	⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) → ∀ 𝑥 ( 𝑥 ∈ 𝑇 → 𝑥 ∈ ( 𝑁 ‘ ∪ ran 𝑓 ) ) )
47		df-ss	⊢ ( 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑇 → 𝑥 ∈ ( 𝑁 ‘ ∪ ran 𝑓 ) ) )
48	46 47	sylibr	⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) → 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) )
49	16 48	jca	⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) → ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ) )
50	49	ex	⊢ ( 𝜑 → ( ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) → ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ) ) )
51	50	eximdv	⊢ ( 𝜑 → ( ∃ 𝑓 ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) → ∃ 𝑓 ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ) ) )
52	15 51	mpd	⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ) )