Metamath Proof Explorer


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 dfss2 ( 𝑇 ⊆ ( 𝑁 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 𝑓 ) ) )